/**CFile**************************************************************** FileName [cecSynth.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Combinational equivalence checking.] Synopsis [Partitioned sequential synthesis.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: cecSynth.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "cecInt.h" #include "aig/gia/giaAig.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Populate sequential synthesis parameters.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Cec_SeqSynthesisSetDefaultParams( Cec_ParSeq_t * p ) { memset( p, 0, sizeof(Cec_ParSeq_t) ); p->fUseLcorr = 0; // enables latch correspondence p->fUseScorr = 0; // enables signal correspondence p->nBTLimit = 1000; // (scorr/lcorr) conflict limit at a node p->nFrames = 1; // (scorr only) the number of timeframes p->nLevelMax = -1; // (scorr only) the max number of levels p->fConsts = 1; // (scl only) merging constants p->fEquivs = 1; // (scl only) merging equivalences p->fUseMiniSat = 0; // enables MiniSat in lcorr/scorr p->nMinDomSize = 100; // the size of minimum clock domain p->fVeryVerbose = 0; // verbose stats p->fVerbose = 0; // verbose stats } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_SeqReadMinDomSize( Cec_ParSeq_t * p ) { return p->nMinDomSize; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_SeqReadVerbose( Cec_ParSeq_t * p ) { return p->fVerbose; } /**Function************************************************************* Synopsis [Computes partitioning of registers.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Gia_Man_t * Gia_ManRegCreatePart( Gia_Man_t * p, Vec_Int_t * vPart, int * pnCountPis, int * pnCountRegs, int ** ppMapBack ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; Vec_Int_t * vNodes, * vRoots; int i, iOut, nCountPis, nCountRegs; int * pMapBack; // collect/mark nodes/PIs in the DFS order from the roots Gia_ManIncrementTravId( p ); vRoots = Vec_IntAlloc( Vec_IntSize(vPart) ); Vec_IntForEachEntry( vPart, iOut, i ) Vec_IntPush( vRoots, Gia_ObjId(p, Gia_ManCo(p, Gia_ManPoNum(p)+iOut)) ); vNodes = Gia_ManCollectNodesCis( p, Vec_IntArray(vRoots), Vec_IntSize(vRoots) ); Vec_IntFree( vRoots ); // unmark register outputs Vec_IntForEachEntry( vPart, iOut, i ) Gia_ObjSetTravIdPrevious( p, Gia_ManCi(p, Gia_ManPiNum(p)+iOut) ); // count pure PIs nCountPis = nCountRegs = 0; Gia_ManForEachPi( p, pObj, i ) nCountPis += Gia_ObjIsTravIdCurrent(p, pObj); // count outputs of other registers Gia_ManForEachRo( p, pObj, i ) nCountRegs += Gia_ObjIsTravIdCurrent(p, pObj); // should be !Gia_... ??? if ( pnCountPis ) *pnCountPis = nCountPis; if ( pnCountRegs ) *pnCountRegs = nCountRegs; // clean old manager Gia_ManFillValue(p); Gia_ManConst0(p)->Value = 0; // create the new manager pNew = Gia_ManStart( Vec_IntSize(vNodes) ); // create the PIs Gia_ManForEachCi( p, pObj, i ) if ( Gia_ObjIsTravIdCurrent(p, pObj) ) pObj->Value = Gia_ManAppendCi(pNew); // add variables for the register outputs // create fake POs to hold the register outputs Vec_IntForEachEntry( vPart, iOut, i ) { pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut); pObj->Value = Gia_ManAppendCi(pNew); Gia_ManAppendCo( pNew, pObj->Value ); Gia_ObjSetTravIdCurrent( p, pObj ); // added } // create the nodes Gia_ManForEachObjVec( vNodes, p, pObj, i ) if ( Gia_ObjIsAnd(pObj) ) pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); // add real POs for the registers Vec_IntForEachEntry( vPart, iOut, i ) { pObj = Gia_ManCo( p, Gia_ManPoNum(p)+iOut ); Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } Gia_ManSetRegNum( pNew, Vec_IntSize(vPart) ); // create map if ( ppMapBack ) { pMapBack = ABC_FALLOC( int, Gia_ManObjNum(pNew) ); // map constant nodes pMapBack[0] = 0; // logic cones of register outputs Gia_ManForEachObjVec( vNodes, p, pObj, i ) { // pObjNew = Aig_Regular(pObj->pData); // pMapBack[pObjNew->Id] = pObj->Id; assert( Abc_Lit2Var(Gia_ObjValue(pObj)) >= 0 ); assert( Abc_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) ); pMapBack[ Abc_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj); } // map register outputs Vec_IntForEachEntry( vPart, iOut, i ) { pObj = Gia_ManCi(p, Gia_ManPiNum(p)+iOut); // pObjNew = pObj->pData; // pMapBack[pObjNew->Id] = pObj->Id; assert( Abc_Lit2Var(Gia_ObjValue(pObj)) >= 0 ); assert( Abc_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) ); pMapBack[ Abc_Lit2Var(Gia_ObjValue(pObj)) ] = Gia_ObjId(p, pObj); } *ppMapBack = pMapBack; } Vec_IntFree( vNodes ); return pNew; } /**Function************************************************************* Synopsis [Transfers the classes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_TransferMappedClasses( Gia_Man_t * pPart, int * pMapBack, int * pReprs ) { Gia_Obj_t * pObj; int i, Id1, Id2, nClasses; if ( pPart->pReprs == NULL ) return 0; nClasses = 0; Gia_ManForEachObj( pPart, pObj, i ) { if ( Gia_ObjRepr(pPart, i) == GIA_VOID ) continue; assert( i < Gia_ManObjNum(pPart) ); assert( Gia_ObjRepr(pPart, i) < Gia_ManObjNum(pPart) ); Id1 = pMapBack[ i ]; Id2 = pMapBack[ Gia_ObjRepr(pPart, i) ]; if ( Id1 == Id2 ) continue; if ( Id1 < Id2 ) pReprs[Id2] = Id1; else pReprs[Id1] = Id2; nClasses++; } return nClasses; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Gia_ManFindRepr_rec( int * pReprs, int Id ) { if ( pReprs[Id] == 0 ) return 0; if ( pReprs[Id] == ~0 ) return Id; return Gia_ManFindRepr_rec( pReprs, pReprs[Id] ); } /**Function************************************************************* Synopsis [Normalizes equivalences.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Gia_ManNormalizeEquivalences( Gia_Man_t * p, int * pReprs ) { int i, iRepr; assert( p->pReprs == NULL ); assert( p->pNexts == NULL ); p->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) Gia_ObjSetRepr( p, i, GIA_VOID ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) { if ( pReprs[i] == ~0 ) continue; iRepr = Gia_ManFindRepr_rec( pReprs, i ); Gia_ObjSetRepr( p, i, iRepr ); } p->pNexts = Gia_ManDeriveNexts( p ); } /**Function************************************************************* Synopsis [Partitioned sequential synthesis.] Description [Returns AIG annotated with equivalence classes.] SideEffects [] SeeAlso [] ***********************************************************************/ int Cec_SequentialSynthesisPart( Gia_Man_t * p, Cec_ParSeq_t * pPars ) { int fPrintParts = 0; char Buffer[100]; Gia_Man_t * pTemp; Vec_Ptr_t * vParts = (Vec_Ptr_t *)p->vClockDoms; Vec_Int_t * vPart; int * pMapBack, * pReprs; int i, nCountPis, nCountRegs; int nClasses; abctime clk = Abc_Clock(); // save parameters if ( fPrintParts ) { // print partitions Abc_Print( 1, "The following clock domains are used:\n" ); Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) { pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, NULL ); sprintf( Buffer, "part%03d.aig", i ); Gia_AigerWrite( pTemp, Buffer, 0, 0 ); Abc_Print( 1, "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n", i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp) ); Gia_ManStop( pTemp ); } } // perform sequential synthesis for clock domains pReprs = ABC_FALLOC( int, Gia_ManObjNum(p) ); Vec_PtrForEachEntry( Vec_Int_t *, vParts, vPart, i ) { pTemp = Gia_ManRegCreatePart( p, vPart, &nCountPis, &nCountRegs, &pMapBack ); if ( nCountPis > 0 ) { if ( pPars->fUseScorr ) { Cec_ParCor_t CorPars, * pCorPars = &CorPars; Cec_ManCorSetDefaultParams( pCorPars ); pCorPars->nBTLimit = pPars->nBTLimit; pCorPars->nLevelMax = pPars->nLevelMax; pCorPars->fVerbose = pPars->fVeryVerbose; pCorPars->fUseCSat = 1; Cec_ManLSCorrespondenceClasses( pTemp, pCorPars ); } else if ( pPars->fUseLcorr ) { Cec_ParCor_t CorPars, * pCorPars = &CorPars; Cec_ManCorSetDefaultParams( pCorPars ); pCorPars->fLatchCorr = 1; pCorPars->nBTLimit = pPars->nBTLimit; pCorPars->fVerbose = pPars->fVeryVerbose; pCorPars->fUseCSat = 1; Cec_ManLSCorrespondenceClasses( pTemp, pCorPars ); } else { // pNew = Gia_ManSeqStructSweep( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose ); // Gia_ManStop( pNew ); Gia_ManSeqCleanupClasses( pTemp, pPars->fConsts, pPars->fEquivs, pPars->fVerbose ); } //Abc_Print( 1, "Part equivalences = %d.\n", Gia_ManEquivCountLitsAll(pTemp) ); nClasses = Gia_TransferMappedClasses( pTemp, pMapBack, pReprs ); if ( pPars->fVerbose ) { Abc_Print( 1, "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. Cl = %5d.\n", i, Vec_IntSize(vPart), Gia_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Gia_ManAndNum(pTemp), nClasses ); } } Gia_ManStop( pTemp ); ABC_FREE( pMapBack ); } // generate resulting equivalences Gia_ManNormalizeEquivalences( p, pReprs ); //Abc_Print( 1, "Total equivalences = %d.\n", Gia_ManEquivCountLitsAll(p) ); ABC_FREE( pReprs ); if ( pPars->fVerbose ) { Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); } return 1; } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END