diff options
Diffstat (limited to 'src/proof/cec/cecSynth.c')
| -rw-r--r-- | src/proof/cec/cecSynth.c | 380 |
1 files changed, 380 insertions, 0 deletions
diff --git a/src/proof/cec/cecSynth.c b/src/proof/cec/cecSynth.c new file mode 100644 index 00000000..21470dd4 --- /dev/null +++ b/src/proof/cec/cecSynth.c @@ -0,0 +1,380 @@ +/**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 "src/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, clk = 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_WriteAiger( 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", clock() - clk ); + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + |