diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2005-09-08 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2005-09-08 08:01:00 -0700 |
commit | eb4cdcdcb4db6e468aa02a7949217fa6da245217 (patch) | |
tree | 34223999f598d157831c030392666a937b020992 /src/base | |
parent | 1260d20cc05fe2d21088cc047c460e85ccdb3b14 (diff) | |
download | abc-eb4cdcdcb4db6e468aa02a7949217fa6da245217.tar.gz abc-eb4cdcdcb4db6e468aa02a7949217fa6da245217.tar.bz2 abc-eb4cdcdcb4db6e468aa02a7949217fa6da245217.zip |
Version abc50908
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abc/abc.h | 23 | ||||
-rw-r--r-- | src/base/abc/abcAig.c | 34 | ||||
-rw-r--r-- | src/base/abc/abcCheck.c | 1 | ||||
-rw-r--r-- | src/base/abc/abcDfs.c | 63 | ||||
-rw-r--r-- | src/base/abc/abcInt.h | 11 | ||||
-rw-r--r-- | src/base/abc/abcNtk.c | 11 | ||||
-rw-r--r-- | src/base/abc/abcObj.c | 7 | ||||
-rw-r--r-- | src/base/abc/abcRefs.c | 70 | ||||
-rw-r--r-- | src/base/abc/abcUtil.c | 95 | ||||
-rw-r--r-- | src/base/abci/abc.c | 150 | ||||
-rw-r--r-- | src/base/abci/abcBalance.c | 31 | ||||
-rw-r--r-- | src/base/abci/abcFraig.c | 10 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 10 | ||||
-rw-r--r-- | src/base/abci/abcRefactor.c | 27 | ||||
-rw-r--r-- | src/base/abci/abcRenode.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcRewrite.c | 20 | ||||
-rw-r--r-- | src/base/abci/abcSat.c | 51 | ||||
-rw-r--r-- | src/base/abci/abcSweep.c | 2 | ||||
-rw-r--r-- | src/base/abci/abcVerify.c | 256 | ||||
-rw-r--r-- | src/base/abcs/abcSeq.c | 2 | ||||
-rw-r--r-- | src/base/main/main.c | 65 | ||||
-rw-r--r-- | src/base/main/main.h | 6 |
22 files changed, 776 insertions, 171 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index aea5a62d..f29859b9 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -147,10 +147,10 @@ struct Abc_Ntk_t_ Vec_Ptr_t * vCos; // the array of combinational outputs (POs followed by latches) Vec_Ptr_t * vLats; // the array of latches (or the cutset in the sequential network) // the stats about the number of living objects - int nObjs; // the number of living objs - int nNets; // the number of living nets - int nNodes; // the number of living nodes - int nLatches; // the number of latches + int nObjs; // the number of live objs + int nNets; // the number of live nets + int nNodes; // the number of live nodes + int nLatches; // the number of live latches int nPis; // the number of primary inputs int nPos; // the number of primary outputs // the functionality manager @@ -167,6 +167,8 @@ struct Abc_Ntk_t_ Vec_Int_t * vLevelsR; // level in the reverse topological order // support information Vec_Ptr_t * vSupps; + // the satisfiable assignment of the miter + int * pModel; // the external don't-care if given Abc_Ntk_t * pExdc; // the EXDC network // miscellaneous data members @@ -401,7 +403,7 @@ extern Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Ab extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ); -extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ); +extern void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel ); extern void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld ); extern bool Abc_AigNodeHasComplFanoutEdge( Abc_Obj_t * pNode ); extern bool Abc_AigNodeHasComplFanoutEdgeTrav( Abc_Obj_t * pNode ); @@ -414,6 +416,7 @@ extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate ); /*=== abcCheck.c ==========================================================*/ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk ); +extern bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj ); extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ); /*=== abcCollapse.c ==========================================================*/ @@ -427,6 +430,7 @@ extern void Abc_NodeFreeCuts( void * p, Abc_Obj_t * pObj ); extern Vec_Ptr_t * Abc_NtkDfs( Abc_Ntk_t * pNtk, int fCollectAll ); extern Vec_Ptr_t * Abc_NtkDfsNodes( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); extern Vec_Ptr_t * Abc_NtkDfsReverse( Abc_Ntk_t * pNtk ); +extern Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ); extern Vec_Ptr_t * Abc_AigDfs( Abc_Ntk_t * pNtk, int fCollectAll, int fCollectCos ); extern Vec_Vec_t * Abc_DfsLevelized( Abc_Obj_t * pNode, bool fTfi ); extern int Abc_NtkGetLevelNum( Abc_Ntk_t * pNtk ); @@ -440,6 +444,7 @@ extern void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t extern void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); /*=== abcFraig.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ); +extern void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ); extern Abc_Ntk_t * Abc_NtkFraigTrust( Abc_Ntk_t * pNtk ); extern int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkFraigRestore(); @@ -470,9 +475,6 @@ extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ); extern int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ); /*=== abcObj.c ==========================================================*/ -extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); -extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); -extern void Abc_ObjAdd( Abc_Obj_t * pObj ); extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj ); extern Abc_Obj_t * Abc_NtkDupConst1( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ); extern Abc_Obj_t * Abc_NtkDupReset( Abc_Ntk_t * pNtkAig, Abc_Ntk_t * pNtkNew ); @@ -560,12 +562,13 @@ extern Vec_Ptr_t * Abc_NodeCollectTfoCands( Abc_ManCut_t * p, Abc_Obj_t * extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); +extern int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); extern Vec_Ptr_t * Abc_NodeMffcCollect( Abc_Obj_t * pNode ); /*=== abcRenode.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); /*=== abcSat.c ==========================================================*/ -extern bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ); +extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ); /*=== abcSeq.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ); @@ -660,6 +663,8 @@ extern int Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_O extern int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ); extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk ); +extern Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk ); +extern void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ); //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 9588f1e0..701fb90f 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -83,7 +83,7 @@ static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_O static void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis ); static void Abc_AigResize( Abc_Aig_t * pMan ); // incremental AIG procedures -static void Abc_AigReplace_int( Abc_Aig_t * pMan ); +static void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel ); static void Abc_AigDelete_int( Abc_Aig_t * pMan ); static void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan ); static void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan ); @@ -655,7 +655,7 @@ Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ) SeeAlso [] ***********************************************************************/ -void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ) +void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool fUpdateLevel ) { assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 ); assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 ); @@ -663,9 +663,12 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ) Vec_PtrPush( pMan->vStackReplaceOld, pOld ); Vec_PtrPush( pMan->vStackReplaceNew, pNew ); while ( Vec_PtrSize(pMan->vStackReplaceOld) ) - Abc_AigReplace_int( pMan ); - Abc_AigUpdateLevel_int( pMan ); - Abc_AigUpdateLevelR_int( pMan ); + Abc_AigReplace_int( pMan, fUpdateLevel ); + if ( fUpdateLevel ) + { + Abc_AigUpdateLevel_int( pMan ); + Abc_AigUpdateLevelR_int( pMan ); + } } /**Function************************************************************* @@ -679,7 +682,7 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew ) SeeAlso [] ***********************************************************************/ -void Abc_AigReplace_int( Abc_Aig_t * pMan ) +void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel ) { Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout; int k, v, iFanin; @@ -736,14 +739,17 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan ) Abc_AigAndCreateFrom( pMan, pFanin1, pFanin2, pFanout ); assert( Abc_AigNodeIsAcyclic(pFanout, pFanout) ); - // schedule the updated fanout for updating direct level - assert( pFanout->fMarkA == 0 ); - pFanout->fMarkA = 1; - Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout ); - // schedule the updated fanout for updating reverse level - assert( pFanout->fMarkB == 0 ); - pFanout->fMarkB = 1; - Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout ); + if ( fUpdateLevel ) + { + // schedule the updated fanout for updating direct level + assert( pFanout->fMarkA == 0 ); + pFanout->fMarkA = 1; + Vec_VecPush( pMan->vLevels, pFanout->Level, pFanout ); + // schedule the updated fanout for updating reverse level + assert( pFanout->fMarkB == 0 ); + pFanout->fMarkB = 1; + Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanout), pFanout ); + } // the fanout has changed, update EXOR status of its fanouts Abc_ObjForEachFanout( pFanout, pFanoutFanout, v ) diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index 1d23d7ed..43235139 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -25,7 +25,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static bool Abc_NtkDoCheck( Abc_Ntk_t * pNtk ); static bool Abc_NtkCheckNames( Abc_Ntk_t * pNtk ); static bool Abc_NtkCheckPis( Abc_Ntk_t * pNtk ); static bool Abc_NtkCheckPos( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index 2fbbee37..31a6e8b9 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -27,6 +27,7 @@ static void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); static void Abc_AigDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); static void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); +static void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); static void Abc_DfsLevelizedTfo_rec( Abc_Obj_t * pNode, Vec_Vec_t * vLevels ); static int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode ); static bool Abc_NtkIsAcyclic_rec( Abc_Obj_t * pNode ); @@ -208,6 +209,68 @@ void Abc_NtkDfsReverse_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) /**Function************************************************************* + Synopsis [Returns the set of CI nodes in the support of the given nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkNodeSupport( Abc_Ntk_t * pNtk, Abc_Obj_t ** ppNodes, int nNodes ) +{ + Vec_Ptr_t * vNodes; + int i; + // set the traversal ID + Abc_NtkIncrementTravId( pNtk ); + // start the array of nodes + vNodes = Vec_PtrAlloc( 100 ); + // go through the PO nodes and call for each of them + for ( i = 0; i < nNodes; i++ ) + if ( Abc_ObjIsCo(ppNodes[i]) ) + Abc_NtkNodeSupport_rec( Abc_ObjFanin0(ppNodes[i]), vNodes ); + else + Abc_NtkNodeSupport_rec( ppNodes[i], vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Performs DFS for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkNodeSupport_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Abc_Obj_t * pFanin; + int i; + assert( !Abc_ObjIsNet(pNode) ); + // if this node is already visited, skip + if ( Abc_NodeIsTravIdCurrent( pNode ) ) + return; + // mark the node as visited + Abc_NodeSetTravIdCurrent( pNode ); + // collect the CI + if ( Abc_ObjIsCi(pNode) ) + { + Vec_PtrPush( vNodes, pNode ); + return; + } + assert( Abc_ObjIsNode( pNode ) ); + // visit the transitive fanin of the node + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_NtkNodeSupport_rec( Abc_ObjFanin0Ntk(pFanin), vNodes ); +} + + +/**Function************************************************************* + Synopsis [Returns the DFS ordered array of logic nodes.] Description [Collects only the internal nodes, leaving out CIs/COs. diff --git a/src/base/abc/abcInt.h b/src/base/abc/abcInt.h index 1a1ab75f..c072c99b 100644 --- a/src/base/abc/abcInt.h +++ b/src/base/abc/abcInt.h @@ -29,6 +29,8 @@ /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// +#define ABC_NUM_STEPS 10 + //////////////////////////////////////////////////////////////////////// /// STRUCTURE DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -38,6 +40,15 @@ //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== abcObj.c ==========================================================*/ +extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); +extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); +extern void Abc_ObjAdd( Abc_Obj_t * pObj ); + +//////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 5c199141..b21d16fc 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abc.h" +#include "abcInt.h" #include "main.h" #include "mio.h" @@ -26,8 +27,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define ABC_NUM_STEPS 10 - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -400,7 +399,10 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * pFinal = Abc_AigConst1( pNtkNew->pManFunc ); Vec_PtrForEachEntry( vRoots, pObj, i ) { - pOther = pObj->pCopy; + if ( Abc_ObjIsCo(pObj) ) + pOther = Abc_ObjFanin0(pObj)->pCopy; + else + pOther = pObj->pCopy; if ( Vec_IntEntry(vValues, i) == 0 ) pOther = Abc_ObjNot(pOther); pFinal = Abc_AigAnd( pNtkNew->pManFunc, pFinal, pOther ); @@ -477,7 +479,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk ) // free large fanout arrays if ( pObj->vFanouts.nCap * 4 > LargePiece ) FREE( pObj->vFanouts.pArray ); - // check that the other things are okay + // these flags should be always zero + // if this is not true, something is wrong somewhere assert( pObj->fMarkA == 0 ); assert( pObj->fMarkB == 0 ); assert( pObj->fMarkC == 0 ); diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index 40c6e7a5..d5c18d2e 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "abc.h" +#include "abcInt.h" #include "main.h" #include "mio.h" @@ -66,7 +67,13 @@ Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) void Abc_ObjRecycle( Abc_Obj_t * pObj ) { Abc_Ntk_t * pNtk = pObj->pNtk; + int LargePiece = (4 << ABC_NUM_STEPS); + // free large fanout arrays + if ( pObj->vFanouts.nCap * 4 > LargePiece ) + FREE( pObj->vFanouts.pArray ); + // clean the memory to make deleted object distinct from the live one memset( pObj, 0, sizeof(Abc_Obj_t) ); + // recycle the object Extra_MmFixedEntryRecycle( pNtk->pMmObj, (char *)pObj ); } diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index 47618bf4..cdb236f3 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -26,6 +26,7 @@ static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes ); static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ); +static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -108,6 +109,42 @@ int Abc_NodeMffcLabel( Abc_Obj_t * pNode ) /**Function************************************************************* + Synopsis [Returns the MFFC size.] + + Description [Profiling shows that this procedure runs the same as + the above one, not faster.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Abc_Obj_t * pTemp; + int nConeSize, i; + + assert( !Abc_ObjIsComplement( pNode ) ); + assert( Abc_ObjIsNode( pNode ) ); + if ( Abc_ObjFaninNum(pNode) == 0 ) + return 0; + + Vec_PtrClear( vNodes ); + nConeSize = Abc_NodeDeref( pNode, vNodes ); + // label the nodes with the current ID and ref their children + Vec_PtrForEachEntry( vNodes, pTemp, i ) + { + Abc_NodeSetTravIdCurrent( pTemp ); + if ( Abc_ObjIsCi(pTemp) ) + continue; + Abc_ObjFanin0(pTemp)->vFanouts.nSize++; + Abc_ObjFanin1(pTemp)->vFanouts.nSize++; + } + return nConeSize; +} + +/**Function************************************************************* + Synopsis [Collects the nodes in MFFC in the topological order.] Description [] @@ -184,6 +221,39 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t Synopsis [References/references the node and returns MFFC size.] + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +{ + Abc_Obj_t * pNode0, * pNode1; + int Counter; + // collect visited nodes + Vec_PtrPush( vNodes, pNode ); + // skip the CI + if ( Abc_ObjIsCi(pNode) ) + return 0; + // process the internal node + pNode0 = Abc_ObjFanin0(pNode); + pNode1 = Abc_ObjFanin1(pNode); + assert( pNode0->vFanouts.nSize > 0 ); + assert( pNode1->vFanouts.nSize > 0 ); + Counter = 1; + if ( --pNode0->vFanouts.nSize == 0 ) + Counter += Abc_NodeDeref( pNode0, vNodes ); + if ( --pNode1->vFanouts.nSize == 0 ) + Counter += Abc_NodeDeref( pNode1, vNodes ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [References/references the node and returns MFFC size.] + Description [Stops at the complemented edges.] SideEffects [] diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 7a6a705d..0f7a4ab8 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -883,6 +883,101 @@ Vec_Ptr_t * Abc_NtkCollectObjects( Abc_Ntk_t * pNtk ) return vNodes; } +/**Function************************************************************* + + Synopsis [Returns the array of CI IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkGetCiIds( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vCiIds; + Abc_Obj_t * pObj; + int i; + vCiIds = Vec_IntAlloc( Abc_NtkCiNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + Vec_IntPush( vCiIds, pObj->Id ); + return vCiIds; +} + +/**Function************************************************************* + + Synopsis [Puts the nodes into the DFS order and reassign their IDs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkReassignIds( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Vec_Ptr_t * vObjsNew; + Abc_Obj_t * pNode, * pTemp; + Abc_Obj_t * pConst1 = NULL, * pReset = NULL; + int i, k; + // start the array of objects with new IDs + vObjsNew = Vec_PtrAlloc( pNtk->nObjs ); + // put constant nodes (if present) first + if ( Abc_NtkIsStrash(pNtk) ) + { + pConst1 = Abc_AigConst1(pNtk->pManFunc); + pConst1->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pConst1 ); + pReset = Abc_AigReset(pNtk->pManFunc); + pReset->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pReset ); + } + // put PI nodes next + Abc_NtkForEachPi( pNtk, pNode, i ) + { + pNode->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pNode ); + } + // put PO nodes next + Abc_NtkForEachPo( pNtk, pNode, i ) + { + pNode->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pNode ); + } + // put latches next + Abc_NtkForEachLatch( pNtk, pNode, i ) + { + pNode->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pNode ); + } + // finally, internal nodes in the DFS order + vNodes = Abc_NtkDfs( pNtk, 1 ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( pNode == pReset || pNode == pConst1 ) + continue; + pNode->Id = Vec_PtrSize( vObjsNew ); + Vec_PtrPush( vObjsNew, pNode ); + } + Vec_PtrFree( vNodes ); + assert( Vec_PtrSize(vObjsNew) == pNtk->nObjs ); + + // update the fanin/fanout arrays + Abc_NtkForEachObj( pNtk, pNode, i ) + { + Abc_ObjForEachFanin( pNode, pTemp, k ) + pNode->vFanins.pArray[k].iFan = pTemp->Id; + Abc_ObjForEachFanout( pNode, pTemp, k ) + pNode->vFanouts.pArray[k].iFan = pTemp->Id; + } + + // replace the array of objs + Vec_PtrFree( pNtk->vObjs ); + pNtk->vObjs = vObjsNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index c9e0df68..dfe3ccc8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -1672,26 +1672,31 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + bool fUpdateLevel; bool fPrecompute; bool fUseZeros; bool fVerbose; // external functions - extern void Rwr_Precompute(); - extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose ); + extern void Rwr_Precompute(); + extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fPrecompute = 0; - fUseZeros = 0; - fVerbose = 0; + fUpdateLevel = 0; + fPrecompute = 0; + fUseZeros = 0; + fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "xzvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "lxzvh" ) ) != EOF ) { switch ( c ) { + case 'l': + fUpdateLevel ^= 1; + break; case 'x': fPrecompute ^= 1; break; @@ -1731,7 +1736,7 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - if ( !Abc_NtkRewrite( pNtk, fUseZeros, fVerbose ) ) + if ( !Abc_NtkRewrite( pNtk, fUpdateLevel, fUseZeros, fVerbose ) ) { fprintf( pErr, "Rewriting has failed.\n" ); return 1; @@ -1739,8 +1744,9 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: rewrite [-zvh]\n" ); + fprintf( pErr, "usage: rewrite [-lzvh]\n" ); fprintf( pErr, "\t performs technology-independent rewriting of the AIG\n" ); + fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -1765,10 +1771,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int nNodeSizeMax; int nConeSizeMax; + bool fUpdateLevel; bool fUseZeros; bool fUseDcs; bool fVerbose; - extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose ); + extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -1777,11 +1784,12 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nNodeSizeMax = 10; nConeSizeMax = 16; + fUpdateLevel = 0; fUseZeros = 0; fUseDcs = 0; fVerbose = 0; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "NCzdvh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "NClzdvh" ) ) != EOF ) { switch ( c ) { @@ -1807,6 +1815,9 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConeSizeMax < 0 ) goto usage; break; + case 'l': + fUpdateLevel ^= 1; + break; case 'z': fUseZeros ^= 1; break; @@ -1846,7 +1857,7 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUseZeros, fUseDcs, fVerbose ) ) + if ( !Abc_NtkRefactor( pNtk, nNodeSizeMax, nConeSizeMax, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ) ) { fprintf( pErr, "Refactoring has failed.\n" ); return 1; @@ -1854,10 +1865,11 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: refactor [-N num] [-C num] [-zdvh]\n" ); + fprintf( pErr, "usage: refactor [-N num] [-C num] [-lzdvh]\n" ); fprintf( pErr, "\t performs technology-independent refactoring of the AIG\n" ); fprintf( pErr, "\t-N num : the max support of the collapsed node [default = %d]\n", nNodeSizeMax ); fprintf( pErr, "\t-C num : the max support of the containing cone [default = %d]\n", nConeSizeMax ); + fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); fprintf( pErr, "\t-d : toggle using don't-cares [default = %s]\n", fUseDcs? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); @@ -2291,7 +2303,9 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk; int c; + int RetValue; int fVerbose; + int nSeconds; pNtk = Abc_FrameReadNet(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -2299,11 +2313,23 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fVerbose = 0; + nSeconds = 20; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Tvh" ) ) != EOF ) { switch ( c ) { + case 'T': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nSeconds = atoi(argv[util_optind]); + util_optind++; + if ( nSeconds < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -2323,7 +2349,7 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) { fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); return 0; - } + } if ( !Abc_NtkIsLogic(pNtk) ) { fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" ); @@ -2334,15 +2360,19 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Abc_NtkIsSopLogic(pNtk) ) Abc_NtkSopToBdd(pNtk); - if ( Abc_NtkMiterSat( pNtk, fVerbose ) ) - printf( "The miter is satisfiable.\n" ); + RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose ); + if ( RetValue == -1 ) + printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) + printf( "The miter is SATISFIABLE.\n" ); else - printf( "The miter is unsatisfiable.\n" ); + printf( "The miter is UNSATISFIABLE.\n" ); return 0; usage: - fprintf( pErr, "usage: sat [-vh]\n" ); + fprintf( pErr, "usage: sat [-T num] [-vh]\n" ); fprintf( pErr, "\t solves the miter\n" ); + fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -2863,6 +2893,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fAllNodes = 0; + memset( pParams, 0, sizeof(Fraig_Params_t) ); pParams->nPatsRand = 2048; // the number of words of random simulation info pParams->nPatsDyna = 2048; // the number of words of dynamic simulation info pParams->nBTLimit = 99; // the max number of backtracks to perform @@ -2879,7 +2910,6 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { switch ( c ) { - case 'R': if ( util_optind >= argc ) { @@ -3913,9 +3943,10 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fSat; int fVerbose; + int nSeconds; - extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ); - extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose ); + extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ); + extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); @@ -3923,13 +3954,25 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - fSat = 0; - fVerbose = 0; + fSat = 0; + fVerbose = 0; + nSeconds = 20; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "svh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "Tsvh" ) ) != EOF ) { switch ( c ) { + case 'T': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nSeconds = atoi(argv[util_optind]); + util_optind++; + if ( nSeconds < 0 ) + goto usage; + break; case 's': fSat ^= 1; break; @@ -3948,24 +3991,25 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) // perform equivalence checking if ( fSat ) - Abc_NtkCecSat( pNtk1, pNtk2 ); + Abc_NtkCecSat( pNtk1, pNtk2, nSeconds ); else - Abc_NtkCecFraig( pNtk1, pNtk2, fVerbose ); + Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 0; usage: - fprintf( pErr, "usage: cec [-svh] <file1> <file2>\n" ); - fprintf( pErr, "\t performs combinational equivalence checking\n" ); - fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); - fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); - fprintf( pErr, "\t-h : print the command usage\n"); - fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); - fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); - fprintf( pErr, "\t if no files are given, uses the current network and its spec\n"); - fprintf( pErr, "\t if one file is given, uses the current network and the file\n"); + fprintf( pErr, "usage: cec [-T num] [-svh] <file1> <file2>\n" ); + fprintf( pErr, "\t performs combinational equivalence checking\n" ); + fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); + fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); + fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); + fprintf( pErr, "\t if no files are given, uses the current network and its spec\n"); + fprintf( pErr, "\t if one file is given, uses the current network and the file\n"); return 1; } @@ -3989,10 +4033,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int nArgcNew; int c; int fSat; + int fVerbose; int nFrames; + int nSeconds; - extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ); - extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ); + extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames ); + extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); pNtk = Abc_FrameReadNet(pAbc); @@ -4000,10 +4046,12 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 3; - fSat = 0; + fSat = 0; + fVerbose = 0; + nFrames = 3; + nSeconds = 20; util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Fsh" ) ) != EOF ) + while ( ( c = util_getopt( argc, argv, "FTsvh" ) ) != EOF ) { switch ( c ) { @@ -4018,6 +4066,20 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nFrames < 0 ) goto usage; break; + case 'T': + if ( util_optind >= argc ) + { + fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + nSeconds = atoi(argv[util_optind]); + util_optind++; + if ( nSeconds < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; case 's': fSat ^= 1; break; @@ -4033,20 +4095,22 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) // perform equivalence checking if ( fSat ) - Abc_NtkSecSat( pNtk1, pNtk2, nFrames ); + Abc_NtkSecSat( pNtk1, pNtk2, nSeconds, nFrames ); else - Abc_NtkSecFraig( pNtk1, pNtk2, nFrames ); + Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); return 0; usage: - fprintf( pErr, "usage: sec [-sh] [-F num] <file1> <file2>\n" ); + fprintf( pErr, "usage: sec [-F num] [-T num] [-svh] <file1> <file2>\n" ); fprintf( pErr, "\t performs bounded sequential equivalence checking\n" ); fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); fprintf( pErr, "\t if no files are given, uses the current network and its spec\n"); diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index 40701e41..5e0f81a1 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -25,8 +25,8 @@ //////////////////////////////////////////////////////////////////////// static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate ); -static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, bool fDuplicate ); -static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int fDuplicate ); +static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate ); +static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate ); static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate ); //////////////////////////////////////////////////////////////////////// @@ -86,7 +86,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica // set the level of PIs of AIG according to the arrival times of the old network Abc_NtkSetNodeLevelsArrival( pNtk ); // allocate temporary storage for supergates - vStorage = Vec_VecStart( Abc_AigGetLevelNum(pNtk) + 1 ); + vStorage = Vec_VecStart( 10 ); // perform balancing of POs pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) ); Abc_NtkForEachCo( pNtk, pNode, i ) @@ -94,7 +94,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica Extra_ProgressBarUpdate( pProgress, i, NULL ); // strash the driver node pDriver = Abc_ObjFanin0(pNode); - Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, fDuplicate ); + Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate ); } Extra_ProgressBarStop( pProgress ); Vec_VecFree( vStorage ); @@ -111,7 +111,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, bool fDuplicate ) +Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate ) { Abc_Aig_t * pMan = pNtkNew->pManFunc; Abc_Obj_t * pNodeNew, * pNode1, * pNode2; @@ -123,7 +123,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ return pNodeOld->pCopy; assert( Abc_ObjIsNode(pNodeOld) ); // get the implication supergate - vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, fDuplicate ); + vSuper = Abc_NodeBalanceCone( pNodeOld, vStorage, Level, fDuplicate ); if ( vSuper->nSize == 0 ) { // it means that the supergate contains two nodes in the opposite polarity pNodeOld->pCopy = Abc_ObjNot(Abc_AigConst1(pMan)); @@ -132,9 +132,11 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ // for each old node, derive the new well-balanced node for ( i = 0; i < vSuper->nSize; i++ ) { - pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, fDuplicate ); + pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate ); vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) ); } + if ( vSuper->nSize < 2 ) + printf( "BUG!\n" ); // sort the new nodes by level in the decreasing order Vec_PtrSort( vSuper, Abc_NodeCompareLevelsDecrease ); // balance the nodes @@ -149,6 +151,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ assert( pNodeOld->pCopy == NULL ); // mark the old node with the new node pNodeOld->pCopy = vSuper->pArray[0]; + vSuper->nSize = 0; return pNodeOld->pCopy; } @@ -165,17 +168,25 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int fDuplicate ) +Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, int fDuplicate ) { Vec_Ptr_t * vNodes; int RetValue, i; assert( !Abc_ObjIsComplement(pNode) ); - vNodes = Vec_VecEntry( vStorage, pNode->Level ); + // extend the storage + if ( Vec_VecSize( vStorage ) <= Level ) + Vec_VecPush( vStorage, Level, 0 ); + // get the temporary array of nodes + vNodes = Vec_VecEntry( vStorage, Level ); Vec_PtrClear( vNodes ); + // collect the nodes in the implication supergate RetValue = Abc_NodeBalanceCone_rec( pNode, vNodes, 1, fDuplicate ); - assert( vNodes->nSize > 0 ); + assert( vNodes->nSize > 1 ); + // unmark the visited nodes for ( i = 0; i < vNodes->nSize; i++ ) Abc_ObjRegular((Abc_Obj_t *)vNodes->pArray[i])->fMarkB = 0; + // if we found the node and its complement in the same implication supergate, + // return empty set of nodes (meaning that we should use constant-0 node) if ( RetValue == -1 ) vNodes->nSize = 0; return vNodes; diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index e82065fc..3f860585 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -26,7 +26,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig ); @@ -83,13 +82,14 @@ Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) SeeAlso [] ***********************************************************************/ -Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ) +void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes ) { Fraig_Man_t * pMan; ProgressBar * pProgress; Fraig_Node_t * pNodeFraig; Vec_Ptr_t * vNodes; Abc_Obj_t * pNode, * pConst1, * pReset; + int fInternal = ((Fraig_Params_t *)pParams)->fInternal; int i; assert( Abc_NtkIsStrash(pNtk) ); @@ -106,11 +106,11 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA // perform strashing vNodes = Abc_AigDfs( pNtk, fAllNodes, 0 ); - if ( !pParams->fInternal ) + if ( !fInternal ) pProgress = Extra_ProgressBarStart( stdout, vNodes->nSize ); Vec_PtrForEachEntry( vNodes, pNode, i ) { - if ( !pParams->fInternal ) + if ( !fInternal ) Extra_ProgressBarUpdate( pProgress, i, NULL ); if ( pNode == pConst1 ) pNodeFraig = Fraig_ManReadConst1(pMan); @@ -123,7 +123,7 @@ Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fA assert( pNode->pCopy == NULL ); pNode->pCopy = (Abc_Obj_t *)pNodeFraig; } - if ( !pParams->fInternal ) + if ( !fInternal ) Extra_ProgressBarStop( pProgress ); Vec_PtrFree( vNodes ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 68dccd18..b6755a04 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -372,8 +372,8 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In Synopsis [Checks the status of the miter.] - Description [Return 1 if the miter is sat for at least one output. - Return 0 if the miter is unsat for all its outputs. Returns -1 if the + Description [Return 0 if the miter is sat for at least one output. + Return 1 if the miter is unsat for all its outputs. Returns -1 if the miter is undecided for some outputs.] SideEffects [] @@ -396,15 +396,15 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ) { // if the miter is constant 1, return immediately printf( "MITER IS CONSTANT 1!\n" ); - return 1; + return 0; } } // if the miter is undecided (or satisfiable), return immediately else return -1; } - // return 0, meaning all outputs are constant zero - return 0; + // return 1, meaning all outputs are constant zero + return 1; } /**Function************************************************************* diff --git a/src/base/abci/abcRefactor.c b/src/base/abci/abcRefactor.c index 92d497fc..3d9534c8 100644 --- a/src/base/abci/abcRefactor.c +++ b/src/base/abci/abcRefactor.c @@ -58,7 +58,7 @@ struct Abc_ManRef_t_ static void Abc_NtkManRefPrintStats( Abc_ManRef_t * p ); static Abc_ManRef_t * Abc_NtkManRefStart( int nNodeSizeMax, int nConeSizeMax, bool fUseDcs, bool fVerbose ); static void Abc_NtkManRefStop( Abc_ManRef_t * p ); -static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose ); +static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -80,7 +80,7 @@ static Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec SeeAlso [] ***********************************************************************/ -int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUseZeros, bool fUseDcs, bool fVerbose ) +int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ) { ProgressBar * pProgress; Abc_ManRef_t * pManRef; @@ -98,7 +98,9 @@ int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool pManCut = Abc_NtkManCutStart( nNodeSizeMax, nConeSizeMax, 2, 1000 ); pManRef = Abc_NtkManRefStart( nNodeSizeMax, nConeSizeMax, fUseDcs, fVerbose ); pManRef->vLeaves = Abc_NtkManCutReadCutLarge( pManCut ); - Abc_NtkStartReverseLevels( pNtk ); + // compute the reverse levels if level update is requested + if ( fUpdateLevel ) + Abc_NtkStartReverseLevels( pNtk ); // resynthesize each node once nNodes = Abc_NtkObjNumMax(pNtk); @@ -121,13 +123,13 @@ clk = clock(); pManRef->timeCut += clock() - clk; // evaluate this cut clk = clock(); - pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUseZeros, fUseDcs, fVerbose ); + pFForm = Abc_NodeRefactor( pManRef, pNode, vFanins, fUpdateLevel, fUseZeros, fUseDcs, fVerbose ); pManRef->timeRes += clock() - clk; if ( pFForm == NULL ) continue; // acceptable replacement found, update the graph clk = clock(); - Dec_GraphUpdateNetwork( pNode, pFForm, pManRef->nLastGain ); + Dec_GraphUpdateNetwork( pNode, pFForm, fUpdateLevel, pManRef->nLastGain ); pManRef->timeNtk += clock() - clk; Dec_GraphFree( pFForm ); } @@ -140,7 +142,13 @@ pManRef->timeTotal = clock() - clkStart; // delete the managers Abc_NtkManCutStop( pManCut ); Abc_NtkManRefStop( pManRef ); - Abc_NtkStopReverseLevels( pNtk ); + // put the nodes into the DFS order and reassign their IDs + Abc_NtkReassignIds( pNtk ); + // fix the levels + if ( fUpdateLevel ) + Abc_NtkStopReverseLevels( pNtk ); + else + Abc_NtkGetLevelNum( pNtk ); // check if ( !Abc_NtkCheck( pNtk ) ) { @@ -161,7 +169,7 @@ pManRef->timeTotal = clock() - clkStart; SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUseZeros, bool fUseDcs, bool fVerbose ) +Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vFanins, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ) { int fVeryVerbose = 0; Abc_Obj_t * pFanin; @@ -169,6 +177,9 @@ Dec_Graph_t * Abc_NodeRefactor( Abc_ManRef_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * DdNode * bNodeFunc; int nNodesSaved, nNodesAdded, i, clk; char * pSop; + int Required; + + Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY; p->nNodesConsidered++; @@ -239,7 +250,7 @@ p->timeFact += clock() - clk; // detect how many new nodes will be added (while taking into account reused nodes) clk = clock(); - nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Abc_NodeReadRequiredLevel(pNode) ); + nNodesAdded = Dec_GraphToNetworkCount( pNode, pFForm, nNodesSaved, Required ); p->timeEval += clock() - clk; // quit if there is no improvement if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !fUseZeros ) diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index 165777f8..ad91134e 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -486,7 +486,7 @@ void Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk ) Abc_ObjFanin1(pNode)->fMarkA == 0 ) nMuxes++; } - printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); +// printf( "The number of MUXes detected = %d (%5.2f %% of logic).\n", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); } /**Function************************************************************* diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index ea221296..81d97028 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -50,7 +50,7 @@ static void Abc_NodePrintCuts( Abc_Obj_t * pNode ); SeeAlso [] ***********************************************************************/ -int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose ) +int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose ) { int fDrop = 0; ProgressBar * pProgress; @@ -67,7 +67,9 @@ int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUseZeros, int fVerbose ) pManRwr = Rwr_ManStart( 0 ); if ( pManRwr == NULL ) return 0; - Abc_NtkStartReverseLevels( pNtk ); + // compute the reverse levels if level update is requested + if ( fUpdateLevel ) + Abc_NtkStartReverseLevels( pNtk ); // start the cut manager clk = clock(); pManCut = Abc_NtkStartCutManForRewrite( pNtk, fDrop ); @@ -90,14 +92,16 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk ); if ( Abc_ObjFanoutNum(pNode) > 1000 ) continue; // for each cut, try to resynthesize it - nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUseZeros ); + nGain = Rwr_NodeRewrite( pManRwr, pManCut, pNode, fUpdateLevel, fUseZeros ); if ( nGain > 0 || nGain == 0 && fUseZeros ) { Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr); int fCompl = Rwr_ManReadCompl(pManRwr); // complement the FF if needed if ( fCompl ) Dec_GraphComplement( pGraph ); - Dec_GraphUpdateNetwork( pNode, pGraph, nGain ); +clk = clock(); + Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, nGain ); +Rwr_ManAddTimeUpdate( pManRwr, clock() - clk ); if ( fCompl ) Dec_GraphComplement( pGraph ); } } @@ -110,7 +114,13 @@ Rwr_ManAddTimeTotal( pManRwr, clock() - clkStart ); Rwr_ManStop( pManRwr ); Cut_ManStop( pManCut ); pNtk->pManCut = NULL; - Abc_NtkStopReverseLevels( pNtk ); + // put the nodes into the DFS order and reassign their IDs + Abc_NtkReassignIds( pNtk ); + // fix the levels + if ( fUpdateLevel ) + Abc_NtkStopReverseLevels( pNtk ); + else + Abc_NtkGetLevelNum( pNtk ); // check if ( !Abc_NtkCheck( pNtk ) ) { diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 4fb059e5..b335086f 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -35,18 +35,18 @@ static void Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * Synopsis [Attempts to solve the miter using an internal SAT solver.] - Description [Returns 1 if the miter is SAT.] + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] SideEffects [] SeeAlso [] ***********************************************************************/ -bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ) +int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) { solver * pSat; lbool status; - int clk; + int RetValue, clk; assert( Abc_NtkIsBddLogic(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); @@ -57,20 +57,18 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ) // load clauses into the solver clk = clock(); pSat = Abc_NtkMiterSatCreate( pNtk ); -// printf( "Created SAT problem with %d variable and %d clauses. ", -// solver_nvars(pSat), solver_nclauses(pSat) ); +// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); // simplify the problem clk = clock(); status = solver_simplify(pSat); -// printf( "Simplified the problem to %d variables and %d clauses. ", -// solver_nvars(pSat), solver_nclauses(pSat) ); +// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); // PRT( "Time", clock() - clk ); if ( status == l_False ) { solver_delete( pSat ); - printf( "The problem is UNSAT after simplification.\n" ); + printf( "The problem is UNSATISFIABLE after simplification.\n" ); return 0; } @@ -78,17 +76,38 @@ bool Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int fVerbose ) clk = clock(); if ( fVerbose ) pSat->verbosity = 1; - status = solver_solve( pSat, NULL, NULL ); -// if ( fVerbose ) -// { - printf( "The problem is %5s. ", (status == l_True)? "SAT" : "UNSAT" ); - PRT( "SAT solver time", clock() - clk ); -// } + status = solver_solve( pSat, NULL, NULL, nSeconds ); + if ( status == l_Undef ) + { +// printf( "The problem timed out.\n" ); + RetValue = -1; + } + else if ( status == l_True ) + { +// printf( "The problem is SATISFIABLE.\n" ); + RetValue = 0; + } + else if ( status == l_False ) + { +// printf( "The problem is UNSATISFIABLE.\n" ); + RetValue = 1; + } + else + assert( 0 ); +// PRT( "SAT solver time", clock() - clk ); + + // if the problem is SAT, get the counterexample + if ( status == l_True ) + { + Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); + pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize ); + Vec_IntFree( vCiIds ); + } // free the solver solver_delete( pSat ); - return status == l_True; + return RetValue; } - + /**Function************************************************************* Synopsis [Sets up the SAT solver.] diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 7000ecad..fa840937 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -25,8 +25,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); - static stmm_table * Abc_NtkFraigEquiv( Fraig_Man_t * p, Abc_Ntk_t * pNtk, int fUseInv, bool fVerbose ); static void Abc_NtkFraigTransform( Abc_Ntk_t * pNtk, stmm_table * tEquiv, int fUseInv, bool fVerbose ); static void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fVerbose, int fUseInv ); diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 55d6cf7d..2d5493ea 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -25,6 +25,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ); +static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ); +static void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -40,7 +44,7 @@ SeeAlso [] ***********************************************************************/ -void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) +void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ) { Abc_Ntk_t * pMiter; Abc_Ntk_t * pCnf; @@ -54,13 +58,17 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) return; } RetValue = Abc_NtkMiterIsConstant( pMiter ); - if ( RetValue == 1 ) + if ( RetValue == 0 ) { Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); + Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); + FREE( pMiter->pModel ); return; } - if ( RetValue == 0 ) + if ( RetValue == 1 ) { Abc_NtkDelete( pMiter ); printf( "Networks are equivalent after structural hashing.\n" ); @@ -77,10 +85,16 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) } // solve the CNF using the SAT solver - if ( Abc_NtkMiterSat( pCnf, 0 ) ) + RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 ); + if ( RetValue == -1 ) + printf( "Networks are undecided (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) printf( "Networks are NOT EQUIVALENT after SAT.\n" ); else printf( "Networks are equivalent after SAT.\n" ); + if ( pCnf->pModel ) + Abc_NtkVerifyReportError( pNtk1, pNtk2, pCnf->pModel ); + FREE( pCnf->pModel ); Abc_NtkDelete( pCnf ); } @@ -96,11 +110,11 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) SeeAlso [] ***********************************************************************/ -void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose ) +void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ) { Fraig_Params_t Params; + Fraig_Man_t * pMan; Abc_Ntk_t * pMiter; - Abc_Ntk_t * pFraig; int RetValue; // get the miter of the two networks @@ -111,13 +125,17 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose ) return; } RetValue = Abc_NtkMiterIsConstant( pMiter ); - if ( RetValue == 1 ) + if ( RetValue == 0 ) { Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + // report the error + pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter ); + Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); + FREE( pMiter->pModel ); return; } - if ( RetValue == 0 ) + if ( RetValue == 1 ) { Abc_NtkDelete( pMiter ); printf( "Networks are equivalent after structural hashing.\n" ); @@ -127,21 +145,27 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose ) // convert the miter into a FRAIG Fraig_ParamsSetDefault( &Params ); Params.fVerbose = fVerbose; - pFraig = Abc_NtkFraig( pMiter, &Params, 0 ); - Abc_NtkDelete( pMiter ); - if ( pFraig == NULL ) - { - printf( "Fraiging has failed.\n" ); - return; - } - RetValue = Abc_NtkMiterIsConstant( pFraig ); - Abc_NtkDelete( pFraig ); - if ( RetValue == 0 ) - { + Params.nSeconds = nSeconds; + pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); + Fraig_ManProveMiter( pMan ); + + // analyze the result + RetValue = Fraig_ManCheckMiter( pMan ); + // report the result + if ( RetValue == -1 ) + printf( "Networks are undecided (SAT solver timed out on the final miter).\n" ); + else if ( RetValue == 1 ) printf( "Networks are equivalent after fraiging.\n" ); - return; + else if ( RetValue == 0 ) + { + printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); + Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) ); } - printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); + else assert( 0 ); + // delete the fraig manager + Fraig_ManFree( pMan ); + // delete the miter + Abc_NtkDelete( pMiter ); } /**Function************************************************************* @@ -155,7 +179,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fVerbose ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) +void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames ) { Abc_Ntk_t * pMiter; Abc_Ntk_t * pFrames; @@ -170,13 +194,13 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) return; } RetValue = Abc_NtkMiterIsConstant( pMiter ); - if ( RetValue == 1 ) + if ( RetValue == 0 ) { Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); return; } - if ( RetValue == 0 ) + if ( RetValue == 1 ) { Abc_NtkDelete( pMiter ); printf( "Networks are equivalent after structural hashing.\n" ); @@ -192,13 +216,13 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) return; } RetValue = Abc_NtkMiterIsConstant( pFrames ); - if ( RetValue == 1 ) + if ( RetValue == 0 ) { Abc_NtkDelete( pFrames ); printf( "Networks are NOT EQUIVALENT after framing.\n" ); return; } - if ( RetValue == 0 ) + if ( RetValue == 1 ) { Abc_NtkDelete( pFrames ); printf( "Networks are equivalent after framing.\n" ); @@ -215,7 +239,10 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) } // solve the CNF using the SAT solver - if ( Abc_NtkMiterSat( pCnf, 0 ) ) + RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 ); + if ( RetValue == -1 ) + printf( "Networks are undecided (SAT solver timed out).\n" ); + else if ( RetValue == 0 ) printf( "Networks are NOT EQUIVALENT after SAT.\n" ); else printf( "Networks are equivalent after SAT.\n" ); @@ -233,11 +260,11 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) SeeAlso [] ***********************************************************************/ -void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) +void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ) { Fraig_Params_t Params; + Fraig_Man_t * pMan; Abc_Ntk_t * pMiter; - Abc_Ntk_t * pFraig; Abc_Ntk_t * pFrames; int RetValue; @@ -249,13 +276,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) return; } RetValue = Abc_NtkMiterIsConstant( pMiter ); - if ( RetValue == 1 ) + if ( RetValue == 0 ) { Abc_NtkDelete( pMiter ); printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); return; } - if ( RetValue == 0 ) + if ( RetValue == 1 ) { Abc_NtkDelete( pMiter ); printf( "Networks are equivalent after structural hashing.\n" ); @@ -271,13 +298,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) return; } RetValue = Abc_NtkMiterIsConstant( pFrames ); - if ( RetValue == 1 ) + if ( RetValue == 0 ) { Abc_NtkDelete( pFrames ); printf( "Networks are NOT EQUIVALENT after framing.\n" ); return; } - if ( RetValue == 0 ) + if ( RetValue == 1 ) { Abc_NtkDelete( pFrames ); printf( "Networks are equivalent after framing.\n" ); @@ -286,23 +313,164 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames ) // convert the miter into a FRAIG Fraig_ParamsSetDefault( &Params ); - pFraig = Abc_NtkFraig( pFrames, &Params, 0 ); - Abc_NtkDelete( pFrames ); - if ( pFraig == NULL ) + Params.fVerbose = fVerbose; + Params.nSeconds = nSeconds; + pMan = Abc_NtkToFraig( pFrames, &Params, 0 ); + Fraig_ManProveMiter( pMan ); + + // analyze the result + RetValue = Fraig_ManCheckMiter( pMan ); + // report the result + if ( RetValue == -1 ) + printf( "Networks are undecided (SAT solver timed out on the final miter).\n" ); + else if ( RetValue == 1 ) + printf( "Networks are equivalent after fraiging.\n" ); + else if ( RetValue == 0 ) { - printf( "Fraiging has failed.\n" ); - return; + printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); +// Abc_NtkVerifyReportError( pNtk1, pNtk2, Fraig_ManReadModel(pMan) ); } - RetValue = Abc_NtkMiterIsConstant( pFraig ); - Abc_NtkDelete( pFraig ); - if ( RetValue == 0 ) + else assert( 0 ); + // delete the fraig manager + Fraig_ManFree( pMan ); + // delete the miter + Abc_NtkDelete( pFrames ); +} + +/**Function************************************************************* + + Synopsis [Reports mismatch between the two networks.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int * pValues1, * pValues2; + int nMisses, nPrinted, i, iNode = -1; + + assert( Abc_NtkCiNum(pNtk1) == Abc_NtkCiNum(pNtk2) ); + assert( Abc_NtkCoNum(pNtk1) == Abc_NtkCoNum(pNtk2) ); + // get the CO values under this model + pValues1 = Abc_NtkVerifySimulatePattern( pNtk1, pModel ); + pValues2 = Abc_NtkVerifySimulatePattern( pNtk2, pModel ); + // count the mismatches + nMisses = 0; + for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) + nMisses += (int)( pValues1[i] != pValues2[i] ); + printf( "Verification failed for %d outputs: ", nMisses ); + // print the first 3 outputs + nPrinted = 0; + for ( i = 0; i < Abc_NtkCoNum(pNtk1); i++ ) + if ( pValues1[i] != pValues2[i] ) + { + if ( iNode == -1 ) + iNode = i; + printf( " %s", Abc_ObjName(Abc_NtkCo(pNtk1,i)) ); + if ( ++nPrinted == 3 ) + break; + } + if ( nPrinted != nMisses ) + printf( " ..." ); + printf( "\n" ); + // report mismatch for the first output + if ( iNode >= 0 ) { - printf( "Networks are equivalent after fraiging.\n" ); - return; + printf( "Output %s: Value in Network1 = %d. Value in Network2 = %d.\n", + Abc_ObjName(Abc_NtkCo(pNtk1,iNode)), pValues1[iNode], pValues2[iNode] ); + printf( "Input pattern: " ); + // collect PIs in the cone + pNode = Abc_NtkCo(pNtk1,iNode); + vNodes = Abc_NtkNodeSupport( pNtk1, &pNode, 1 ); + // set the PI numbers + Abc_NtkForEachCi( pNtk1, pNode, i ) + pNode->pCopy = (void*)i; + // print the model + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + assert( Abc_ObjIsCi(pNode) ); + printf( " %s=%d", Abc_ObjName(pNode), pModel[(int)pNode->pCopy] ); + } + printf( "\n" ); + Vec_PtrFree( vNodes ); } - printf( "Networks are NOT EQUIVALENT after fraiging.\n" ); + free( pValues1 ); + free( pValues2 ); +} + +/**Function************************************************************* + + Synopsis [Returns a dummy pattern full of zeros.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk ) +{ + int * pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); + memset( pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) ); + return pModel; } +/**Function************************************************************* + + Synopsis [Returns the PO values under the given input pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNode; + int * pValues, Value0, Value1, i; + int fStrashed = 0; + if ( !Abc_NtkIsStrash(pNtk) ) + { + pNtk = Abc_NtkStrash(pNtk, 0, 0); + fStrashed = 1; + } + // increment the trav ID + Abc_NtkIncrementTravId( pNtk ); + // set the CI values + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->pCopy = (void *)pModel[i]; + // simulate in the topological order + vNodes = Abc_NtkDfs( pNtk, 1 ); + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + if ( Abc_NodeIsConst(pNode) ) + pNode->pCopy = NULL; + else + { + Value0 = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); + Value1 = ((int)Abc_ObjFanin1(pNode)->pCopy) ^ Abc_ObjFaninC1(pNode); + pNode->pCopy = (void *)(Value0 & Value1); + } + } + Vec_PtrFree( vNodes ); + // fill the output values + pValues = ALLOC( int, Abc_NtkCoNum(pNtk) ); + Abc_NtkForEachCo( pNtk, pNode, i ) + pValues[i] = ((int)Abc_ObjFanin0(pNode)->pCopy) ^ Abc_ObjFaninC0(pNode); + if ( fStrashed ) + Abc_NtkDelete( pNtk ); + return pValues; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abcs/abcSeq.c b/src/base/abcs/abcSeq.c index a41edac1..344417af 100644 --- a/src/base/abcs/abcSeq.c +++ b/src/base/abcs/abcSeq.c @@ -112,7 +112,7 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) if ( Abc_ObjIsCi(pFaninNew) || !Abc_NodeIsConst(pFaninNew) ) continue; pConst = Abc_ObjNotCond( Abc_AigConst1(pManNew), Abc_ObjFaninC0(pLatch) ); - Abc_AigReplace( pManNew, pLatch, pConst ); + Abc_AigReplace( pManNew, pLatch, pConst, 0 ); fChange = 1; Counter++; } diff --git a/src/base/main/main.c b/src/base/main/main.c index 0622a3bd..d44dade9 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -20,6 +20,9 @@ #include "mainInt.h" +// this line should be included in the library project +#define _LIB + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// @@ -30,6 +33,8 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s); /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// +#ifndef _LIB + /**Function************************************************************* Synopsis [The main() procedure.] @@ -64,8 +69,8 @@ int main( int argc, char * argv[] ) fInitRead = 0; fFinalWrite = 0; sInFile = sOutFile = NULL; - sprintf( sReadCmd, "read_blif_mv" ); - sprintf( sWriteCmd, "write_blif_mv" ); + sprintf( sReadCmd, "read" ); + sprintf( sWriteCmd, "write" ); util_getopt_reset(); while ((c = util_getopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) { @@ -226,6 +231,62 @@ usage: return 1; } +#endif + +/**Function************************************************************* + + Synopsis [Initialization procedure for the library project.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_Start() +{ + Abc_Frame_t * pAbc; + + // added to detect memory leaks: +#ifdef _DEBUG + _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); +#endif + + // get global frame (singleton pattern) + // will be initialized on first call + pAbc = Abc_FrameGetGlobalFrame(); + + // source the resource file + Abc_UtilsSource( pAbc ); +} + +/**Function************************************************************* + + Synopsis [Deallocation procedure for the library project.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_Stop() +{ + Abc_Frame_t * pAbc; + int fStatus = 0; + + // if the memory should be freed, quit packages + if ( fStatus == -2 ) + { + pAbc = Abc_FrameGetGlobalFrame(); + // perform uninitializations + Abc_FrameEnd( pAbc ); + // stop the framework + Abc_FrameDeallocate( pAbc ); + } +} /**Function******************************************************************** diff --git a/src/base/main/main.h b/src/base/main/main.h index 0d47dec5..6a2db817 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -73,7 +73,11 @@ typedef struct Abc_Frame_t_ Abc_Frame_t; /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// -/*=== mvFrame.c ===========================================================*/ +/*=== main.c ===========================================================*/ +extern void Abc_Start(); +extern void Abc_Stop(); + +/*=== mainFrame.c ===========================================================*/ extern Abc_Ntk_t * Abc_FrameReadNet( Abc_Frame_t * p ); extern FILE * Abc_FrameReadOut( Abc_Frame_t * p ); extern FILE * Abc_FrameReadErr( Abc_Frame_t * p ); |