diff options
Diffstat (limited to 'src/base/abci')
| -rw-r--r-- | src/base/abci/abc.c | 14 | ||||
| -rw-r--r-- | src/base/abci/abcClpBdd.c | 42 | ||||
| -rw-r--r-- | src/base/abci/abcIvy.c | 9 | ||||
| -rw-r--r-- | src/base/abci/abcMiter.c | 94 | ||||
| -rw-r--r-- | src/base/abci/abcNtbdd.c | 55 | ||||
| -rw-r--r-- | src/base/abci/abcOrder.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcPrint.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcResub.c | 12 | ||||
| -rw-r--r-- | src/base/abci/abcRr.c | 8 | ||||
| -rw-r--r-- | src/base/abci/abcStrash.c | 2 | ||||
| -rw-r--r-- | src/base/abci/abcSweep.c | 24 | ||||
| -rw-r--r-- | src/base/abci/abcTiming.c | 4 | ||||
| -rw-r--r-- | src/base/abci/abcUnreach.c | 9 | ||||
| -rw-r--r-- | src/base/abci/abcVanEijk.c | 824 | ||||
| -rw-r--r-- | src/base/abci/abcVanImp.c | 1002 | ||||
| -rw-r--r-- | src/base/abci/abcVerify.c | 2 | ||||
| -rw-r--r-- | src/base/abci/module.make | 2 |
17 files changed, 141 insertions, 1966 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8cf0e0af..bbc9a226 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -3901,8 +3901,7 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( argc == globalUtilOptind + 1 ) { - pNodeCo = Abc_NtkFindTerm( pNtk, argv[globalUtilOptind] ); - pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); @@ -7433,6 +7432,8 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); + printf( "This command is not implemented\n" ); + // set defaults nFrames = 1; fExdc = 1; @@ -7495,10 +7496,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - if ( fImp ) - pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose ); - else - pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); +// if ( fImp ) +// pNtkRes = Abc_NtkVanImp( pNtk, nFrames, fExdc, fVerbose ); +// else +// pNtkRes = Abc_NtkVanEijk( pNtk, nFrames, fExdc, fVerbose ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c index 1de087e8..650f379f 100644 --- a/src/base/abci/abcClpBdd.c +++ b/src/base/abci/abcClpBdd.c @@ -25,7 +25,6 @@ //////////////////////////////////////////////////////////////////////// static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ); //////////////////////////////////////////////////////////////////////// @@ -59,10 +58,7 @@ Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, i } // create the new network - if ( fDualRail ) - pNtkNew = Abc_NtkFromGlobalBddsDual( pNtk ); - else - pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); + pNtkNew = Abc_NtkFromGlobalBdds( pNtk ); Abc_NtkFreeGlobalBdds( pNtk ); if ( pNtkNew == NULL ) { @@ -134,42 +130,6 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk ) -{ - ProgressBar * pProgress; - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pNode, * pNodeNew; - DdManager * dd = pNtk->pManGlob; - int i; - // start the new network - pNtkNew = Abc_NtkStartFromDual( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD ); - // make sure the new manager has the same number of inputs - Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 ); - // process the POs - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Cudd_Not( Vec_PtrEntry(pNtk->vFuncsGlob, i) ) ); - Abc_ObjAddFanin( pNode->pCopy->pCopy, pNodeNew ); - pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) ); - Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); - } - Extra_ProgressBarStop( pProgress ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Derives the network with the given global BDD.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc ) { Abc_Obj_t * pNodeNew, * pTemp; diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 6538b360..dae5408d 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -502,6 +502,10 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) { pObjNew = Abc_NtkCreateLatch( pNtk ); + pFaninNew0 = Abc_NtkCreateBo( pNtk ); + pFaninNew1 = Abc_NtkCreateBi( pNtk ); + Abc_ObjAddFanin( pObjNew, pFaninNew0 ); + Abc_ObjAddFanin( pFaninNew1, pObjNew ); if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC ) Abc_LatchSetInitDc( pObjNew ); else if ( Ivy_ObjInit(pNode) == IVY_INIT_1 ) @@ -509,8 +513,9 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig else if ( Ivy_ObjInit(pNode) == IVY_INIT_0 ) Abc_LatchSetInit0( pObjNew ); else assert( 0 ); - pNode->TravId = Abc_EdgeFromNode( pObjNew ); + pNode->TravId = Abc_EdgeFromNode( pFaninNew1 ); } + Abc_NtkAddDummyBoxNames( pNtk ); // rebuild the AIG Ivy_ManForEachNodeVec( pMan, vNodes, pNode, i ) { @@ -556,7 +561,7 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) { pFaninNew = Abc_ObjFanin0Ivy( pNtk, pNode ); - Abc_ObjAddFanin( Abc_NtkLatch(pNtk, i), pFaninNew ); + Abc_ObjAddFanin( Abc_ObjFanin0(Abc_NtkBox(pNtk, i)), pFaninNew ); } Vec_IntFree( vLatches ); Vec_IntFree( vNodes ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index ff05fe69..ab61dd45 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -54,6 +54,8 @@ Abc_Ntk_t * Abc_NtkMiter( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) { Abc_Ntk_t * pTemp = NULL; int fRemove1, fRemove2; + assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); // check that the networks have the same PIs/POs/latches if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, fComb ) ) return NULL; @@ -139,12 +141,12 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk pObj = Abc_NtkCi(pNtk2, i); pObj->pCopy = pObjNew; // add name - Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); } // create the only PO pObjNew = Abc_NtkCreatePo( pNtkMiter ); // add the PO name - Abc_NtkLogicStoreName( pObjNew, "miter" ); + Abc_ObjAssignName( pObjNew, "miter", NULL ); } else { @@ -157,24 +159,28 @@ void Abc_NtkMiterPrepare( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNtk pObj = Abc_NtkPi(pNtk2, i); pObj->pCopy = pObjNew; // add name - Abc_NtkLogicStoreName( pObjNew, Abc_ObjName(pObj) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), NULL ); } // create the only PO pObjNew = Abc_NtkCreatePo( pNtkMiter ); // add the PO name - Abc_NtkLogicStoreName( pObjNew, "miter" ); + Abc_ObjAssignName( pObjNew, "miter", NULL ); // create the latches Abc_NtkForEachLatch( pNtk1, pObj, i ) { - pObjNew = Abc_NtkDupObj( pNtkMiter, pObj ); - // add name - Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_1" ); + pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 ); + // add names + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_1" ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pObj)), "_1" ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_1" ); } Abc_NtkForEachLatch( pNtk2, pObj, i ) { - pObjNew = Abc_NtkDupObj( pNtkMiter, pObj ); + pObjNew = Abc_NtkDupBox( pNtkMiter, pObj, 0 ); // add name - Abc_NtkLogicStoreNamePlus( pObjNew, Abc_ObjName(pObj), "_2" ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pObj), "_2" ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pObj)), "_2" ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pObj)), "_2" ); } } } @@ -265,9 +271,9 @@ void Abc_NtkMiterFinalize( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Abc_Ntk_t * pNt } // connect new latches Abc_NtkForEachLatch( pNtk1, pNode, i ) - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); + Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) ); Abc_NtkForEachLatch( pNtk2, pNode, i ) - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); + Abc_ObjAddFanin( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjChild0Copy(Abc_ObjFanin0(pNode)) ); } // add the miter pMiter = Abc_AigMiter( pNtkMiter->pManFunc, vPairs ); @@ -302,6 +308,8 @@ Abc_Ntk_t * Abc_NtkMiterAnd( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) assert( 0 == Abc_NtkLatchNum(pNtk1) ); assert( 0 == Abc_NtkLatchNum(pNtk2) ); assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk1) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk2) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -354,6 +362,7 @@ Abc_Ntk_t * Abc_NtkMiterCofactor( Abc_Ntk_t * pNtk, Vec_Int_t * vPiValues ) assert( Abc_NtkIsStrash(pNtk) ); assert( 1 == Abc_NtkCoNum(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -421,6 +430,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In assert( Out < Abc_NtkCoNum(pNtk) ); assert( In1 < Abc_NtkCiNum(pNtk) ); assert( In2 < Abc_NtkCiNum(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -486,6 +496,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) assert( Abc_NtkIsStrash(pNtk) ); assert( 1 == Abc_NtkCoNum(pNtk) ); assert( In < Abc_NtkCiNum(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); @@ -545,6 +556,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ) Abc_Ntk_t * pNtkTemp; Abc_Obj_t * pObj; int i; + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); Abc_NtkForEachPi( pNtk, pObj, i ) { @@ -663,34 +675,38 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) char Buffer[1000]; ProgressBar * pProgress; Abc_Ntk_t * pNtkFrames; - Abc_Obj_t * pLatch, * pLatchNew; + Abc_Obj_t * pLatch, * pLatchOut; int i, Counter; assert( nFrames > 0 ); assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsDfsOrdered(pNtk) ); + assert( Abc_NtkHasOnlyLatchBoxes(pNtk) ); // start the new network pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames ); pNtkFrames->pName = Extra_UtilStrsav(Buffer); + // map the constant nodes + Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { Abc_NtkForEachLatch( pNtk, pLatch, i ) - Abc_NtkDupObj( pNtkFrames, pLatch ); + Abc_NtkDupBox( pNtkFrames, pLatch, 1 ); } else { Counter = 0; Abc_NtkForEachLatch( pNtk, pLatch, i ) { + pLatchOut = Abc_ObjFanout0(pLatch); if ( Abc_LatchIsInitNone(pLatch) || Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI { - pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames); - Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) ); + pLatchOut->pCopy = Abc_NtkCreatePi(pNtkFrames); + Abc_ObjAssignName( pLatchOut->pCopy, Abc_ObjName(pLatchOut), NULL ); Counter++; } else - pLatch->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); + pLatchOut->pCopy = Abc_ObjNotCond( Abc_AigConst1(pNtkFrames), Abc_LatchIsInit0(pLatch) ); } if ( Counter ) printf( "Warning: %d uninitialized latches are replaced by free PI variables.\n", Counter ); @@ -708,22 +724,15 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) // connect the new latches to the outputs of the last frame if ( !fInitial ) { + // we cannot use pLatch->pCopy here because pLatch->pCopy is used for temporary storage of strashed values Abc_NtkForEachLatch( pNtk, pLatch, i ) - { - pLatchNew = Abc_NtkLatch(pNtkFrames, i); - Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); - Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); - } + Abc_ObjAddFanin( Abc_ObjFanin0(pLatch)->pCopy, Abc_ObjFanout0(pLatch)->pCopy ); } - Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pNext = NULL; // remove dangling nodes Abc_AigCleanup( pNtkFrames->pManFunc ); - // reorder the latches Abc_NtkOrderCisCos( pNtkFrames ); - // make sure that everything is okay if ( !Abc_NtkCheck( pNtkFrames ) ) { @@ -755,31 +764,29 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame ) int i; // create the prefix to be added to the node names sprintf( Buffer, "_%02d", iFrame ); - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); // add the new PI nodes Abc_NtkForEachPi( pNtk, pNode, i ) - Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer ); // add the internal nodes Abc_AigForEachAnd( pNtk, pNode, i ) pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); // add the new POs Abc_NtkForEachPo( pNtk, pNode, i ) { - Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer ); Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); } // add the new asserts Abc_NtkForEachAssert( pNtk, pNode, i ) { - Abc_NtkLogicStoreNamePlus( Abc_NtkDupObj(pNtkFrames, pNode), Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( Abc_NtkDupObj(pNtkFrames, pNode, 0), Abc_ObjName(pNode), Buffer ); Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); } - // transfer the implementation of the latch drivers to the latches + // transfer the implementation of the latch inputs to the latch outputs Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pNext = Abc_ObjChild0Copy(pLatch); + pLatch->pCopy = Abc_ObjChild0Copy(Abc_ObjFanin0(pLatch)); Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pCopy = pLatch->pNext; + Abc_ObjFanout0(pLatch)->pCopy = pLatch->pCopy; } @@ -797,6 +804,7 @@ void Abc_NtkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame ) ***********************************************************************/ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFrameMapping addFrameMapping, void* arg ) { +/* char Buffer[1000]; ProgressBar * pProgress; Abc_Ntk_t * pNtkFrames; @@ -825,7 +833,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram if ( Abc_LatchIsInitDc(pLatch) ) // don't-care initial value - create a new PI { pLatch->pCopy = Abc_NtkCreatePi(pNtkFrames); - Abc_NtkLogicStoreName( pLatch->pCopy, Abc_ObjName(pLatch) ); + Abc_ObjAssignName( pLatch->pCopy, Abc_ObjName(pLatch), NULL ); Counter++; } else { @@ -854,9 +862,9 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram { Abc_NtkForEachLatch( pNtk, pLatch, i ) { - pLatchNew = Abc_NtkLatch(pNtkFrames, i); + pLatchNew = Abc_NtkBox(pNtkFrames, i); Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); - Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); + Abc_ObjAssignName( pLatchNew, Abc_ObjName(pLatch), NULL ); } } Abc_NtkForEachLatch( pNtk, pLatch, i ) @@ -876,6 +884,8 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram return NULL; } return pNtkFrames; +*/ + return NULL; } /**Function************************************************************* @@ -894,6 +904,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram ***********************************************************************/ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vNodes, AddFrameMapping addFrameMapping, void* arg ) { +/* char Buffer[10]; Abc_Obj_t * pNode, * pNodeNew, * pLatch; Abc_Obj_t * pConst1, * pConst1New; @@ -907,7 +918,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec Abc_NtkForEachPi( pNtk, pNode, i ) { pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode ); - Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer ); if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); } // add the internal nodes @@ -925,7 +936,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec { pNodeNew = Abc_NtkDupObj( pNtkFrames, pNode ); Abc_ObjAddFanin( pNodeNew, Abc_ObjChild0Copy(pNode) ); - Abc_NtkLogicStoreNamePlus( pNodeNew, Abc_ObjName(pNode), Buffer ); + Abc_ObjAssignName( pNodeNew, Abc_ObjName(pNode), Buffer ); if (addFrameMapping) addFrameMapping(pNodeNew, pNode, iFrame, arg); } // transfer the implementation of the latch drivers to the latches @@ -953,6 +964,7 @@ void Abc_NtkAddFrame2( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec addFrameMapping(pLatch->pCopy, pLatch, iFrame+1, arg); } } +*/ } @@ -993,12 +1005,12 @@ int Abc_NtkDemiter( Abc_Ntk_t * pNtk ) // add the PO corresponding to control input pPoNew = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pPoNew, pNodeC ); - Abc_NtkLogicStoreName( pPoNew, "addOut1" ); + Abc_ObjAssignName( pPoNew, "addOut1", NULL ); // add the PO corresponding to other input pPoNew = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pPoNew, pNodeB ); - Abc_NtkLogicStoreName( pPoNew, "addOut2" ); + Abc_ObjAssignName( pPoNew, "addOut2", NULL ); // mark the nodes in the first cone pNodeB = Abc_ObjRegular(pNodeB); @@ -1047,7 +1059,7 @@ int Abc_NtkOrPos( Abc_Ntk_t * pNtk ) // create the new PO pNode = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pNode, pMiter ); - Abc_NtkLogicStoreName( pNode, "miter" ); + Abc_ObjAssignName( pNode, "miter", NULL ); // make sure that everything is okay if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index ac46501c..9a88db99 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -84,7 +84,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) ); // add the PIs corresponding to the names Vec_PtrForEachEntry( vNamesPi, pName, i ) - Abc_NtkLogicStoreName( Abc_NtkCreatePi(pNtk), pName ); + Abc_ObjAssignName( Abc_NtkCreatePi(pNtk), pName, NULL ); // create the node pNode = Abc_NtkCreateNode( pNtk ); pNode->pData = Cudd_bddTransfer( dd, pNtk->pManFunc, bFunc ); Cudd_Ref(pNode->pData); @@ -93,7 +93,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo // create the only PO pNodePo = Abc_NtkCreatePo( pNtk ); Abc_ObjAddFanin( pNodePo, pNode ); - Abc_NtkLogicStoreName( pNodePo, pNamePo ); + Abc_ObjAssignName( pNodePo, pNamePo, NULL ); // make the network minimum base Abc_NtkMinimumBase( pNtk ); if ( vNamesPiFake ) @@ -246,7 +246,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly { ProgressBar * pProgress; Vec_Ptr_t * vFuncsGlob; - Abc_Obj_t * pNode, * pFanin; + Abc_Obj_t * pObj, * pFanin; DdNode * bFunc; DdManager * dd; int i, k, Counter; @@ -264,17 +264,17 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly // clean storage for local BDDs Abc_NtkCleanCopy( pNtk ); // set the elementary variables - Abc_NtkForEachCi( pNtk, pNode, i ) - if ( Abc_ObjFanoutNum(pNode) > 0 ) + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) { - pNode->pCopy = (Abc_Obj_t *)dd->vars[i]; + pObj->pCopy = (Abc_Obj_t *)dd->vars[i]; Cudd_Ref( dd->vars[i] ); } // assign the constant node BDD - pNode = Abc_AigConst1(pNtk); - if ( Abc_ObjFanoutNum(pNode) > 0 ) + pObj = Abc_AigConst1(pNtk); + if ( Abc_ObjFanoutNum(pObj) > 0 ) { - pNode->pCopy = (Abc_Obj_t *)dd->one; + pObj->pCopy = (Abc_Obj_t *)dd->one; Cudd_Ref( dd->one ); } @@ -285,9 +285,9 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly { // construct the BDDs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); - Abc_NtkForEachLatch( pNtk, pNode, i ) + Abc_NtkForEachLatchInput( pNtk, pObj, i ) { - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) { if ( fVerbose ) @@ -296,7 +296,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly Cudd_Quit( dd ); return NULL; } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) ); Cudd_Ref( bFunc ); Vec_PtrPush( vFuncsGlob, bFunc ); } Extra_ProgressBarStop( pProgress ); @@ -305,9 +305,9 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly { // construct the BDDs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkNodeNum(pNtk) ); - Abc_NtkForEachCo( pNtk, pNode, i ) + Abc_NtkForEachCo( pNtk, pObj, i ) { - bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax, pProgress, &Counter, fVerbose ); + bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pObj), nBddSizeMax, pProgress, &Counter, fVerbose ); if ( bFunc == NULL ) { if ( fVerbose ) @@ -316,34 +316,35 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly Cudd_Quit( dd ); return NULL; } - bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pNode) ); Cudd_Ref( bFunc ); + bFunc = Cudd_NotCond( bFunc, Abc_ObjFaninC0(pObj) ); Cudd_Ref( bFunc ); Vec_PtrPush( vFuncsGlob, bFunc ); } Extra_ProgressBarStop( pProgress ); } /* // derefence the intermediate BDDs - Abc_NtkForEachNode( pNtk, pNode, i ) - if ( pNode->pCopy ) + Abc_NtkForEachNode( pNtk, pObj, i ) + if ( pObj->pCopy ) { - Cudd_RecursiveDeref( dd, (DdNode *)pNode->pCopy ); - pNode->pCopy = NULL; + Cudd_RecursiveDeref( dd, (DdNode *)pObj->pCopy ); + pObj->pCopy = NULL; } */ /* // make sure all nodes are derefed - Abc_NtkForEachObj( pNtk, pNode, i ) + Abc_NtkForEachObj( pNtk, pObj, i ) { - if ( pNode->pCopy != NULL ) - printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pNode->Id ); - if ( pNode->vFanouts.nSize > 0 ) - printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pNode->Id ); + if ( pObj->pCopy != NULL ) + printf( "Abc_NtkGlobalBdds() error: Node %d has BDD assigned\n", pObj->Id ); + if ( pObj->vFanouts.nSize > 0 ) + printf( "Abc_NtkGlobalBdds() error: Node %d has refs assigned\n", pObj->Id ); } */ // reset references - Abc_NtkForEachObj( pNtk, pNode, i ) - Abc_ObjForEachFanin( pNode, pFanin, k ) - pFanin->vFanouts.nSize++; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + pFanin->vFanouts.nSize++; // reorder one more time if ( fReorder ) diff --git a/src/base/abci/abcOrder.c b/src/base/abci/abcOrder.c index c9ebdc12..04417f77 100644 --- a/src/base/abci/abcOrder.c +++ b/src/base/abci/abcOrder.c @@ -70,7 +70,7 @@ void Abc_NtkImplementCiOrder( Abc_Ntk_t * pNtk, char * pFileName, int fReverse, vSupp = Vec_PtrAlloc( Abc_NtkCiNum(pNtk) ); while ( fscanf( pFile, "%s", Buffer ) == 1 ) { - pObj = Abc_NtkFindTerm( pNtk, Buffer ); + pObj = Abc_NtkFindCi( pNtk, Buffer ); if ( pObj == NULL || !Abc_ObjIsCi(pObj) ) { printf( "Name \"%s\" is not a PI name. Cannot use this order.\n", Buffer ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e3bb764d..81059a0f 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -247,7 +247,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) assert( Init < 4 ); InitNums[Init]++; - pFanin = Abc_ObjFanin0(pLatch); + pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) ) continue; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 9fcc6979..61be3dee 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -147,9 +147,9 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd if ( fUpdateLevel ) Abc_NtkStartReverseLevels( pNtk ); - if ( Abc_NtkLatchNum(pNtk) ) - Abc_NtkForEachLatch(pNtk, pNode, i) - pNode->pNext = pNode->pData; +// if ( Abc_NtkLatchNum(pNtk) ) +// Abc_NtkForEachLatch(pNtk, pNode, i) +// pNode->pNext = pNode->pData; // resynthesize each node once nNodes = Abc_NtkObjNumMax(pNtk); @@ -221,9 +221,9 @@ pManRes->timeTotal = clock() - clkStart; Abc_NtkForEachObj( pNtk, pNode, i ) pNode->pData = NULL; - if ( Abc_NtkLatchNum(pNtk) ) - Abc_NtkForEachLatch(pNtk, pNode, i) - pNode->pData = pNode->pNext, pNode->pNext = NULL; +// if ( Abc_NtkLatchNum(pNtk) ) +// Abc_NtkForEachLatch(pNtk, pNode, i) +// pNode->pData = pNode->pNext, pNode->pNext = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); diff --git a/src/base/abci/abcRr.c b/src/base/abci/abcRr.c index 03073075..63beac6c 100644 --- a/src/base/abci/abcRr.c +++ b/src/base/abci/abcRr.c @@ -106,8 +106,8 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa p->nNodesOld = Abc_NtkNodeNum(pNtk); p->nLevelsOld = Abc_AigGetLevelNum(pNtk); // remember latch values - Abc_NtkForEachLatch( pNtk, pNode, i ) - pNode->pNext = pNode->pData; +// Abc_NtkForEachLatch( pNtk, pNode, i ) +// pNode->pNext = pNode->pData; // go through the nodes Abc_NtkCleanCopy(pNtk); nNodes = Abc_NtkObjNumMax(pNtk); @@ -216,8 +216,8 @@ int Abc_NtkRR( Abc_Ntk_t * pNtk, int nFaninLevels, int nFanoutLevels, int fUseFa Abc_RRManPrintStats( p ); Abc_RRManStop( p ); // restore latch values - Abc_NtkForEachLatch( pNtk, pNode, i ) - pNode->pData = pNode->pNext, pNode->pNext = NULL; +// Abc_NtkForEachLatch( pNtk, pNode, i ) +// pNode->pData = pNode->pNext, pNode->pNext = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); Abc_NtkGetLevelNum( pNtk ); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index c54ea33c..d00be668 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -327,7 +327,7 @@ Abc_Ntk_t * Abc_NtkTopmost( Abc_Ntk_t * pNtk, int nLevels ) pPoNew = Abc_NtkCreatePo(pNtkNew); Abc_ObjAddFanin( pPoNew, pObjNew ); Abc_NtkAddDummyPiNames( pNtkNew ); - Abc_NtkLogicStoreName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)) ); + Abc_ObjAssignName( pPoNew, Abc_ObjName(Abc_NtkPo(pNtk, 0)), NULL ); // make sure everything is okay if ( !Abc_NtkCheck( pNtkNew ) ) { diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 8f1ab180..7c6df88a 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -59,11 +59,31 @@ bool Abc_NtkFraigSweep( Abc_Ntk_t * pNtk, int fUseInv, int fExdc, int fVerbose ) Abc_Ntk_t * pNtkAig; Fraig_Man_t * pMan; stmm_table * tEquiv; + Abc_Obj_t * pObj; + int i, fUseTrick; assert( !Abc_NtkIsStrash(pNtk) ); + // save gate assignments + fUseTrick = 0; + if ( Abc_NtkIsMappedLogic(pNtk) ) + { + fUseTrick = 1; + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pNext = pObj->pData; + } // derive the AIG pNtkAig = Abc_NtkStrash( pNtk, 0, 1 ); + // reconstruct gate assignments + if ( fUseTrick ) + { + extern void * Abc_FrameReadLibGen(); + Aig_ManStop( pNtk->pManFunc ); + pNtk->pManFunc = Abc_FrameReadLibGen(); + pNtk->ntkFunc = ABC_FUNC_MAP; + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pData = pObj->pNext, pObj->pNext = NULL; + } // perform fraiging of the AIG Fraig_ParamsSetDefault( &Params ); @@ -176,8 +196,8 @@ stmm_table * Abc_NtkFraigEquiv( Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ) // skip the dangling nodes if ( pNodeAig == NULL ) continue; - // skip the nodes that fanout into POs - if ( Abc_NodeHasUniqueCoFanout(pNode) ) + // skip the nodes that fanout into COs + if ( Abc_NodeHasCoFanout(pNode) ) continue; // get the FRAIG node gNode = Fraig_NotCond( Abc_ObjRegular(pNodeAig)->pCopy, Abc_ObjIsComplement(pNodeAig) ); diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index 5add0dda..8364b783 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -254,9 +254,9 @@ void Abc_NtkTimeInitialize( Abc_Ntk_t * pNtk ) continue; *pTime = pNtk->pManTime->tReqDef; } - // set the 0 arrival times for latches and constant nodes + // set the 0 arrival times for latch outputs and constant nodes ppTimes = (Abc_Time_t **)pNtk->pManTime->vArrs->pArray; - Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkForEachLatchOutput( pNtk, pObj, i ) { pTime = ppTimes[pObj->Id]; pTime->Fall = pTime->Rise = pTime->Worst = 0.0; diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 156d9b3d..cced1c47 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -278,6 +278,7 @@ DdNode * Abc_NtkComputeUnreachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * b ***********************************************************************/ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUnreach ) { +/* Abc_Ntk_t * pNtkNew; Abc_Obj_t * pNode, * pNodeNew; int * pPermute; @@ -290,7 +291,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // create PIs corresponding to LOs Abc_NtkForEachLatch( pNtk, pNode, i ) - Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode) ); + Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pNode), NULL ); // cannot ADD POs here because pLatch->pCopy point to the PIs // create a new node @@ -313,9 +314,9 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // for each CO, create PO (skip POs equal to CIs because of name conflict) Abc_NtkForEachPo( pNtk, pNode, i ) if ( !Abc_ObjIsCi(Abc_ObjFanin0(pNode)) ) - Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode) ); + Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pNode), NULL ); Abc_NtkForEachLatch( pNtk, pNode, i ) - Abc_NtkLogicStoreName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in") ); + Abc_ObjAssignName( pNode->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pNode, "_in"), NULL ); // link to the POs of the network Abc_NtkForEachPo( pNtk, pNode, i ) @@ -337,6 +338,8 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn return NULL; } return pNtkNew; +*/ + return NULL; } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c deleted file mode 100644 index 50baa285..00000000 --- a/src/base/abci/abcVanEijk.c +++ /dev/null @@ -1,824 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcVanEijk.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Implementation of van Eijk's method for finding - signal correspondence: C. A. J. van Eijk. "Sequential equivalence - checking based on structural similarities", IEEE Trans. CAD, - vol. 19(7), July 2000, pp. 814-819.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - October 2, 2005.] - - Revision [$Id: abcVanEijk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "fraig.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); -static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames ); -static Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ); -static int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ); -static void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ); -static int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ); -static void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ); - -extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); -extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); -extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); - -static Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ); - -//////////////////////////////////////////////////////////////////////// -/// INLINED FUNCTIONS /// -//////////////////////////////////////////////////////////////////////// - -// sets the correspondence of the node in the frame -static inline void Abc_NodeVanEijkWriteCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame, Abc_Obj_t * pEntry ) -{ - Vec_PtrWriteEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id, pEntry ); -} -// returns the correspondence of the node in the frame -static inline Abc_Obj_t * Abc_NodeVanEijkReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) -{ - return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); -} -// returns the hash value of the node in the frame -static inline Abc_Obj_t * Abc_NodeVanEijkHash( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) -{ - return Abc_ObjRegular( Abc_NodeVanEijkReadCorresp(pNode, vCorresp, iFrame)->pCopy ); -} -// returns the representative node of the class to which the node belongs -static inline Abc_Obj_t * Abc_NodeVanEijkRepr( Abc_Obj_t * pNode ) -{ - if ( pNode->pNext == NULL ) - return NULL; - while ( pNode->pNext ) - pNode = pNode->pNext; - return pNode; -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives classes of sequentially equivalent nodes.] - - Description [Performs sequential sweep by combining the equivalent - nodes. Adds EXDC network to the current network to record the subset - of unreachable states computed by identifying the equivalent nodes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijk( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) -{ - Fraig_Params_t Params; - Abc_Ntk_t * pNtkSingle; - Vec_Ptr_t * vClasses; - Abc_Ntk_t * pNtkNew; - - assert( Abc_NtkIsStrash(pNtk) ); - - // FRAIG the network to get rid of combinational equivalences - Fraig_ParamsSetDefaultFull( &Params ); - pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - Abc_AigSetNodePhases( pNtkSingle ); - Abc_NtkCleanNext(pNtkSingle); - - // get the equivalence classes - vClasses = Abc_NtkVanEijkClasses( pNtkSingle, nFrames, fVerbose ); - if ( Vec_PtrSize(vClasses) > 0 ) - { - // transform the network by merging nodes in the equivalence classes - pNtkNew = Abc_NtkVanEijkFrames( pNtkSingle, NULL, 1, 0, 1 ); -// pNtkNew = Abc_NtkDup( pNtkSingle ); - // derive the EXDC network if asked - if ( fExdc ) - pNtkNew->pExdc = Abc_NtkVanEijkDeriveExdc( pNtkSingle, vClasses ); - } - else - pNtkNew = Abc_NtkDup( pNtkSingle ); - Abc_NtkVanEijkClassesTest( pNtkSingle, vClasses ); - Vec_PtrFree( vClasses ); - - Abc_NtkDelete( pNtkSingle ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Derives the classes of sequentially equivalent nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkClasses( Abc_Ntk_t * pNtkSingle, int nFrames, int fVerbose ) -{ - Fraig_Man_t * pFraig; - Abc_Ntk_t * pNtkMulti; - Vec_Ptr_t * vCorresp, * vClasses; - int nIter, RetValue; - int nAddFrames = 0; - - if ( fVerbose ) - printf( "The number of ANDs after FRAIGing = %d.\n", Abc_NtkNodeNum(pNtkSingle) ); - - // get the AIG of the base case - vCorresp = Vec_PtrAlloc( 100 ); - pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames + nAddFrames, 0, 0 ); - if ( fVerbose ) - printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + nAddFrames, Abc_NtkNodeNum(pNtkMulti) ); - - // FRAIG the initialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) - pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 1 ); - Fraig_ManFree( pFraig ); - - // find initial equivalence classes - vClasses = Abc_NtkVanEijkClassesDeriveBase( pNtkSingle, vCorresp, nFrames + nAddFrames ); - if ( fVerbose ) - printf( "The number of classes in the base case = %5d. Pairs = %8d.\n", Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); - Abc_NtkDelete( pNtkMulti ); - - // refine the classes using iterative FRAIGing - for ( nIter = 1; Vec_PtrSize(vClasses) > 0; nIter++ ) - { - // derive the network with equivalence classes - Abc_NtkVanEijkClassesOrder( vClasses ); - pNtkMulti = Abc_NtkVanEijkFrames( pNtkSingle, vCorresp, nFrames, 1, 0 ); - // simulate with classes (TO DO) - - // FRAIG the unitialized frames (labels the nodes of pNtkMulti with FRAIG nodes to be used as hash keys) - pFraig = Abc_NtkVanEijkFraig( pNtkMulti, 0 ); - Fraig_ManFree( pFraig ); - - // refine the classes - RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, nFrames, vClasses ); - Abc_NtkDelete( pNtkMulti ); - if ( fVerbose ) - printf( "The number of classes after %2d iterations = %5d. Pairs = %8d.\n", nIter, Vec_PtrSize(vClasses), Abc_NtkVanEijkClassesCountPairs(vClasses) ); - // quit if there is no change - if ( RetValue == 0 ) - break; - } - Vec_PtrFree( vCorresp ); - - if ( fVerbose ) - { - Abc_Obj_t * pObj, * pClass; - int i, Counter; - printf( "The classes are: " ); - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - Counter = 0; - for ( pObj = pClass; pObj; pObj = pObj->pNext ) - Counter++; - printf( " %d", Counter ); -/* - printf( " = {" ); - for ( pObj = pClass; pObj; pObj = pObj->pNext ) - printf( " %d", pObj->Id ); - printf( " } " ); -*/ - } - printf( "\n" ); - } - return vClasses; -} - -/**Function************************************************************* - - Synopsis [Computes the equivalence classes of nodes using the base case.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveBase( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vCorresp, int nFrames ) -{ - Vec_Ptr_t * vClasses; - int i, RetValue; - // derive the classes for the last frame - vClasses = Abc_NtkVanEijkClassesDeriveFirst( pNtkSingle, vCorresp, nFrames - 1 ); - // refine the classes using other timeframes - for ( i = 0; i < nFrames - 1; i++ ) - { - if ( Vec_PtrSize(vClasses) == 0 ) - break; - RetValue = Abc_NtkVanEijkClassesRefine( pNtkSingle, vCorresp, i, vClasses ); -// if ( RetValue ) -// printf( " yes%s", (i==nFrames-2 ? "\n":"") ); -// else -// printf( " no%s", (i==nFrames-2 ? "\n":"") ); - } - return vClasses; -} - - -/**Function************************************************************* - - Synopsis [Computes the equivalence classes of nodes.] - - Description [Original network (pNtk) is mapped into the unfolded frames - using given array of nodes (vCorresp). Each node in the unfolded frames - is mapped into a FRAIG node (pNode->pCopy). This procedure uses next - pointers (pNode->pNext) to combine the nodes into equivalence classes. - Each class is represented by its representative node with the minimum level. - Only the last frame is considered.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkClassesDeriveFirst( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame ) -{ - Abc_Obj_t * pNode, * pKey, ** ppSlot; - stmm_table * tTable; - stmm_generator * gen; - Vec_Ptr_t * vClasses; - int i; - // start the table hashing FRAIG nodes into classes of original network nodes - tTable = stmm_init_table( st_ptrcmp, st_ptrhash ); - // create the table - Abc_NtkCleanNext( pNtk ); - Abc_NtkForEachObj( pNtk, pNode, i ) - { - if ( Abc_ObjIsPo(pNode) ) - continue; - pKey = Abc_NodeVanEijkHash( pNode, vCorresp, iFrame ); - if ( !stmm_find_or_add( tTable, (char *)pKey, (char ***)&ppSlot ) ) - *ppSlot = NULL; - pNode->pNext = *ppSlot; - *ppSlot = pNode; - } - // collect only non-trivial classes - vClasses = Vec_PtrAlloc( 100 ); - stmm_foreach_item( tTable, gen, (char **)&pKey, (char **)&pNode ) - if ( pNode->pNext ) - Vec_PtrPush( vClasses, pNode ); - stmm_free_table( tTable ); - return vClasses; -} - -/**Function************************************************************* - - Synopsis [Refines the classes using one frame.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkVanEijkClassesRefine( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int iFrame, Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pHeadSame, ** ppTailSame; - Abc_Obj_t * pHeadDiff, ** ppTailDiff; - Abc_Obj_t * pNode, * pClass, * pKey; - int i, k, fChange = 0; - Vec_PtrForEachEntry( vClasses, pClass, i ) - { -// assert( pClass->pNext ); - pKey = Abc_NodeVanEijkHash( pClass, vCorresp, iFrame ); - for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) - if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) - break; - if ( pNode == NULL ) - continue; - fChange = 1; - // create two classes - pHeadSame = NULL; ppTailSame = &pHeadSame; - pHeadDiff = NULL; ppTailDiff = &pHeadDiff; - for ( pNode = pClass; pNode; pNode = pNode->pNext ) - if ( Abc_NodeVanEijkHash(pNode, vCorresp, iFrame) != pKey ) - *ppTailDiff = pNode, ppTailDiff = &pNode->pNext; - else - *ppTailSame = pNode, ppTailSame = &pNode->pNext; - *ppTailSame = NULL; - *ppTailDiff = NULL; - assert( pHeadSame && pHeadDiff ); - // put the updated class back - Vec_PtrWriteEntry( vClasses, i, pHeadSame ); - // append the new class to be processed later - Vec_PtrPush( vClasses, pHeadDiff ); - } - // remove trivial classes - k = 0; - Vec_PtrForEachEntry( vClasses, pClass, i ) - if ( pClass->pNext ) - Vec_PtrWriteEntry( vClasses, k++, pClass ); - Vec_PtrShrink( vClasses, k ); - return fChange; -} - -/**Function************************************************************* - - Synopsis [Orders nodes in the equivalence classes.] - - Description [Finds a min-level representative of each class and puts it last.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkClassesOrder( Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pClass, * pNode, * pPrev, * pNodeMin, * pPrevMin; - int i; - // go through the classes - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - assert( pClass->pNext ); - pPrevMin = NULL; - pNodeMin = pClass; - for ( pPrev = pClass, pNode = pClass->pNext; pNode; pPrev = pNode, pNode = pNode->pNext ) - if ( pNodeMin->Level >= pNode->Level ) - { - pPrevMin = pPrev; - pNodeMin = pNode; - } - if ( pNodeMin->pNext == NULL ) // already last - continue; - // update the class - if ( pNodeMin == pClass ) - Vec_PtrWriteEntry( vClasses, i, pNodeMin->pNext ); - else - pPrevMin->pNext = pNodeMin->pNext; - // attach the min node - assert( pPrev->pNext == NULL ); - pPrev->pNext = pNodeMin; - pNodeMin->pNext = NULL; - } - Vec_PtrForEachEntry( vClasses, pClass, i ) - assert( pClass->pNext ); -} - -/**Function************************************************************* - - Synopsis [Counts pairs of equivalent nodes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkVanEijkClassesCountPairs( Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pClass, * pNode; - int i, nPairs = 0; - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - assert( pClass->pNext ); - for ( pNode = pClass->pNext; pNode; pNode = pNode->pNext ) - nPairs++; - } - return nPairs; -} - -/**Function************************************************************* - - Synopsis [Sanity check for the class representation.] - - Description [Checks that pNode->pNext is only used in the classes.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkClassesTest( Abc_Ntk_t * pNtkSingle, Vec_Ptr_t * vClasses ) -{ - Abc_Obj_t * pClass, * pObj; - int i; - Abc_NtkCleanCopy( pNtkSingle ); - Vec_PtrForEachEntry( vClasses, pClass, i ) - for ( pObj = pClass; pObj; pObj = pObj->pNext ) - if ( pObj->pNext ) - pObj->pCopy = (Abc_Obj_t *)1; - Abc_NtkForEachObj( pNtkSingle, pObj, i ) - assert( (pObj->pCopy != NULL) == (pObj->pNext != NULL) ); - Abc_NtkCleanCopy( pNtkSingle ); -} - - -/**Function************************************************************* - - Synopsis [Performs DFS for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) -{ - Abc_Obj_t * pRepr; - // skip CI and const - if ( Abc_ObjFaninNum(pNode) < 2 ) - return; - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - return; - // mark the node as visited - Abc_NodeSetTravIdCurrent( pNode ); - assert( Abc_ObjIsNode( pNode ) ); - // check if the node belongs to the class - if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) - Abc_NtkVanEijkDfs_rec( pRepr, vNodes ); - else - { - Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pNode), vNodes ); - Abc_NtkVanEijkDfs_rec( Abc_ObjFanin1(pNode), vNodes ); - } - // add the node after the fanins have been added - Vec_PtrPush( vNodes, pNode ); -} - -/**Function************************************************************* - - Synopsis [Finds DFS ordering of nodes using equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanEijkDfs( Abc_Ntk_t * pNtk ) -{ - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i; - vNodes = Vec_PtrAlloc( 100 ); - Abc_NtkIncrementTravId( pNtk ); - Abc_NtkForEachCo( pNtk, pObj, i ) - Abc_NtkVanEijkDfs_rec( Abc_ObjFanin0(pObj), vNodes ); - return vNodes; -} - - -/**Function************************************************************* - - Synopsis [Derives the timeframes of the network.] - - Description [Returns mapping of the orig nodes into the frame nodes (vCorresp).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ) -{ - char Buffer[100]; - Abc_Ntk_t * pNtkFrames; - Abc_Obj_t * pLatch, * pLatchNew; - Vec_Ptr_t * vOrder; - int i; - assert( nFrames > 0 ); - assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkIsDfsOrdered(pNtk) ); - // clean the array of connections - if ( vCorresp ) - Vec_PtrFill( vCorresp, (nFrames + fAddLast)*Abc_NtkObjNumMax(pNtk), NULL ); - // start the new network - pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 ); - if ( fShortNames ) - { - pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName); - pNtkFrames->pSpec = Extra_UtilStrsav(pNtk->pSpec); - } - else - { - sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast ); - pNtkFrames->pName = Extra_UtilStrsav(Buffer); - } - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); - // create new latches and remember them in the new latches - Abc_NtkForEachLatch( pNtk, pLatch, i ) - Abc_NtkDupObj( pNtkFrames, pLatch ); - // collect nodes in such a way each class representative goes first - vOrder = Abc_NtkVanEijkDfs( pNtk ); - // create the timeframes - for ( i = 0; i < nFrames; i++ ) - Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, i, vCorresp, vOrder, fShortNames ); - Vec_PtrFree( vOrder ); - // add one more timeframe without class info - if ( fAddLast ) - Abc_NtkVanEijkAddFrame( pNtkFrames, pNtk, nFrames, vCorresp, NULL, fShortNames ); - // connect the new latches to the outputs of the last frame - Abc_NtkForEachLatch( pNtk, pLatch, i ) - { - pLatchNew = Abc_NtkLatch(pNtkFrames, i); - Abc_ObjAddFanin( pLatchNew, pLatch->pCopy ); - Abc_NtkLogicStoreName( pLatchNew, Abc_ObjName(pLatch) ); - pLatch->pNext = NULL; - } - // remove dangling nodes -// Abc_AigCleanup( pNtkFrames->pManFunc ); - // otherwise some external nodes may have dandling pointers - - // make sure that everything is okay - if ( !Abc_NtkCheck( pNtkFrames ) ) - printf( "Abc_NtkVanEijkFrames: The network check has failed.\n" ); - return pNtkFrames; -} - -/**Function************************************************************* - - Synopsis [Adds one time frame to the new network.] - - Description [If the ordering of nodes is given, uses it. Otherwise, - uses the DSF order of the nodes in the network.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ) -{ - char Buffer[10]; - Abc_Obj_t * pNode, * pLatch, * pRepr; - Vec_Ptr_t * vTemp; - int i; - // create the prefix to be added to the node names - sprintf( Buffer, "_%02d", iFrame ); - // add the new PI nodes - Abc_NtkForEachPi( pNtk, pNode, i ) - { - pNode->pCopy = Abc_NtkCreatePi(pNtkFrames); - if ( fShortNames ) - Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); - else - Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); - } - // remember the CI mapping - if ( vCorresp ) - { - pNode = Abc_AigConst1(pNtk); - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - Abc_NtkForEachCi( pNtk, pNode, i ) - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - } - // go through the nodes in the given order or in the natural order - if ( vOrder ) - { - // add the internal nodes - Vec_PtrForEachEntry( vOrder, pNode, i ) - { - if ( pRepr = Abc_NodeVanEijkRepr(pNode) ) - pNode->pCopy = Abc_ObjNotCond( pRepr->pCopy, pNode->fPhase ^ pRepr->fPhase ); - else - pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); - assert( Abc_ObjRegular(pNode->pCopy) != NULL ); - if ( vCorresp ) - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - } - } - else - { - // add the internal nodes - Abc_AigForEachAnd( pNtk, pNode, i ) - { - pNode->pCopy = Abc_AigAnd( pNtkFrames->pManFunc, Abc_ObjChild0Copy(pNode), Abc_ObjChild1Copy(pNode) ); - assert( Abc_ObjRegular(pNode->pCopy) != NULL ); - if ( vCorresp ) - Abc_NodeVanEijkWriteCorresp( pNode, vCorresp, iFrame, Abc_ObjRegular(pNode->pCopy) ); - } - } - // add the new POs - Abc_NtkForEachPo( pNtk, pNode, i ) - { - pNode->pCopy = Abc_NtkCreatePo(pNtkFrames); - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjChild0Copy(pNode) ); - if ( fShortNames ) - Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); - else - Abc_NtkLogicStoreNamePlus( pNode->pCopy, Abc_ObjName(pNode), Buffer ); - } - // transfer the implementation of the latch drivers to the latches - vTemp = Vec_PtrAlloc( 100 ); - Abc_NtkForEachLatch( pNtk, pLatch, i ) - Vec_PtrPush( vTemp, Abc_ObjChild0Copy(pLatch) ); - Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pCopy = Vec_PtrEntry( vTemp, i ); - Vec_PtrFree( vTemp ); - - Abc_AigForEachAnd( pNtk, pNode, i ) - pNode->pCopy = NULL; -} - -/**Function************************************************************* - - Synopsis [Fraigs the network with or without initialization.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ) -{ - Fraig_Man_t * pMan; - Fraig_Params_t Params; - ProgressBar * pProgress; - Abc_Obj_t * pNode; - int i; - assert( Abc_NtkIsStrash(pMulti) ); - // create the FRAIG manager - Fraig_ParamsSetDefaultFull( &Params ); - pMan = Fraig_ManCreate( &Params ); - // clean the copy fields in the old network - Abc_NtkCleanCopy( pMulti ); - // map the constant nodes - Abc_AigConst1(pMulti)->pCopy = (Abc_Obj_t *)Fraig_ManReadConst1(pMan); - if ( fInit ) - { - // map the PI nodes - Abc_NtkForEachPi( pMulti, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); - // map the latches - Abc_NtkForEachLatch( pMulti, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fraig_NotCond( Fraig_ManReadConst1(pMan), !Abc_LatchIsInit1(pNode) ); - } - else - { - // map the CI nodes - Abc_NtkForEachCi( pMulti, pNode, i ) - pNode->pCopy = (Abc_Obj_t *)Fraig_ManReadIthVar(pMan, i); - } - // perform fraiging - pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pMulti) ); - Abc_AigForEachAnd( pMulti, pNode, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNode->pCopy = (Abc_Obj_t *)Fraig_NodeAnd( pMan, - Fraig_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) ), - Fraig_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) ) ); - } - Extra_ProgressBarStop( pProgress ); - return pMan; -} - - -/**Function************************************************************* - - Synopsis [Create EXDC from the equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;//, *pObjNew; - Abc_Obj_t * pMiter, * pTotal; - Vec_Ptr_t * vCone; - int i, k; - - assert( Abc_NtkIsStrash(pNtk) ); - - // start the network - pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); - pNtkNew->pName = Extra_UtilStrsav("exdc"); - pNtkNew->pSpec = NULL; - - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // for each CI, create PI - Abc_NtkForEachCi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); - // cannot add latches here because pLatch->pCopy pointers are used - - // create the cones for each pair of nodes in an equivalence class - pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - Vec_PtrForEachEntry( vClasses, pClass, i ) - { - assert( pClass->pNext ); - // get the cone for the representative node - pRepr = Abc_NodeVanEijkRepr( pClass ); - if ( Abc_ObjFaninNum(pRepr) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pRepr, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pRepr ); - } - // go through the node pairs (representative is last in the list) - for ( pNode = pClass; pNode != pRepr; pNode = pNode->pNext ) - { - // get the cone for the node - assert( Abc_ObjFaninNum(pNode) == 2 ); - vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode ); - // complement if there is phase difference - pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ^ pRepr->fPhase ); - // add the miter - pMiter = Abc_AigXor( pNtkNew->pManFunc, pRepr->pCopy, pNode->pCopy ); - } - // add the miter to the final - pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); - } - -/* - // create the only PO - pObjNew = Abc_NtkCreatePo( pNtkNew ); - // add the PO name - Abc_NtkLogicStoreName( pObjNew, "DC" ); - // add the PO - Abc_ObjAddFanin( pObjNew, pTotal ); - - // quontify the PIs existentially - pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); - - // get the new PO - pObjNew = Abc_NtkPo( pNtkNew, 0 ); - // remember the miter output - pTotal = Abc_ObjChild0( pObjNew ); - // remove the PO - Abc_NtkDeleteObj( pObjNew ); - - // make the old network point to the new things - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pCopy = Abc_NtkPi( pNtkNew, i ); -*/ - - // for each CO, create PO (skip POs equal to CIs because of name conflict) - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix( pObj, "_in") ); - - // link to the POs of the network - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - - // remove the extra nodes - Abc_AigCleanup( pNtkNew->pManFunc ); - - // check the result - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkVanEijkDeriveExdc: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c deleted file mode 100644 index 339d64d1..00000000 --- a/src/base/abci/abcVanImp.c +++ /dev/null @@ -1,1002 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcVanImp.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Implementation of van Eijk's method for implications.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - October 2, 2005.] - - Revision [$Id: abcVanImp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "fraig.h" -#include "sim.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Van_Man_t_ Van_Man_t; -struct Van_Man_t_ -{ - // single frame representation - Abc_Ntk_t * pNtkSingle; // single frame - Vec_Int_t * vCounters; // the counters of 1s in the simulation info - Vec_Ptr_t * vZeros; // the set of constant 0 candidates - Vec_Int_t * vImps; // the set of all implications - Vec_Int_t * vImpsMis; // the minimum independent set of implications - // multiple frame representation - Abc_Ntk_t * pNtkMulti; // multiple frame - Vec_Ptr_t * vCorresp; // the correspondence between single frame and multiple frames - // parameters - int nFrames; // the number of timeframes - int nWords; // the number of simulation words - int nIdMax; // the maximum ID in the single frame - int fVerbose; // the verbosiness flag - // statistics - int nPairsAll; - int nImpsAll; - int nEquals; - int nZeros; - // runtime - int timeAll; - int timeSim; - int timeAdd; - int timeCheck; - int timeInfo; - int timeMis; -}; - -static void Abc_NtkVanImpCompute( Van_Man_t * p ); -static Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ); -static void Abc_NtkVanImpComputeAll( Van_Man_t * p ); -static Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ); -static void Abc_NtkVanImpManFree( Van_Man_t * p ); -static void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); -static int Abc_NtkVanImpCountEqual( Van_Man_t * p ); - -static Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ); - -extern Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nFrames, int fAddLast, int fShortNames ); -extern void Abc_NtkVanEijkAddFrame( Abc_Ntk_t * pNtkFrames, Abc_Ntk_t * pNtk, int iFrame, Vec_Ptr_t * vCorresp, Vec_Ptr_t * vOrder, int fShortNames ); -extern Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit ); - -//////////////////////////////////////////////////////////////////////// -/// INLINED FUNCTIONS /// -//////////////////////////////////////////////////////////////////////// - -// returns the correspondence of the node in the frame -static inline Abc_Obj_t * Abc_NodeVanImpReadCorresp( Abc_Obj_t * pNode, Vec_Ptr_t * vCorresp, int iFrame ) -{ - return Vec_PtrEntry( vCorresp, iFrame * Abc_NtkObjNumMax(pNode->pNtk) + pNode->Id ); -} -// returns the left node of the implication -static inline Abc_Obj_t * Abc_NodeVanGetLeft( Abc_Ntk_t * pNtk, unsigned Imp ) -{ - return Abc_NtkObj( pNtk, Imp >> 16 ); -} -// returns the right node of the implication -static inline Abc_Obj_t * Abc_NodeVanGetRight( Abc_Ntk_t * pNtk, unsigned Imp ) -{ - return Abc_NtkObj( pNtk, Imp & 0xFFFF ); -} -// returns the implication -static inline unsigned Abc_NodeVanGetImp( Abc_Obj_t * pLeft, Abc_Obj_t * pRight ) -{ - return (pLeft->Id << 16) | pRight->Id; -} -// returns the right node of the implication -static inline void Abc_NodeVanPrintImp( unsigned Imp ) -{ - printf( "%d -> %d ", Imp >> 16, Imp & 0xFFFF ); -} - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derives implications that hold sequentially.] - - Description [Adds EXDC network to the current network to record the - set of computed sequentially equivalence implications, representing - a subset of unreachable states.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanImp( Abc_Ntk_t * pNtk, int nFrames, int fExdc, int fVerbose ) -{ - Fraig_Params_t Params; - Abc_Ntk_t * pNtkNew; - Van_Man_t * p; - - assert( Abc_NtkIsStrash(pNtk) ); - - // start the manager - p = ALLOC( Van_Man_t, 1 ); - memset( p, 0, sizeof(Van_Man_t) ); - p->nFrames = nFrames; - p->fVerbose = fVerbose; - p->vCorresp = Vec_PtrAlloc( 100 ); - - // FRAIG the network to get rid of combinational equivalences - Fraig_ParamsSetDefaultFull( &Params ); - p->pNtkSingle = Abc_NtkFraig( pNtk, &Params, 0, 0 ); - p->nIdMax = Abc_NtkObjNumMax( p->pNtkSingle ); - Abc_AigSetNodePhases( p->pNtkSingle ); - Abc_NtkCleanNext( p->pNtkSingle ); -// if ( fVerbose ) -// printf( "The number of ANDs in 1 timeframe = %d.\n", Abc_NtkNodeNum(p->pNtkSingle) ); - - // derive multiple time-frames and node correspondence (to be used in the inductive case) - p->pNtkMulti = Abc_NtkVanEijkFrames( p->pNtkSingle, p->vCorresp, nFrames, 1, 0 ); -// if ( fVerbose ) -// printf( "The number of ANDs in %d timeframes = %d.\n", nFrames + 1, Abc_NtkNodeNum(p->pNtkMulti) ); - - // get the implications - Abc_NtkVanImpCompute( p ); - - // create the new network with EXDC correspondingn to the computed implications - if ( fExdc && (Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImpsMis) > 0) ) - { - if ( p->pNtkSingle->pExdc ) - { - printf( "The old EXDC network is thrown away.\n" ); - Abc_NtkDelete( p->pNtkSingle->pExdc ); - p->pNtkSingle->pExdc = NULL; - } - pNtkNew = Abc_NtkDup( p->pNtkSingle ); - pNtkNew->pExdc = Abc_NtkVanImpDeriveExdc( p->pNtkSingle, p->vZeros, p->vImpsMis ); - } - else - pNtkNew = Abc_NtkDup( p->pNtkSingle ); - - // free stuff - Abc_NtkVanImpManFree( p ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Frees the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpManFree( Van_Man_t * p ) -{ - Abc_NtkDelete( p->pNtkMulti ); - Abc_NtkDelete( p->pNtkSingle ); - Vec_PtrFree( p->vCorresp ); - Vec_PtrFree( p->vZeros ); - Vec_IntFree( p->vCounters ); - Vec_IntFree( p->vImpsMis ); - Vec_IntFree( p->vImps ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Derives the minimum independent set of sequential implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpCompute( Van_Man_t * p ) -{ - Fraig_Man_t * pFraig; - Vec_Ptr_t * vZeros; - Vec_Int_t * vImps, * vImpsTemp; - int nIters, clk; - - // compute all implications and count 1s in the simulation info -clk = clock(); - Abc_NtkVanImpComputeAll( p ); -p->timeAll += clock() - clk; - - // compute the MIS -clk = clock(); - p->vImpsMis = Abc_NtkVanImpComputeMis( p ); -p->timeMis += clock() - clk; - - if ( p->fVerbose ) - { - printf( "Pairs = %8d. Imps = %8d. Seq = %7d. MIS = %7d. Equ = %5d. Const = %5d.\n", - p->nPairsAll, p->nImpsAll, Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), p->nEquals, p->nZeros ); - PRT( "Visiting all nodes pairs while preparing for the inductive case", p->timeAll ); - printf( "Start : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); - } - - // iterate to perform the iterative filtering of implications - for ( nIters = 1; Vec_PtrSize(p->vZeros) > 0 || Vec_IntSize(p->vImps) > 0; nIters++ ) - { - // FRAIG the ununitialized frames - pFraig = Abc_NtkVanEijkFraig( p->pNtkMulti, 0 ); - - // assuming that zeros and imps hold in the first k-1 frames - // check if they hold in the k-th frame - vZeros = Vec_PtrAlloc( 100 ); - vImps = Vec_IntAlloc( 100 ); - Abc_NtkVanImpFilter( p, pFraig, vZeros, vImps ); - Fraig_ManFree( pFraig ); - -clk = clock(); - vImpsTemp = p->vImps; - p->vImps = vImps; - Vec_IntFree( p->vImpsMis ); - p->vImpsMis = Abc_NtkVanImpComputeMis( p ); - p->vImps = vImpsTemp; -p->timeMis += clock() - clk; - - // report the results - if ( p->fVerbose ) - printf( "Iter = %2d: Seq = %7d. MIS = %7d. Const = %5d.\n", nIters, Vec_IntSize(vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(vZeros) ); - - // if the fixed point is reaches, quit the loop - if ( Vec_PtrSize(vZeros) == Vec_PtrSize(p->vZeros) && Vec_IntSize(vImps) == Vec_IntSize(p->vImps) ) - { // no change - Vec_PtrFree(vZeros); - Vec_IntFree(vImps); - break; - } - - // update the sets - Vec_PtrFree( p->vZeros ); p->vZeros = vZeros; - Vec_IntFree( p->vImps ); p->vImps = vImps; - } - - // compute the MIS -clk = clock(); - Vec_IntFree( p->vImpsMis ); - p->vImpsMis = Abc_NtkVanImpComputeMis( p ); -// p->vImpsMis = Vec_IntDup( p->vImps ); -p->timeMis += clock() - clk; - if ( p->fVerbose ) - printf( "Final : Seq = %7d. MIS = %7d. Const = %5d.\n", Vec_IntSize(p->vImps), Vec_IntSize(p->vImpsMis), Vec_PtrSize(p->vZeros) ); - - -/* - if ( p->fVerbose ) - { - PRT( "All ", p->timeAll ); - PRT( "Sim ", p->timeSim ); - PRT( "Add ", p->timeAdd ); - PRT( "Check ", p->timeCheck ); - PRT( "Mis ", p->timeMis ); - } -*/ - -/* - // print the implications in the MIS - if ( p->fVerbose ) - { - Abc_Obj_t * pNode, * pNode1, * pNode2; - unsigned Imp; - int i; - if ( Vec_PtrSize(p->vZeros) ) - { - printf( "The const nodes are: " ); - Vec_PtrForEachEntry( p->vZeros, pNode, i ) - printf( "%d(%d) ", pNode->Id, pNode->fPhase ); - printf( "\n" ); - } - if ( Vec_IntSize(p->vImpsMis) ) - { - printf( "The implications are: " ); - Vec_IntForEachEntry( p->vImpsMis, Imp, i ) - { - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - printf( "%d(%d)=>%d(%d) ", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); - } - printf( "\n" ); - } - } -*/ -} - -/**Function************************************************************* - - Synopsis [Filters zeros and implications by performing one inductive step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpFilter( Van_Man_t * p, Fraig_Man_t * pFraig, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) -{ - ProgressBar * pProgress; - Abc_Obj_t * pNode, * pNodeM1, * pNodeM2, * pNode1, * pNode2, * pObj; - Fraig_Node_t * pFNode1, * pFNode2; - Fraig_Node_t * ppFNodes[2]; - unsigned Imp; - int i, f, k, clk; - -clk = clock(); - for ( f = 0; f < p->nFrames; f++ ) - { - // add new clauses for zeros - Vec_PtrForEachEntry( p->vZeros, pNode, i ) - { - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, f ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode1 = Fraig_NotCond( pFNode1, !pNode->fPhase ); - Fraig_ManAddClause( pFraig, &pFNode1, 1 ); - } - // add new clauses for imps - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, f ); - pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, f ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); - ppFNodes[0] = Fraig_NotCond( pFNode1, !pNode1->fPhase ); - ppFNodes[1] = Fraig_NotCond( pFNode2, pNode2->fPhase ); -// assert( Fraig_Regular(ppFNodes[0]) != Fraig_Regular(ppFNodes[1]) ); - Fraig_ManAddClause( pFraig, ppFNodes, 2 ); - } - } -p->timeAdd += clock() - clk; - - // check the zero nodes -clk = clock(); - Vec_PtrClear( vZeros ); - Vec_PtrForEachEntry( p->vZeros, pNode, i ) - { - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode, p->vCorresp, p->nFrames ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode1 = Fraig_Regular(pFNode1); - pFNode2 = Fraig_ManReadConst1(pFraig); - if ( pFNode1 == pFNode2 || Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) - Vec_PtrPush( vZeros, pNode ); - else - { - // since we disproved this zero, we should add all possible implications to p->vImps - // these implications will be checked below and only correct ones will remain - Abc_NtkForEachObj( p->pNtkSingle, pObj, k ) - { - if ( Abc_ObjIsPo(pObj) ) - continue; - if ( Vec_IntEntry( p->vCounters, pObj->Id ) > 0 ) - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode, pObj) ); - } - } - } - - // check implications - pProgress = Extra_ProgressBarStart( stdout, p->vImps->nSize ); - Vec_IntClear( vImps ); - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - Extra_ProgressBarUpdate( pProgress, i, NULL ); - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - pNodeM1 = Abc_NodeVanImpReadCorresp( pNode1, p->vCorresp, p->nFrames ); - pNodeM2 = Abc_NodeVanImpReadCorresp( pNode2, p->vCorresp, p->nFrames ); - pFNode1 = Fraig_NotCond( Abc_ObjRegular(pNodeM1)->pCopy, Abc_ObjIsComplement(pNodeM1) ); - pFNode2 = Fraig_NotCond( Abc_ObjRegular(pNodeM2)->pCopy, Abc_ObjIsComplement(pNodeM2) ); - pFNode1 = Fraig_NotCond( pFNode1, !pNode1->fPhase ); - pFNode2 = Fraig_NotCond( pFNode2, pNode2->fPhase ); - if ( pFNode1 == Fraig_Not(pFNode2) ) - { - Vec_IntPush( vImps, Imp ); - continue; - } - if ( pFNode1 == pFNode2 ) - { - if ( pFNode1 == Fraig_Not( Fraig_ManReadConst1(pFraig) ) ) - continue; - if ( pFNode1 == Fraig_ManReadConst1(pFraig) ) - { - Vec_IntPush( vImps, Imp ); - continue; - } - pFNode1 = Fraig_Regular(pFNode1); - pFNode2 = Fraig_ManReadConst1(pFraig); - if ( Fraig_NodeIsEquivalent( pFraig, pFNode1, pFNode2, -1, 100 ) ) - Vec_IntPush( vImps, Imp ); - continue; - } - - if ( Fraig_ManCheckClauseUsingSat( pFraig, pFNode1, pFNode2, -1 ) ) - Vec_IntPush( vImps, Imp ); - } - Extra_ProgressBarStop( pProgress ); -p->timeCheck += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [Computes all implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpComputeAll( Van_Man_t * p ) -{ - ProgressBar * pProgress; - Fraig_Man_t * pManSingle; - Vec_Ptr_t * vInfo; - Abc_Obj_t * pObj, * pNode1, * pNode2, * pConst1; - Fraig_Node_t * pFNode1, * pFNode2; - unsigned * pPats1, * pPats2; - int nFrames, nUnsigned, RetValue; - int clk, i, k, Count1, Count2; - - // decide how many frames to simulate - nFrames = 32; - nUnsigned = 32; - p->nWords = nFrames * nUnsigned; - - // simulate randomly the initialized frames -clk = clock(); - vInfo = Sim_SimulateSeqRandom( p->pNtkSingle, nFrames, nUnsigned ); - - // complement the info for those nodes whose phase is 1 - Abc_NtkForEachObj( p->pNtkSingle, pObj, i ) - if ( pObj->fPhase ) - Sim_UtilSetCompl( Sim_SimInfoGet(vInfo, pObj), p->nWords ); - - // compute the number of ones for each node - p->vCounters = Sim_UtilCountOnesArray( vInfo, p->nWords ); -p->timeSim += clock() - clk; - - // FRAIG the uninitialized frame - pManSingle = Abc_NtkVanEijkFraig( p->pNtkSingle, 0 ); - // now pNode->pCopy are assigned the pointers to the corresponding FRAIG nodes - -/* -Abc_NtkForEachPi( p->pNtkSingle, pNode1, i ) -printf( "PI = %d\n", pNode1->Id ); -Abc_NtkForEachLatch( p->pNtkSingle, pNode1, i ) -printf( "Latch = %d\n", pNode1->Id ); -Abc_NtkForEachPo( p->pNtkSingle, pNode1, i ) -printf( "PO = %d\n", pNode1->Id ); -*/ - - // go through the pairs of signals in the frames - pProgress = Extra_ProgressBarStart( stdout, p->nIdMax ); - pConst1 = Abc_AigConst1(p->pNtkSingle); - p->vImps = Vec_IntAlloc( 100 ); - p->vZeros = Vec_PtrAlloc( 100 ); - Abc_NtkForEachObj( p->pNtkSingle, pNode1, i ) - { - if ( Abc_ObjIsPo(pNode1) ) - continue; - if ( pNode1 == pConst1 ) - continue; - Extra_ProgressBarUpdate( pProgress, i, NULL ); - - // get the number of zeros of this node - Count1 = Vec_IntEntry( p->vCounters, pNode1->Id ); - if ( Count1 == 0 ) - { - Vec_PtrPush( p->vZeros, pNode1 ); - p->nZeros++; - continue; - } - pPats1 = Sim_SimInfoGet(vInfo, pNode1); - - Abc_NtkForEachObj( p->pNtkSingle, pNode2, k ) - { - if ( k >= i ) - break; - if ( Abc_ObjIsPo(pNode2) ) - continue; - if ( pNode2 == pConst1 ) - continue; - p->nPairsAll++; - - // here we have a pair of nodes (pNode1 and pNode2) - // such that Id(pNode1) < Id(pNode2) - assert( pNode2->Id < pNode1->Id ); - - // get the number of zeros of this node - Count2 = Vec_IntEntry( p->vCounters, pNode2->Id ); - if ( Count2 == 0 ) - continue; - pPats2 = Sim_SimInfoGet(vInfo, pNode2); - - // check for implications - if ( Count1 < Count2 ) - { -//clk = clock(); - RetValue = Sim_UtilInfoIsImp( pPats1, pPats2, p->nWords ); -//p->timeInfo += clock() - clk; - if ( !RetValue ) - continue; - p->nImpsAll++; - // pPats1 => pPats2 or pPats1' v pPats2 - pFNode1 = Fraig_NotCond( pNode1->pCopy, !pNode1->fPhase ); - pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); - // check if this implication is combinational - if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) - continue; - // otherwise record it - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); - } - else if ( Count2 < Count1 ) - { -//clk = clock(); - RetValue = Sim_UtilInfoIsImp( pPats2, pPats1, p->nWords ); -//p->timeInfo += clock() - clk; - if ( !RetValue ) - continue; - p->nImpsAll++; - // pPats2 => pPats2 or pPats2' v pPats1 - pFNode2 = Fraig_NotCond( pNode2->pCopy, !pNode2->fPhase ); - pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); - // check if this implication is combinational - if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, pFNode2 ) ) - continue; - // otherwise record it - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); - } - else - { -//clk = clock(); - RetValue = Sim_UtilInfoIsEqual(pPats1, pPats2, p->nWords); -//p->timeInfo += clock() - clk; - if ( !RetValue ) - continue; - p->nEquals++; - // get the FRAIG nodes - pFNode1 = Fraig_NotCond( pNode1->pCopy, pNode1->fPhase ); - pFNode2 = Fraig_NotCond( pNode2->pCopy, pNode2->fPhase ); - - // check if this implication is combinational - if ( Fraig_ManCheckClauseUsingSimInfo( pManSingle, Fraig_Not(pFNode1), pFNode2 ) ) - { - if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); - else - assert( 0 ); // impossible for FRAIG - } - else - { - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode1, pNode2) ); - if ( !Fraig_ManCheckClauseUsingSimInfo( pManSingle, pFNode1, Fraig_Not(pFNode2) ) ) - Vec_IntPush( p->vImps, Abc_NodeVanGetImp(pNode2, pNode1) ); - } - } -// printf( "Implication %d %d -> %d %d \n", pNode1->Id, pNode1->fPhase, pNode2->Id, pNode2->fPhase ); - } - } - Fraig_ManFree( pManSingle ); - Sim_UtilInfoFree( vInfo ); - Extra_ProgressBarStop( pProgress ); -} - - -/**Function************************************************************* - - Synopsis [Sorts the nodes.] - - Description [Sorts the nodes appearing in the left-hand sides of the - implications by the number of 1s in their simulation info.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NtkVanImpSortByOnes( Van_Man_t * p ) -{ - Abc_Obj_t * pNode, * pList; - Vec_Ptr_t * vSorted; - unsigned Imp; - int i, nOnes; - - // start the sorted array - vSorted = Vec_PtrStart( p->nWords * 32 ); - // go through the implications - Abc_NtkIncrementTravId( p->pNtkSingle ); - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - pNode = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - assert( !Abc_ObjIsPo(pNode) ); - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - continue; - // mark the node as visited - Abc_NodeSetTravIdCurrent( pNode ); - - // add the node to the list - nOnes = Vec_IntEntry( p->vCounters, pNode->Id ); - pList = Vec_PtrEntry( vSorted, nOnes ); - pNode->pNext = pList; - Vec_PtrWriteEntry( vSorted, nOnes, pNode ); - } - return vSorted; -} - -/**Function************************************************************* - - Synopsis [Computes the array of beginnings.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkVanImpComputeBegs( Van_Man_t * p ) -{ - Vec_Int_t * vBegins; - unsigned Imp; - int i, ItemLast, ItemCur; - - // sort the implications (by the number of the left-hand-side node) - Vec_IntSort( p->vImps, 0 ); - - // start the array of beginnings - vBegins = Vec_IntStart( p->nIdMax + 1 ); - - // mark the begining of each node's implications - ItemLast = 0; - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - ItemCur = (Imp >> 16); - if ( ItemCur == ItemLast ) - continue; - Vec_IntWriteEntry( vBegins, ItemCur, i ); - ItemLast = ItemCur; - } - // fill in the empty spaces - ItemLast = Vec_IntSize(p->vImps); - Vec_IntWriteEntry( vBegins, p->nIdMax, ItemLast ); - Vec_IntForEachEntryReverse( vBegins, ItemCur, i ) - { - if ( ItemCur == 0 ) - Vec_IntWriteEntry( vBegins, i, ItemLast ); - else - ItemLast = ItemCur; - } - - Imp = Vec_IntEntry( p->vImps, 0 ); - ItemCur = (Imp >> 16); - for ( i = 0; i <= ItemCur; i++ ) - Vec_IntWriteEntry( vBegins, i, 0 ); - return vBegins; -} - -/**Function************************************************************* - - Synopsis [Derives the minimum subset of implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkVanImpMark_rec( Abc_Obj_t * pNode, Vec_Vec_t * vImpsMis ) -{ - Vec_Int_t * vNexts; - int i, Next; - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNode ) ) - return; - // mark the node as visited - Abc_NodeSetTravIdCurrent( pNode ); - // mark the children - vNexts = Vec_VecEntry( vImpsMis, pNode->Id ); - Vec_IntForEachEntry( vNexts, Next, i ) - Abc_NtkVanImpMark_rec( Abc_NtkObj(pNode->pNtk, Next), vImpsMis ); -} - -/**Function************************************************************* - - Synopsis [Derives the minimum subset of implications.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Abc_NtkVanImpComputeMis( Van_Man_t * p ) -{ - Abc_Obj_t * pNode, * pNext, * pList; - Vec_Vec_t * vMatrix; - Vec_Ptr_t * vSorted; - Vec_Int_t * vBegins; - Vec_Int_t * vImpsMis; - int i, k, iStart, iStop; - void * pEntry; - unsigned Imp; - - if ( Vec_IntSize(p->vImps) == 0 ) - return Vec_IntAlloc(0); - - // compute the sorted list of nodes by the number of 1s - Abc_NtkCleanNext( p->pNtkSingle ); - vSorted = Abc_NtkVanImpSortByOnes( p ); - - // compute the array of beginnings - vBegins = Abc_NtkVanImpComputeBegs( p ); - -/* -Vec_IntForEachEntry( p->vImps, Imp, i ) -{ - printf( "%d: ", i ); - Abc_NodeVanPrintImp( Imp ); -} -printf( "\n\n" ); -Vec_IntForEachEntry( vBegins, Imp, i ) - printf( "%d=%d ", i, Imp ); -printf( "\n\n" ); -*/ - - // compute the MIS by considering nodes in the reverse order of ones - vMatrix = Vec_VecStart( p->nIdMax ); - Vec_PtrForEachEntryReverse( vSorted, pList, i ) - { - for ( pNode = pList; pNode; pNode = pNode->pNext ) - { - // get the starting and stopping implication of this node - iStart = Vec_IntEntry( vBegins, pNode->Id ); - iStop = Vec_IntEntry( vBegins, pNode->Id + 1 ); - if ( iStart == iStop ) - continue; - assert( iStart < iStop ); - // go through all the implications of this node - Abc_NtkIncrementTravId( p->pNtkSingle ); - Abc_NodeIsTravIdCurrent( pNode ); - Vec_IntForEachEntryStartStop( p->vImps, Imp, k, iStart, iStop ) - { - assert( pNode == Abc_NodeVanGetLeft(p->pNtkSingle, Imp) ); - pNext = Abc_NodeVanGetRight(p->pNtkSingle, Imp); - // if this node is already visited, skip - if ( Abc_NodeIsTravIdCurrent( pNext ) ) - continue; - assert( pNode->Id != pNext->Id ); - // add implication - Vec_VecPush( vMatrix, pNode->Id, (void *)pNext->Id ); - // recursively mark dependent nodes - Abc_NtkVanImpMark_rec( pNext, vMatrix ); - } - } - } - Vec_IntFree( vBegins ); - Vec_PtrFree( vSorted ); - - // transfer the MIS into the normal array - vImpsMis = Vec_IntAlloc( 100 ); - Vec_VecForEachEntry( vMatrix, pEntry, i, k ) - { - assert( (i << 16) != ((int)pEntry) ); - Vec_IntPush( vImpsMis, (i << 16) | ((int)pEntry) ); - } - Vec_VecFree( vMatrix ); - return vImpsMis; -} - - -/**Function************************************************************* - - Synopsis [Count equal pairs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkVanImpCountEqual( Van_Man_t * p ) -{ - Abc_Obj_t * pNode1, * pNode2, * pNode3; - Vec_Int_t * vBegins; - int iStart, iStop; - unsigned Imp, ImpR; - int i, k, Counter; - - // compute the array of beginnings - vBegins = Abc_NtkVanImpComputeBegs( p ); - - // go through each node and out - Counter = 0; - Vec_IntForEachEntry( p->vImps, Imp, i ) - { - pNode1 = Abc_NodeVanGetLeft( p->pNtkSingle, Imp ); - pNode2 = Abc_NodeVanGetRight( p->pNtkSingle, Imp ); - if ( pNode1->Id > pNode2->Id ) - continue; - iStart = Vec_IntEntry( vBegins, pNode2->Id ); - iStop = Vec_IntEntry( vBegins, pNode2->Id + 1 ); - Vec_IntForEachEntryStartStop( p->vImps, ImpR, k, iStart, iStop ) - { - assert( pNode2 == Abc_NodeVanGetLeft(p->pNtkSingle, ImpR) ); - pNode3 = Abc_NodeVanGetRight(p->pNtkSingle, ImpR); - if ( pNode1 == pNode3 ) - { - Counter++; - break; - } - } - } - Vec_IntFree( vBegins ); - return Counter; -} - - -/**Function************************************************************* - - Synopsis [Create EXDC from the equivalence classes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_Int_t * vImps ) -{ - Abc_Ntk_t * pNtkNew; - Vec_Ptr_t * vCone; - Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;//, * pObjNew; - unsigned Imp; - int i, k; - - assert( Abc_NtkIsStrash(pNtk) ); - - // start the network - pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); - pNtkNew->pName = Extra_UtilStrsav( "exdc" ); - pNtkNew->pSpec = NULL; - - // map the constant nodes - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - // for each CI, create PI - Abc_NtkForEachCi( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePi(pNtkNew), Abc_ObjName(pObj) ); - // cannot add latches here because pLatch->pCopy pointers are used - - // build logic cone for zero nodes - pTotal = Abc_ObjNot( Abc_AigConst1(pNtkNew) ); - Vec_PtrForEachEntry( vZeros, pNode, i ) - { - // build the logic cone for the node - if ( Abc_ObjFaninNum(pNode) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pNode, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode ); - } - // complement if there is phase difference - pNode->pCopy = Abc_ObjNotCond( pNode->pCopy, pNode->fPhase ); - - // add it to the EXDC - pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pNode->pCopy ); - } - - // create logic cones for the implications - Vec_IntForEachEntry( vImps, Imp, i ) - { - pNode1 = Abc_NtkObj(pNtk, Imp >> 16); - pNode2 = Abc_NtkObj(pNtk, Imp & 0xFFFF); - - // build the logic cone for the first node - if ( Abc_ObjFaninNum(pNode1) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pNode1, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode1 ); - } - // complement if there is phase difference - pNode1->pCopy = Abc_ObjNotCond( pNode1->pCopy, pNode1->fPhase ); - - // build the logic cone for the second node - if ( Abc_ObjFaninNum(pNode2) == 2 ) - { - vCone = Abc_NtkDfsNodes( pNtk, &pNode2, 1 ); - Vec_PtrForEachEntry( vCone, pObj, k ) - pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); - Vec_PtrFree( vCone ); - assert( pObj == pNode2 ); - } - // complement if there is phase difference - pNode2->pCopy = Abc_ObjNotCond( pNode2->pCopy, pNode2->fPhase ); - - // build the implication and add it to the EXDC - pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) ); - pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter ); - } -/* - // create the only PO - pObjNew = Abc_NtkCreatePo( pNtkNew ); - // add the PO name - Abc_NtkLogicStoreName( pObjNew, "DC" ); - // add the PO - Abc_ObjAddFanin( pObjNew, pTotal ); - - // quontify the PIs existentially - pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew ); - - // get the new PO - pObjNew = Abc_NtkPo( pNtkNew, 0 ); - // remember the miter output - pTotal = Abc_ObjChild0( pObjNew ); - // remove the PO - Abc_NtkDeleteObj( pObjNew ); - - // make the old network point to the new things - Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkNew); - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pCopy = Abc_NtkPi( pNtkNew, i ); -*/ - - // for each CO, create PO (skip POs equal to CIs because of name conflict) - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjName(pObj) ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_NtkLogicStoreName( pObj->pCopy = Abc_NtkCreatePo(pNtkNew), Abc_ObjNameSuffix(pObj, "_in") ); - - // link to the POs of the network - Abc_NtkForEachPo( pNtk, pObj, i ) - if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - Abc_NtkForEachLatch( pNtk, pObj, i ) - Abc_ObjAddFanin( pObj->pCopy, pTotal ); - - // remove the extra nodes - Abc_AigCleanup( pNtkNew->pManFunc ); - - // check the result - if ( !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkVanImpDeriveExdc: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } - return pNtkNew; -} - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index c6782b07..1fddc8cb 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -544,7 +544,7 @@ void Abc_NtkGetSeqPoSupp( Abc_Ntk_t * pNtk, int iFrame, int iNumPo ) Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = NULL; Abc_NtkForEachLatch( pNtk, pObj, i ) - if ( Abc_NtkLatch(pFrames, i)->pCopy ) + if ( Abc_NtkBox(pFrames, i)->pCopy ) pObj->pCopy = (void *)1; Abc_NtkForEachPi( pNtk, pObj, i ) for ( k = 0; k <= iFrame; k++ ) diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 54c6f05c..dba9e6fd 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -33,6 +33,4 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcTiming.c \ src/base/abci/abcUnate.c \ src/base/abci/abcUnreach.c \ - src/base/abci/abcVanEijk.c \ - src/base/abci/abcVanImp.c \ src/base/abci/abcVerify.c |