diff options
Diffstat (limited to 'src')
43 files changed, 983 insertions, 239 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 ); diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h index 6ecc9678..783655fa 100644 --- a/src/opt/dec/dec.h +++ b/src/opt/dec/dec.h @@ -97,7 +97,7 @@ struct Dec_Man_t_ /*=== decAbc.c ========================================================*/ extern Abc_Obj_t * Dec_GraphToNetwork( Abc_Aig_t * pMan, Dec_Graph_t * pGraph ); extern int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); -extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ); +extern void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain ); /*=== decFactor.c ========================================================*/ extern Dec_Graph_t * Dec_Factor( char * pSop ); /*=== decMan.c ========================================================*/ diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c index 9931b136..62f90889 100644 --- a/src/opt/dec/decAbc.c +++ b/src/opt/dec/decAbc.c @@ -126,7 +126,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa else if ( Abc_ObjRegular(pAnd) == Abc_ObjRegular(pAnd1) ) LevelNew = (int)Abc_ObjRegular(pAnd1)->Level; LevelOld = (int)Abc_ObjRegular(pAnd)->Level; - assert( LevelNew == LevelOld ); +// assert( LevelNew == LevelOld ); } if ( LevelNew > LevelMax ) return -1; @@ -148,7 +148,7 @@ int Dec_GraphToNetworkCount( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMa SeeAlso [] ***********************************************************************/ -void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ) +void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpdateLevel, int nGain ) { Abc_Obj_t * pRootNew; Abc_Ntk_t * pNtk = pRoot->pNtk; @@ -157,7 +157,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain // create the new structure of nodes pRootNew = Dec_GraphToNetwork( pNtk->pManFunc, pGraph ); // remove the old nodes - Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew ); + Abc_AigReplace( pNtk->pManFunc, pRoot, pRootNew, fUpdateLevel ); // compare the gains nNodesNew = Abc_NtkNodeNum(pNtk); assert( nGain <= nNodesOld - nNodesNew ); diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h index 6d1a6c06..1467ce7a 100644 --- a/src/opt/rwr/rwr.h +++ b/src/opt/rwr/rwr.h @@ -49,6 +49,7 @@ struct Rwr_Man_t_ char * pPhases; // canonical phases char * pPerms; // canonical permutations unsigned char * pMap; // mapping of functions into class numbers + unsigned short * pMapInv; // mapping of classes into functions char * pPractical; // practical NPN classes char ** pPerms4; // four-var permutations // node space @@ -63,10 +64,11 @@ struct Rwr_Man_t_ int nClasses; // the number of NN classes // the result of resynthesis int fCompl; // indicates if the output of FF should be complemented - void * pGraph; // the decomposition tree (temporary) + void * pGraph; // the decomposition tree (temporary) Vec_Ptr_t * vFanins; // the fanins array (temporary) Vec_Ptr_t * vFaninsCur; // the fanins array (temporary) Vec_Int_t * vLevNums; // the array of levels (temporary) + Vec_Ptr_t * vNodesTemp; // the nodes in MFFC (temporary) // node statistics int nNodesConsidered; int nNodesRewritten; @@ -80,6 +82,8 @@ struct Rwr_Man_t_ int timeCut; int timeRes; int timeEval; + int timeMffc; + int timeUpdate; int timeTotal; }; @@ -114,7 +118,7 @@ static inline Rwr_Node_t * Rwr_NotCond( Rwr_Node_t * p, int c ) { return (Rwr_N /*=== rwrDec.c ========================================================*/ extern void Rwr_ManPreprocess( Rwr_Man_t * p ); /*=== rwrEva.c ========================================================*/ -extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros ); +extern int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros ); /*=== rwrLib.c ========================================================*/ extern void Rwr_ManPrecompute( Rwr_Man_t * p ); extern Rwr_Node_t * Rwr_ManAddVar( Rwr_Man_t * p, unsigned uTruth, int fPrecompute ); @@ -128,6 +132,7 @@ extern void Rwr_ManPrintStats( Rwr_Man_t * p ); extern void * Rwr_ManReadDecs( Rwr_Man_t * p ); extern int Rwr_ManReadCompl( Rwr_Man_t * p ); extern void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time ); +extern void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time ); extern void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time ); /*=== rwrPrint.c ========================================================*/ extern void Rwr_ManPrint( Rwr_Man_t * p ); diff --git a/src/opt/rwr/rwrDec.c b/src/opt/rwr/rwrDec.c index d072879d..a7f55a90 100644 --- a/src/opt/rwr/rwrDec.c +++ b/src/opt/rwr/rwrDec.c @@ -49,6 +49,8 @@ void Rwr_ManPreprocess( Rwr_Man_t * p ) Rwr_Node_t * pNode; int i, k; // put the nodes into the structure + p->pMapInv = ALLOC( unsigned short, 222 ); + memset( p->pMapInv, 0, sizeof(unsigned short) * 222 ); p->vClasses = Vec_VecStart( 222 ); for ( i = 0; i < p->nFuncs; i++ ) { @@ -60,6 +62,7 @@ void Rwr_ManPreprocess( Rwr_Man_t * p ) assert( pNode->uTruth == p->pTable[i]->uTruth ); assert( p->pMap[pNode->uTruth] >= 0 && p->pMap[pNode->uTruth] < 222 ); Vec_VecPush( p->vClasses, p->pMap[pNode->uTruth], pNode ); + p->pMapInv[ p->pMap[pNode->uTruth] ] = p->puCanons[pNode->uTruth]; } } // compute decomposition forms for each node and verify them diff --git a/src/opt/rwr/rwrEva.c b/src/opt/rwr/rwrEva.c index c934dfd8..8a00cec8 100644 --- a/src/opt/rwr/rwrEva.c +++ b/src/opt/rwr/rwrEva.c @@ -49,7 +49,7 @@ static Dec_Graph_t * Rwr_CutEvaluate( Rwr_Man_t * p, Abc_Obj_t * pRoot, Cut_Cut_ SeeAlso [] ***********************************************************************/ -int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUseZeros ) +int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int fUpdateLevel, int fUseZeros ) { int fVeryVerbose = 0; Dec_Graph_t * pGraph; @@ -63,7 +63,7 @@ int Rwr_NodeRewrite( Rwr_Man_t * p, Cut_Man_t * pManCut, Abc_Obj_t * pNode, int p->nNodesConsidered++; // get the required times - Required = Abc_NodeReadRequiredLevel( pNode ); + Required = fUpdateLevel? Abc_NodeReadRequiredLevel(pNode) : ABC_INFINITY; // get the node's cuts clk = clock(); pCut = (Cut_Cut_t *)Abc_NodeGetCutsRecursive( pManCut, pNode ); @@ -98,6 +98,7 @@ clk = clock(); } p->nCutsGood++; +clk2 = clock(); // mark the fanin boundary Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Abc_ObjRegular(pFanin)->vFanouts.nSize++; @@ -107,6 +108,7 @@ clk = clock(); // unmark the fanin boundary Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Abc_ObjRegular(pFanin)->vFanouts.nSize--; +p->timeMffc += clock() - clk2; // evaluate the cut clk2 = clock(); diff --git a/src/opt/rwr/rwrMan.c b/src/opt/rwr/rwrMan.c index a21dd520..bfeaa273 100644 --- a/src/opt/rwr/rwrMan.c +++ b/src/opt/rwr/rwrMan.c @@ -75,6 +75,7 @@ clk = clock(); p->vLevNums = Vec_IntAlloc( 50 ); p->vFanins = Vec_PtrAlloc( 50 ); p->vFaninsCur = Vec_PtrAlloc( 50 ); + p->vNodesTemp = Vec_PtrAlloc( 50 ); if ( fPrecompute ) { // precompute subgraphs Rwr_ManPrecompute( p ); @@ -112,11 +113,13 @@ void Rwr_ManStop( Rwr_Man_t * p ) Dec_GraphFree( (Dec_Graph_t *)pNode->pNext ); } if ( p->vClasses ) Vec_VecFree( p->vClasses ); + Vec_PtrFree( p->vNodesTemp ); Vec_PtrFree( p->vForest ); Vec_IntFree( p->vLevNums ); Vec_PtrFree( p->vFanins ); Vec_PtrFree( p->vFaninsCur ); Extra_MmFixedStop( p->pMmNode, 0 ); + FREE( p->pMapInv ); free( p->pTable ); free( p->pPractical ); free( p->pPerms4 ); @@ -151,14 +154,16 @@ void Rwr_ManPrintStats( Rwr_Man_t * p ) PRT( "Start ", p->timeStart ); PRT( "Cuts ", p->timeCut ); PRT( "Resynthesis ", p->timeRes ); + PRT( " Mffc ", p->timeMffc ); PRT( " Eval ", p->timeEval ); + PRT( "Update ", p->timeUpdate ); PRT( "TOTAL ", p->timeTotal ); /* - printf( "The scores are : " ); + printf( "The scores are:\n" ); for ( i = 0; i < 222; i++ ) if ( p->nScores[i] > 0 ) - printf( "%d=%d ", i, p->nScores[i] ); + printf( "%3d = %8d canon = %5d\n", i, p->nScores[i], p->pMapInv[i] ); printf( "\n" ); */ } @@ -222,6 +227,22 @@ void Rwr_ManAddTimeCuts( Rwr_Man_t * p, int Time ) SeeAlso [] ***********************************************************************/ +void Rwr_ManAddTimeUpdate( Rwr_Man_t * p, int Time ) +{ + p->timeUpdate += Time; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Rwr_ManAddTimeTotal( Rwr_Man_t * p, int Time ) { p->timeTotal += Time; diff --git a/src/opt/rwr/rwrPrint.c b/src/opt/rwr/rwrPrint.c index 30c99f00..9011ce56 100644 --- a/src/opt/rwr/rwrPrint.c +++ b/src/opt/rwr/rwrPrint.c @@ -79,6 +79,33 @@ void Rwr_GetBushVolume( Rwr_Man_t * p, int Entry, int * pVolume, int * pnFuncs ) /**Function************************************************************* + Synopsis [Adds the node to the end of the list.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Rwr_GetBushSumOfVolumes( Rwr_Man_t * p, int Entry ) +{ + Rwr_Node_t * pNode; + int Volume, VolumeTotal = 0; + for ( pNode = p->pTable[Entry]; pNode; pNode = pNode->pNext ) + { + if ( pNode->uTruth != p->puCanons[pNode->uTruth] ) + continue; + Volume = 0; + Rwr_ManIncTravId( p ); + Rwr_Trav2_rec( p, pNode, &Volume ); + VolumeTotal += Volume; + } + return VolumeTotal; +} + +/**Function************************************************************* + Synopsis [Prints one rwr node.] Description [] @@ -219,9 +246,9 @@ void Rwr_ManPrint( Rwr_Man_t * p ) continue; if ( i != p->puCanons[i] ) continue; - fprintf( pFile, "\nClass %3d. Func %6d. ", p->pMap[i], Counter++ ); + fprintf( pFile, "\nClass %3d. Func %6d. ", p->pMap[i], Counter++ ); Rwr_GetBushVolume( p, i, &Volume, &nFuncs ); - fprintf( pFile, "Functions = %2d. Volume = %2d. ", nFuncs, Volume ); + fprintf( pFile, "Roots = %3d. Vol = %3d. Sum = %3d. ", nFuncs, Volume, Rwr_GetBushSumOfVolumes(p, i) ); uTruth = i; Extra_PrintBinary( pFile, &uTruth, 16 ); fprintf( pFile, "\n" ); diff --git a/src/opt/sim/simSupp.c b/src/opt/sim/simSupp.c index 576e19cc..d805da72 100644 --- a/src/opt/sim/simSupp.c +++ b/src/opt/sim/simSupp.c @@ -35,8 +35,6 @@ static void Sim_UtilAssignFromFifo( Sim_Man_t * p ); static void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int nCounters ); static int Sim_SolveSuppModelVerify( Abc_Ntk_t * pNtk, int * pModel, int Input, int Output ); -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// //////////////////////////////////////////////////////////////////////// @@ -469,6 +467,7 @@ void Sim_SolveTargetsUsingSat( Sim_Man_t * p, int Limit ) // transform the miter into a fraig Fraig_ParamsSetDefault( &Params ); + Params.nSeconds = ABC_INFINITY; Params.fInternal = 1; clk = clock(); pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); diff --git a/src/opt/sim/simSymSat.c b/src/opt/sim/simSymSat.c index db9917b3..a98d4b5e 100644 --- a/src/opt/sim/simSymSat.c +++ b/src/opt/sim/simSymSat.c @@ -26,8 +26,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -extern int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern ); -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); +static int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * pPattern ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFITIONS /// @@ -145,6 +144,7 @@ int Sim_SymmsSatProveOne( Sym_Man_t * p, int Out, int Var1, int Var2, unsigned * Params.fInternal = 1; Params.nPatsRand = 512; Params.nPatsDyna = 512; + Params.nSeconds = ABC_INFINITY; clk = clock(); pMan = Abc_NtkToFraig( pMiter, &Params, 0 ); diff --git a/src/sat/asat/added.c b/src/sat/asat/added.c index d7f5b104..d7358749 100644 --- a/src/sat/asat/added.c +++ b/src/sat/asat/added.c @@ -119,6 +119,30 @@ void Asat_ClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) fprintf( pFile, "\n" ); } +/**Function************************************************************* + + Synopsis [Returns a counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * solver_get_model( solver * p, int * pVars, int nVars ) +{ + int * pModel; + int i; + pModel = ALLOC( int, nVars ); + for ( i = 0; i < nVars; i++ ) + { + assert( pVars[i] >= 0 && pVars[i] < p->size ); + pModel[i] = (int)(p->model.ptr[pVars[i]] == (void *)l_True); + } + return pModel; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/asat/solver.c b/src/sat/asat/solver.c index c9dadcb4..98024a7f 100644 --- a/src/sat/asat/solver.c +++ b/src/sat/asat/solver.c @@ -22,6 +22,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include <stdio.h> #include <assert.h> #include <math.h> +#include <time.h> #include "solver.h" @@ -1055,13 +1056,14 @@ bool solver_simplify(solver* s) } -bool solver_solve(solver* s, lit* begin, lit* end) +int solver_solve(solver* s, lit* begin, lit* end, int nSeconds) { double nof_conflicts = 100; double nof_learnts = solver_nclauses(s) / 3; lbool status = l_Undef; lbool* values = s->assigns; lit* i; + int timeStart = clock(); for (i = begin; i < end; i++) if ((lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]) == l_False || (assume(s,*i), solver_propagate(s) != 0)){ @@ -1096,12 +1098,15 @@ bool solver_solve(solver* s, lit* begin, lit* end) status = solver_search(s,(int)nof_conflicts, (int)nof_learnts); nof_conflicts *= 1.5; nof_learnts *= 1.1; + // if the runtime limit is exceeded, quit the restart loop + if ( clock() - timeStart >= nSeconds * CLOCKS_PER_SEC ) + break; } if (s->verbosity >= 1) printf("==============================================================================\n"); solver_canceluntil(s,0); - return status != l_False; + return status; } diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h index e04d5780..f328fad5 100644 --- a/src/sat/asat/solver.h +++ b/src/sat/asat/solver.h @@ -69,7 +69,8 @@ extern void solver_delete(solver* s); extern bool solver_addclause(solver* s, lit* begin, lit* end); extern bool solver_simplify(solver* s); -extern bool solver_solve(solver* s, lit* begin, lit* end); +extern int solver_solve(solver* s, lit* begin, lit* end, int nSeconds); +extern int * solver_get_model( solver * p, int * pVars, int nVars ); extern int solver_nvars(solver* s); extern int solver_nclauses(solver* s); diff --git a/src/sat/csat/csat_apis.c b/src/sat/csat/csat_apis.c index b030caef..4481297a 100644 --- a/src/sat/csat/csat_apis.c +++ b/src/sat/csat/csat_apis.c @@ -24,6 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define ABC_DEFAULT_TIMEOUT 60 // 60 seconds + struct CSAT_ManagerStruct_t { // information about the problem @@ -33,7 +35,8 @@ struct CSAT_ManagerStruct_t Abc_Ntk_t * pTarget; // the AIG representing the target char * pDumpFileName; // the name of the file to dump the target network // solving parameters - int mode; // 0 = baseline; 1 = resource-aware fraiging + int mode; // 0 = brute-force SAT; 1 = resource-aware FRAIG + int nSeconds; // time limit for pure SAT solving Fraig_Params_t Params; // the set of parameters to call FRAIG package // information about the target int nog; // the numbers of gates in the target @@ -44,11 +47,9 @@ struct CSAT_ManagerStruct_t }; static CSAT_Target_ResultT * CSAT_TargetResAlloc( int nVars ); -static void CSAT_TargetResFree( CSAT_Target_ResultT * p ); static char * CSAT_GetNodeName( CSAT_Manager mng, Abc_Obj_t * pNode ); // some external procedures -extern Fraig_Man_t * Abc_NtkToFraig( Abc_Ntk_t * pNtk, Fraig_Params_t * pParams, int fAllNodes ); extern int Io_WriteBench( Abc_Ntk_t * pNtk, char * FileName ); //////////////////////////////////////////////////////////////////////// @@ -77,6 +78,7 @@ CSAT_Manager CSAT_InitManager() mng->tNode2Name = stmm_init_table(stmm_ptrcmp, stmm_ptrhash); mng->vNodes = Vec_PtrAlloc( 100 ); mng->vValues = Vec_IntAlloc( 100 ); + mng->nSeconds = ABC_DEFAULT_TIMEOUT; return mng; } @@ -107,7 +109,7 @@ void CSAT_QuitManager( CSAT_Manager mng ) Synopsis [Sets solver options for learning.] - Description [0 = baseline; 1 = resource-aware solving.] + Description [0 = brute-force SAT; 1 = resource-aware FRAIG.] SideEffects [] @@ -118,11 +120,11 @@ void CSAT_SetSolveOption( CSAT_Manager mng, enum CSAT_OptionT option ) { mng->mode = option; if ( option == 0 ) - printf( "CSAT_SetSolveOption: Setting baseline solving mode.\n" ); + printf( "CSAT_SetSolveOption: Setting brute-force SAT mode.\n" ); else if ( option == 1 ) - printf( "CSAT_SetSolveOption: Setting resource-aware solving mode.\n" ); + printf( "CSAT_SetSolveOption: Setting resource-aware FRAIG mode.\n" ); else - printf( "CSAT_SetSolveOption: Unknown option.\n" ); + printf( "CSAT_SetSolveOption: Unknown solving mode.\n" ); } @@ -280,7 +282,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) assert( Abc_NtkLatchNum(pNtk) == 0 ); // make sure everything is okay with the network structure - if ( !Abc_NtkCheckRead( pNtk ) ) + if ( !Abc_NtkDoCheck( pNtk ) ) { printf( "CSAT_Check_Integrity: The internal network check has failed.\n" ); return 0; @@ -311,7 +313,7 @@ int CSAT_Check_Integrity( CSAT_Manager mng ) ***********************************************************************/ void CSAT_SetTimeLimit( CSAT_Manager mng, int runtime ) { - printf( "CSAT_SetTimeLimit: The resource limit is not implemented (warning).\n" ); + mng->nSeconds = runtime; } /**Function************************************************************* @@ -458,7 +460,8 @@ void CSAT_SolveInit( CSAT_Manager mng ) memset( pParams, 0, sizeof(Fraig_Params_t) ); pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info - pParams->nBTLimit = 99; // the max number of backtracks to perform at a node + pParams->nBTLimit = 10; // the max number of backtracks to perform at a node + pParams->nSeconds = mng->nSeconds; // the time out for the final proof pParams->fFuncRed = mng->mode; // performs only one level hashing pParams->fFeedBack = 1; // enables solver feedback pParams->fDist1Pats = 1; // enables distance-1 patterns @@ -498,6 +501,7 @@ void CSAT_AnalyzeTargets( CSAT_Manager mng ) enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) { Fraig_Man_t * pMan; + Abc_Ntk_t * pCnf; int * pModel; int RetValue, i; @@ -505,34 +509,68 @@ enum CSAT_StatusT CSAT_Solve( CSAT_Manager mng ) if ( mng->pTarget == NULL ) { printf( "CSAT_Solve: Target network is not derived by CSAT_SolveInit().\n" ); return UNDETERMINED; } - // transform the target into a fraig - pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); - Fraig_ManProveMiter( pMan ); - - // analyze the result - mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); - RetValue = Fraig_ManCheckMiter( pMan ); - if ( RetValue == -1 ) - mng->pResult->status = UNDETERMINED; - else if ( RetValue == 1 ) - mng->pResult->status = UNSATISFIABLE; - else if ( RetValue == 0 ) + // optimizations of the target go here + // for example, to enable one pass of rewriting, uncomment this line +// Abc_NtkRewrite( mng->pTarget, 0, 1, 0 ); + + if ( mng->mode == 0 ) // brute-force SAT + { + // transfor the AIG into a logic network for efficient CNF construction + pCnf = Abc_NtkRenode( mng->pTarget, 0, 100, 1, 0, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, mng->nSeconds, 0 ); + + // analyze the result + mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + if ( RetValue == -1 ) + mng->pResult->status = UNDETERMINED; + else if ( RetValue == 1 ) + mng->pResult->status = UNSATISFIABLE; + else if ( RetValue == 0 ) + { + mng->pResult->status = SATISFIABLE; + // create the array of PI names and values + for ( i = 0; i < mng->pResult->no_sig; i++ ) + { + mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given + mng->pResult->values[i] = pCnf->pModel[i]; + } + FREE( mng->pTarget->pModel ); + } + else assert( 0 ); + Abc_NtkDelete( pCnf ); + } + else if ( mng->mode == 1 ) // resource-aware fraiging { - mng->pResult->status = SATISFIABLE; - pModel = Fraig_ManReadModel( pMan ); - assert( pModel != NULL ); - // create the array of PI names and values - for ( i = 0; i < mng->pResult->no_sig; i++ ) + // transform the target into a fraig + pMan = Abc_NtkToFraig( mng->pTarget, &mng->Params, 0 ); + Fraig_ManProveMiter( pMan ); + RetValue = Fraig_ManCheckMiter( pMan ); + + // analyze the result + mng->pResult = CSAT_TargetResAlloc( Abc_NtkCiNum(mng->pTarget) ); + if ( RetValue == -1 ) + mng->pResult->status = UNDETERMINED; + else if ( RetValue == 1 ) + mng->pResult->status = UNSATISFIABLE; + else if ( RetValue == 0 ) { - mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given - mng->pResult->values[i] = pModel[i]; + mng->pResult->status = SATISFIABLE; + pModel = Fraig_ManReadModel( pMan ); + assert( pModel != NULL ); + // create the array of PI names and values + for ( i = 0; i < mng->pResult->no_sig; i++ ) + { + mng->pResult->names[i] = CSAT_GetNodeName(mng, Abc_NtkCi(mng->pNtk, i)); // returns the same string that was given + mng->pResult->values[i] = pModel[i]; + } } + else assert( 0 ); + // delete the fraig manager + Fraig_ManFree( pMan ); } - else + else assert( 0 ); - // delete the fraig manager - Fraig_ManFree( pMan ); // delete the target Abc_NtkDelete( mng->pTarget ); mng->pTarget = NULL; @@ -558,9 +596,9 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) /**Function************************************************************* - Synopsis [Dumps the target AIG into the BENCH file.] + Synopsis [Dumps the original network into the BENCH file.] - Description [] + Description [This procedure should be modified to dump the target.] SideEffects [] @@ -569,11 +607,13 @@ CSAT_Target_ResultT * CSAT_Get_Target_Result( CSAT_Manager mng, int TargetID ) ***********************************************************************/ void CSAT_Dump_Bench_File( CSAT_Manager mng ) { - Abc_Ntk_t * pNtkTemp; + Abc_Ntk_t * pNtkTemp, * pNtkAig; char * pFileName; - + // derive the netlist - pNtkTemp = Abc_NtkLogicToNetlistBench( mng->pTarget ); + pNtkAig = Abc_NtkStrash( mng->pNtk, 0, 0 ); + pNtkTemp = Abc_NtkLogicToNetlistBench( pNtkAig ); + Abc_NtkDelete( pNtkAig ); if ( pNtkTemp == NULL ) { printf( "CSAT_Dump_Bench_File: Dumping BENCH has failed.\n" ); return; } pFileName = mng->pDumpFileName? mng->pDumpFileName: "abc_test.bench"; diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h index 124ca266..4ac5a6a3 100644 --- a/src/sat/csat/csat_apis.h +++ b/src/sat/csat/csat_apis.h @@ -167,6 +167,10 @@ extern enum CSAT_StatusT CSAT_Solve(CSAT_Manager mng); extern CSAT_Target_ResultT * CSAT_Get_Target_Result(CSAT_Manager mng, int TargetID); extern void CSAT_Dump_Bench_File(CSAT_Manager mng); +// ADDED PROCEDURES: +extern void CSAT_QuitManager( CSAT_Manager mng ); +extern void CSAT_TargetResFree( CSAT_Target_ResultT * p ); + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h index 901bbac9..75dfb812 100644 --- a/src/sat/fraig/fraig.h +++ b/src/sat/fraig/fraig.h @@ -43,6 +43,7 @@ struct Fraig_ParamsStruct_t_ int nPatsRand; // the number of words of random simulation info int nPatsDyna; // the number of words of dynamic simulation info int nBTLimit; // the max number of backtracks to perform + int nSeconds; // the timeout for the final proof int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables distance-1 patterns @@ -162,8 +163,8 @@ extern int Fraig_CheckTfi( Fraig_Man_t * pMan, Fraig_Node_t * pO extern int Fraig_CountLevels( Fraig_Man_t * pMan ); /*=== fraigSat.c =============================================================*/ -extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ); -extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ); +extern int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ); +extern int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ); extern void Fraig_ManProveMiter( Fraig_Man_t * p ); extern int Fraig_ManCheckMiter( Fraig_Man_t * p ); diff --git a/src/sat/fraig/fraigCanon.c b/src/sat/fraig/fraigCanon.c index 5a7d0563..a8d6c3af 100644 --- a/src/sat/fraig/fraigCanon.c +++ b/src/sat/fraig/fraigCanon.c @@ -167,7 +167,7 @@ Fraig_Node_t * Fraig_NodeAndCanon( Fraig_Man_t * pMan, Fraig_Node_t * p1, Fraig_ // there is another node which looks the same according to simulation // use SAT to resolve the ambiguity - if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit ) ) + if ( Fraig_NodeIsEquivalent( pMan, pNodeOld, pNodeNew, pMan->nBTLimit, 1000000 ) ) { // set the node to be equivalent with this node // to prevent loops, only set if the old node is not in the TFI of the new node diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h index 131b750c..f14fb4c1 100644 --- a/src/sat/fraig/fraigInt.h +++ b/src/sat/fraig/fraigInt.h @@ -143,6 +143,7 @@ struct Fraig_ManStruct_t_ int nWordsRand; // the number of words of random simulation info int nWordsDyna; // the number of words of dynamic simulation info int nBTLimit; // the max number of backtracks to perform + int nSeconds; // the runtime limit for the miter proof int fFuncRed; // performs only one level hashing int fFeedBack; // enables solver feedback int fDist1Pats; // enables solver feedback diff --git a/src/sat/fraig/fraigMan.c b/src/sat/fraig/fraigMan.c index e5979c93..aa7e5999 100644 --- a/src/sat/fraig/fraigMan.c +++ b/src/sat/fraig/fraigMan.c @@ -46,6 +46,7 @@ void Fraig_ParamsSetDefault( Fraig_Params_t * pParams ) pParams->nPatsRand = FRAIG_PATTERNS_RANDOM; // the number of words of random simulation info pParams->nPatsDyna = FRAIG_PATTERNS_DYNAMIC; // the number of words of dynamic simulation info pParams->nBTLimit = 99; // the max number of backtracks to perform + pParams->nSeconds = 20; // the max number of seconds to solve the miter pParams->fFuncRed = 1; // performs only one level hashing pParams->fFeedBack = 1; // enables solver feedback pParams->fDist1Pats = 1; // enables distance-1 patterns @@ -100,6 +101,7 @@ Fraig_Man_t * Fraig_ManCreate( Fraig_Params_t * pParams ) p->nWordsRand = FRAIG_NUM_WORDS( pParams->nPatsRand ); // the number of words of random simulation info p->nWordsDyna = FRAIG_NUM_WORDS( pParams->nPatsDyna ); // the number of patterns for dynamic simulation info p->nBTLimit = pParams->nBTLimit; // -1 means infinite backtrack limit + p->nSeconds = pParams->nSeconds; // the timeout for the final miter p->fFuncRed = pParams->fFuncRed; // enables functional reduction (otherwise, only one-level hashing is performed) p->fFeedBack = pParams->fFeedBack; // enables solver feedback (the use of counter-examples in simulation) p->fDist1Pats = pParams->fDist1Pats; // enables solver feedback (the use of counter-examples in simulation) diff --git a/src/sat/fraig/fraigSat.c b/src/sat/fraig/fraigSat.c index 17201e58..fcb1018f 100644 --- a/src/sat/fraig/fraigSat.c +++ b/src/sat/fraig/fraigSat.c @@ -56,13 +56,13 @@ extern void * Msat_ClauseVecReadEntry( void * p, int i ); SeeAlso [] ***********************************************************************/ -int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit ) +int Fraig_NodesAreEqual( Fraig_Man_t * p, Fraig_Node_t * pNode1, Fraig_Node_t * pNode2, int nBTLimit, int nTimeLimit ) { if ( pNode1 == pNode2 ) return 1; if ( pNode1 == Fraig_Not(pNode2) ) return 0; - return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit ); + return Fraig_NodeIsEquivalent( p, Fraig_Regular(pNode1), Fraig_Regular(pNode2), nBTLimit, nTimeLimit ); } /**Function************************************************************* @@ -95,7 +95,7 @@ void Fraig_ManProveMiter( Fraig_Man_t * p ) // skip nodes that are different according to simulation if ( !Fraig_CompareSimInfo( pNode, p->pConst1, p->nWordsRand, 1 ) ) continue; - if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1 ) ) + if ( Fraig_NodeIsEquivalent( p, p->pConst1, pNode, -1, p->nSeconds ) ) { if ( Fraig_IsComplement(p->vOutputs->pArray[i]) ) p->vOutputs->pArray[i] = Fraig_Not(p->pConst1); @@ -160,7 +160,7 @@ int Fraig_ManCheckMiter( Fraig_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit ) +int Fraig_NodeIsEquivalent( Fraig_Man_t * p, Fraig_Node_t * pOld, Fraig_Node_t * pNew, int nBTLimit, int nTimeLimit ) { int RetValue, RetValue1, i, fComp, clk; int fVerbose = 0; @@ -227,7 +227,7 @@ if ( fVerbose ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); // run the solver clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) @@ -286,7 +286,7 @@ p->time3 += clock() - clk; Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, fComp) ); // run the solver clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, nTimeLimit ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) { @@ -411,7 +411,7 @@ if ( fVerbose ) Msat_IntVecPush( p->vProj, MSAT_VAR2LIT(pNew->Num, !fComp) ); // run the solver clk = clock(); - RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit ); + RetValue1 = Msat_SolverSolve( p->pSat, p->vProj, nBTLimit, 1000000 ); p->timeSat += clock() - clk; if ( RetValue1 == MSAT_FALSE ) diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h index 21ddcb81..8cbbea97 100644 --- a/src/sat/msat/msat.h +++ b/src/sat/msat/msat.h @@ -79,7 +79,7 @@ extern bool Msat_SolverParseDimacs( FILE * pFile, Msat_Solver_t ** p extern bool Msat_SolverAddVar( Msat_Solver_t * p ); extern bool Msat_SolverAddClause( Msat_Solver_t * p, Msat_IntVec_t * pLits ); extern bool Msat_SolverSimplifyDB( Msat_Solver_t * p ); -extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit ); +extern bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * pVecAssumps, int nBackTrackLimit, int nTimeLimit ); // printing stats, assignments, and clauses extern void Msat_SolverPrintStats( Msat_Solver_t * p ); extern void Msat_SolverPrintAssignment( Msat_Solver_t * p ); diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c index b8d9f328..6a1a1ae7 100644 --- a/src/sat/msat/msatSolverCore.c +++ b/src/sat/msat/msatSolverCore.c @@ -131,11 +131,12 @@ void Msat_SolverPrintStats( Msat_Solver_t * p ) SeeAlso [] ***********************************************************************/ -bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit ) +bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTrackLimit, int nTimeLimit ) { Msat_SearchParams_t Params = { 0.95, 0.999 }; double nConflictsLimit, nLearnedLimit; Msat_Type_t Status; + int timeStart = clock(); int64 nConflictsOld = p->Stats.nConflicts; int64 nDecisionsOld = p->Stats.nDecisions; @@ -174,6 +175,9 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra // if the limit on the number of backtracks is given, quit the restart loop if ( nBackTrackLimit > 0 ) break; + // if the runtime limit is exceeded, quit the restart loop + if ( clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC ) + break; } Msat_SolverCancelUntil( p, 0 ); p->nBackTracks = (int)p->Stats.nConflicts - p->nBackTracks; |