diff options
Diffstat (limited to 'src/aig/cec/cecSynth.c')
| -rw-r--r-- | src/aig/cec/cecSynth.c | 380 |
1 files changed, 0 insertions, 380 deletions
diff --git a/src/aig/cec/cecSynth.c b/src/aig/cec/cecSynth.c deleted file mode 100644 index 52b50a43..00000000 --- a/src/aig/cec/cecSynth.c +++ /dev/null @@ -1,380 +0,0 @@ -/**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 "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( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 ); - assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) ); - pMapBack[ Gia_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( Gia_Lit2Var(Gia_ObjValue(pObj)) >= 0 ); - assert( Gia_Lit2Var(Gia_ObjValue(pObj)) < Gia_ManObjNum(pNew) ); - pMapBack[ Gia_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 - |