| /**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; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Gia_ManTestOnePair_rec( sat_solver * pSat, Gia_Man_t * p, int iObj, Vec_Int_t * vSatVar ) |
| { |
| Gia_Obj_t * pObj; |
| int iVar, iVar0, iVar1; |
| if ( Vec_IntEntry(vSatVar, iObj) >= 0 ) |
| return Vec_IntEntry(vSatVar, iObj); |
| iVar = sat_solver_addvar(pSat); |
| Vec_IntWriteEntry( vSatVar, iObj, iVar ); |
| pObj = Gia_ManObj( p, iObj ); |
| if ( Gia_ObjIsAnd(pObj) ) |
| { |
| iVar0 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId0(pObj, iObj), vSatVar ); |
| iVar1 = Gia_ManTestOnePair_rec( pSat, p, Gia_ObjFaninId1(pObj, iObj), vSatVar ); |
| sat_solver_add_and( pSat, iVar, iVar0, iVar1, Gia_ObjFaninC0(pObj), Gia_ObjFaninC1(pObj), 0 ); |
| } |
| return iVar; |
| } |
| int Gia_ManTestOnePair( Gia_Man_t * p, int iObj1, int iObj2, int fPhase ) |
| { |
| int Lits[2] = {1}, status; |
| sat_solver * pSat = sat_solver_new(); |
| Vec_Int_t * vSatVar = Vec_IntStartFull( Gia_ManObjNum(p) ); |
| Vec_IntWriteEntry( vSatVar, 0, sat_solver_addvar(pSat) ); |
| sat_solver_addclause( pSat, Lits, Lits + 1 ); |
| Gia_ManTestOnePair_rec( pSat, p, iObj1, vSatVar ); |
| Gia_ManTestOnePair_rec( pSat, p, iObj2, vSatVar ); |
| Lits[0] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj1), 1 ); |
| Lits[1] = Abc_Var2Lit( Vec_IntEntry(vSatVar, iObj2), fPhase ); |
| status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 ); |
| if ( status == l_False ) |
| { |
| Lits[0] = Abc_LitNot( Lits[0] ); |
| Lits[1] = Abc_LitNot( Lits[1] ); |
| status = sat_solver_solve( pSat, Lits, Lits + 2, 0, 0, 0, 0 ); |
| } |
| Vec_IntFree( vSatVar ); |
| sat_solver_delete( pSat ); |
| return status; |
| } |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
