diff options
67 files changed, 2529 insertions, 449 deletions
@@ -231,6 +231,10 @@ SOURCE=.\src\base\abci\abcDelay.c # End Source File # Begin Source File +SOURCE=.\src\base\abci\abcDprove2.c +# End Source File +# Begin Source File + SOURCE=.\src\base\abci\abcDress.c # End Source File # Begin Source File @@ -2269,6 +2273,14 @@ SOURCE=.\src\misc\util\abc_global.h SOURCE=.\src\misc\util\util_hack.h # End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilMem.c +# End Source File +# Begin Source File + +SOURCE=.\src\misc\util\utilMem.h +# End Source File # End Group # Begin Group "nm" @@ -3107,6 +3119,10 @@ SOURCE=.\src\aig\ntl\ntlMap.c # End Source File # Begin Source File +SOURCE=.\src\aig\ntl\ntlNames.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\ntl\ntlObj.c # End Source File # Begin Source File @@ -3669,46 +3685,6 @@ SOURCE=.\src\aig\cgt\cgtSat.c # Begin Group "nal" # PROP Default_Filter "" -# Begin Source File - -SOURCE=.\src\aig\nal090422\nal.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalCore.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalFlop.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalFunc.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalInt.h -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalMan.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalModels.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalRead.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalUtil.c -# End Source File -# Begin Source File - -SOURCE=.\src\aig\nal090422\nalWrite.c -# End Source File # End Group # Begin Group "gia" @@ -3747,6 +3723,10 @@ SOURCE=.\src\aig\gia\giaCSatOld.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaCTas.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaDfs.c # End Source File # Begin Source File @@ -3787,6 +3767,10 @@ SOURCE=.\src\aig\gia\giaFront.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaGiarf.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaGlitch.c # End Source File # Begin Source File @@ -3795,6 +3779,10 @@ SOURCE=.\src\aig\gia\giaHash.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaHcd.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaMan.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 38ba167f..56e2336a 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -481,13 +481,16 @@ extern Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupTrim( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p ); -extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ); +extern Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder ); +extern Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios ); extern Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupWithoutPos( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepres( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDupRepresDfs( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl ); +extern Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs ); extern Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs ); +extern Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs ); /*=== aigFanout.c ==========================================================*/ extern void Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); extern void Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout ); diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c index eeaf4c91..90579f59 100644 --- a/src/aig/aig/aigDup.c +++ b/src/aig/aig/aigDup.c @@ -602,9 +602,8 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ) +Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios ) { - Vec_Ptr_t * vPios; Aig_Man_t * pNew; Aig_Obj_t * pObj, * pObjNew; int i, nNodes; @@ -631,7 +630,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ) // duplicate internal nodes Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig; - vPios = Aig_ManOrderPios( p, pGuide ); Vec_PtrForEachEntry( vPios, pObj, i ) { if ( Aig_ObjIsPi(pObj) ) @@ -650,7 +648,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide ) pObj->pData = pObjNew; } } - Vec_PtrFree( vPios ); // assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) ); if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) ) printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes ); @@ -982,6 +979,54 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper ) SeeAlso [] ***********************************************************************/ +Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pMiter; + int i; + assert( Aig_ManRegNum(p) > 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // set registers + pNew->nRegs = fAddRegs? p->nRegs : 0; + pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs; + pNew->nTruePos = 1; + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create the PO + pMiter = Aig_ManConst0(pNew); + Aig_ManForEachPoSeq( p, pObj, i ) + pMiter = Aig_Or( pNew, pMiter, Aig_ObjChild0Copy(pObj) ); + Aig_ObjCreatePo( pNew, pMiter ); + // create register inputs with MUXes + if ( fAddRegs ) + { + Aig_ManForEachLiSeq( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManCleanup( pNew ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG with only one primary output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs ) { Aig_Man_t * pNew; @@ -1018,6 +1063,57 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs ) return pNew; } +/**Function************************************************************* + + Synopsis [Duplicates AIG with only one primary output.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i, nOuts = 0; + assert( Aig_ManRegNum(p) > 0 ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + // create the POs + nOuts = 0; + Aig_ManForEachPoSeq( p, pObj, i ) + nOuts += ( Aig_ObjFanin0(pObj) != Aig_ManConst1(p) ); + // set registers + pNew->nRegs = fAddRegs? p->nRegs : 0; + pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs; + pNew->nTruePos = nOuts; + // duplicate internal nodes + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + // create the PO + Aig_ManForEachPoSeq( p, pObj, i ) + if ( Aig_ObjFanin0(pObj) != Aig_ManConst1(p) ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + // create register inputs with MUXes + if ( fAddRegs ) + { + Aig_ManForEachLiSeq( p, pObj, i ) + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + Aig_ManCleanup( pNew ); + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 0b6ff6bd..11d3f3d7 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -373,8 +373,8 @@ void Aig_ManPrintStats( Aig_Man_t * p ) { int nChoices = Aig_ManChoiceNum(p); printf( "%-15s : ", p->pName ); - printf( "pi = %5d ", Aig_ManPiNum(p) ); - printf( "po = %5d ", Aig_ManPoNum(p) ); + printf( "pi = %5d ", Aig_ManPiNum(p)-Aig_ManRegNum(p) ); + printf( "po = %5d ", Aig_ManPoNum(p)-Aig_ManRegNum(p) ); if ( Aig_ManRegNum(p) ) printf( "lat = %5d ", Aig_ManRegNum(p) ); printf( "and = %7d ", Aig_ManAndNum(p) ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 6e0cb3e8..6849ba70 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1223,6 +1223,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon // extern void * Abc_FrameGetGlobalFrame(); extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax ); + Vec_Ptr_t * vPios; Vec_Ptr_t * vOutsTotal, * vOuts; Aig_Man_t * pAigTotal, * pAigPart, * pAig, * pTemp; Vec_Int_t * vPart, * vPartSupp; @@ -1323,8 +1324,10 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon // create the equivalent nodes lists Aig_ManMarkValidChoices( pAig ); // reconstruct the network - pAig = Aig_ManDupDfsGuided( pTemp = pAig, Vec_PtrEntry(vAigs,0) ); + vPios = Aig_ManOrderPios( pAig, Vec_PtrEntry(vAigs,0) ); + pAig = Aig_ManDupDfsGuided( pTemp = pAig, vPios ); Aig_ManStop( pTemp ); + Vec_PtrFree( vPios ); // duplicate the timing manager pTemp = Vec_PtrEntry( vAigs, 0 ); if ( pTemp->pManTime ) @@ -1541,6 +1544,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p ) ***********************************************************************/ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) { + Vec_Ptr_t * vPios; Aig_Man_t * pNew, * pThis, * pPrev, * pTemp; int i; // start AIG with choices @@ -1562,8 +1566,10 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) // create the equivalent nodes lists Aig_ManMarkValidChoices( pNew ); // reconstruct the network - pNew = Aig_ManDupDfsGuided( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) ); + vPios = Aig_ManOrderPios( pNew, Vec_PtrEntry( vAigs, 0 ) ); + pNew = Aig_ManDupDfsGuided( pTemp = pNew, vPios ); Aig_ManStop( pTemp ); + Vec_PtrFree( vPios ); // duplicate the timing manager pTemp = Vec_PtrEntry( vAigs, 0 ); if ( pTemp->pManTime ) @@ -1573,6 +1579,12 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose ) return pNew; } +/* + Vec_Ptr_t * vPios; + vPios = Aig_ManOrderPios( pMan, pAig ); + Vec_PtrFree( vPios ); +*/ + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index d49fffd3..f51b8871 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -1278,6 +1278,133 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v assert( vArr->nSize <= vArr2->nSize ); } +#include "fra.h" +#include "saig.h" + +extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex ); +extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig ); +extern int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame ); + +/**Function************************************************************* + + Synopsis [Starts the process of retuning values for internal nodes.] + + Description [Should be called when pCex is available, before probing + any object for its value using Aig_ManCounterExampleValueLookup().] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex ) +{ + Aig_Obj_t * pObj, * pObjRi, * pObjRo; + int Val0, Val1, nObjs, i, k, iBit = 0; + assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs + assert( pAig->pData2 == NULL ); // if this fail, there may be a memory leak + // allocate memory to store simulation bits for internal nodes + pAig->pData2 = ABC_CALLOC( unsigned, Aig_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) ); + // the register values in the counter-example should be zero + Saig_ManForEachLo( pAig, pObj, k ) + assert( Aig_InfoHasBit(pCex->pData, iBit++) == 0 ); + // iterate through the timeframes + nObjs = Aig_ManObjNum(pAig); + for ( i = 0; i <= pCex->iFrame; i++ ) + { + // set constant 1 node + Aig_InfoSetBit( pAig->pData2, nObjs * i + 0 ); + // set primary inputs according to the counter-example + Saig_ManForEachPi( pAig, pObj, k ) + if ( Aig_InfoHasBit(pCex->pData, iBit++) ) + Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) ); + // compute values for each node + Aig_ManForEachNode( pAig, pObj, k ) + { + Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) ); + Val1 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) ); + if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) ) + Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) ); + } + // derive values for combinational outputs + Aig_ManForEachPo( pAig, pObj, k ) + { + Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) ); + if ( Val0 ^ Aig_ObjFaninC0(pObj) ) + Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) ); + } + if ( i == pCex->iFrame ) + continue; + // transfer values to the register output of the next frame + Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k ) + if ( Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) ) + Aig_InfoSetBit( pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) ); + } + assert( iBit == pCex->nBits ); + // check that the counter-example is correct, that is, the corresponding output is asserted + assert( Aig_InfoHasBit( pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) ); +} + +/**Function************************************************************* + + Synopsis [Stops the process of retuning values for internal nodes.] + + Description [Should be called when probing is no longer needed] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig ) +{ + assert( pAig->pData2 != NULL ); // if this fail, we try to call this procedure more than once + free( pAig->pData2 ); + pAig->pData2 = NULL; +} + +/**Function************************************************************* + + Synopsis [Returns the value of the given object in the given timeframe.] + + Description [Should be called to probe the value of an object with + the given ID (iFrame is a 0-based number of a time frame - should not + exceed the number of timeframes in the original counter-example).] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Aig_ManCounterExampleValueLookup( Aig_Man_t * pAig, int Id, int iFrame ) +{ + assert( Id >= 0 && Id < Aig_ManObjNum(pAig) ); + return Aig_InfoHasBit( pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id ); +} + +/**Function************************************************************* + + Synopsis [Procedure to test the above code.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex ) +{ + Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNum(pAig)/2 ); + int iFrame = ABC_MAX( 0, pCex->iFrame - 1 ); + printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame ); + Aig_ManCounterExampleValueStart( pAig, pCex ); + printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame, + Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) ); + Aig_ManCounterExampleValueStop( pAig ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h index ee91fe8b..e5d585ce 100644 --- a/src/aig/bbr/bbr.h +++ b/src/aig/bbr/bbr.h @@ -57,7 +57,7 @@ typedef struct Bbr_ImageTree_t_ Bbr_ImageTree_t; extern Bbr_ImageTree_t * Bbr_bddImageStart( DdManager * dd, DdNode * bCare, int nParts, DdNode ** pbParts, - int nVars, DdNode ** pbVars, int fVerbose ); + int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ); extern DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare ); extern void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree ); extern DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree ); @@ -74,7 +74,7 @@ extern void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ); extern int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ); extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose ); /*=== bbrReach.c ==========================================================*/ -extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); +extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); #ifdef __cplusplus } diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c index 41253dbc..4555570a 100644 --- a/src/aig/bbr/bbrCex.c +++ b/src/aig/bbr/bbrCex.c @@ -63,7 +63,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, // create the cube of NS variables bCubeNs = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) ); Cudd_Ref( bCubeNs ); - pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose ); + pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, 100000000, fVerbose ); Cudd_RecursiveDeref( dd, bCubeNs ); if ( pTree == NULL ) { diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c index edd344bf..aed302eb 100644 --- a/src/aig/bbr/bbrImage.c +++ b/src/aig/bbr/bbrImage.c @@ -27,7 +27,7 @@ Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in Image Computation. ICCAD, 2001. */ - + /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ @@ -49,6 +49,7 @@ struct Bbr_ImageTree_t_ int nNodesMax; // the max number of nodes in one iter int nNodesMaxT; // the overall max number of nodes int nIter; // the number of iterations with this tree + int nBddMax; // the number of node to stop }; struct Bbr_ImageNode_t_ @@ -89,8 +90,6 @@ struct Bbr_ImageVar_t_ /* Macro declarations */ /*---------------------------------------------------------------------------*/ -#define BDD_BLOW_UP 2000000 - #define b0 Cudd_Not((dd)->one) #define b1 (dd)->one @@ -116,7 +115,7 @@ static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd, static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode ); static int Bbr_BuildTreeNode( DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes, - int nVars, Bbr_ImageVar_t ** pVars, int * pfStop ); + int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax ); static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes ); static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode ); @@ -166,7 +165,7 @@ static void Bbr_bddPrint( DdManager * dd, DdNode * F ); Bbr_ImageTree_t * Bbr_bddImageStart( DdManager * dd, DdNode * bCare, // the care set int nParts, DdNode ** pbParts, // the partitions for image computation - int nVars, DdNode ** pbVars, int fVerbose ) // the NS and parameter variables (not quantified!) + int nVars, DdNode ** pbVars, int nBddMax, int fVerbose ) // the NS and parameter variables (not quantified!) { Bbr_ImageTree_t * pTree; Bbr_ImagePart_t ** pParts; @@ -184,7 +183,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart( pCare = pNodes[nParts]; // process the nodes - while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop ) ); + while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) ); // consider the case of BDD node blowup if ( fStop ) @@ -213,6 +212,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart( pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 ); memset( pTree, 0, sizeof(Bbr_ImageTree_t) ); pTree->pCare = pCare; + pTree->nBddMax = nBddMax; pTree->fVerbose = fVerbose; // merge the topmost nodes @@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode ) if ( pTree->nNodesMax < nNodes ) pTree->nNodesMax = nNodes; } - if ( dd->keys-dd->dead > BDD_BLOW_UP ) + if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax ) return 0; return 1; } @@ -716,7 +716,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode ) ***********************************************************************/ int Bbr_BuildTreeNode( DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes, - int nVars, Bbr_ImageVar_t ** pVars, int * pfStop ) + int nVars, Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax ) { Bbr_ImageNode_t * pNode1, * pNode2; Bbr_ImageVar_t * pVar; @@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd, } *pfStop = 0; - if ( dd->keys-dd->dead > BDD_BLOW_UP ) + if ( dd->keys-dd->dead > (unsigned)nBddMax ) { *pfStop = 1; return 0; diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c index 1d43f6fb..7d0e4bc0 100644 --- a/src/aig/bbr/bbrReach.c +++ b/src/aig/bbr/bbrReach.c @@ -220,11 +220,16 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D int i, nIters, nBddSize; int nThreshold = 10000; Vec_Ptr_t * vOnionRings; + int status, method; + + status = Cudd_ReorderingStatus( dd, &method ); + if ( status ) + Cudd_AutodynDisable( dd ); // start the image computation bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs ); if ( fPartition ) - pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose ); + pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), nBddMax, fVerbose ); else pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose ); Cudd_RecursiveDeref( dd, bCubeCs ); @@ -235,6 +240,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D return -1; } + if ( status ) + Cudd_AutodynEnable( dd, method ); + // start the onion rings vOnionRings = Vec_PtrAlloc( 1000 ); @@ -360,11 +368,11 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D Description [] SideEffects [] - + SeeAlso [] ***********************************************************************/ -int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) +int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ) { DdManager * dd; DdNode ** pbParts, ** pbOutputs; @@ -397,6 +405,10 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP // create the initial state and the variable map bInitial = Aig_ManInitStateVarMap( dd, p, fVerbose ); Cudd_Ref( bInitial ); + // set reordering + if ( fReorderImage ) + Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT ); + // check the result RetValue = -1; for ( i = 0; i < Saig_ManPoNum(p); i++ ) @@ -456,7 +468,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP SeeAlso [] ***********************************************************************/ -int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ) +int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ) { Ssw_Cex_t * pCexOld, * pCexNew; Aig_Man_t * p; @@ -468,12 +480,12 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fP if ( Aig_ObjRefs(pObj) == 0 ) break; if ( i == Saig_ManPiNum(pInit) ) - return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); + return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent ); // create new AIG p = Aig_ManDupTrim( pInit ); assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) ); assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) ); - RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent ); + RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent ); if ( RetValue != 0 ) { Aig_ManStop( p ); diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h index 8e14d2ef..fcadb6ab 100644 --- a/src/aig/cec/cec.h +++ b/src/aig/cec/cec.h @@ -48,6 +48,7 @@ struct Cec_ParSat_t_ int fPolarFlip; // flops polarity of variables int fCheckMiter; // the circuit is the miter int fFirstStop; // stop on the first sat output + int fLearnCls; // perform clause learning int fVerbose; // verbose stats }; diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c index 0662d73d..f51d138d 100644 --- a/src/aig/cec/cecChoice.c +++ b/src/aig/cec/cecChoice.c @@ -380,17 +380,17 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars ) +Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars ) { - Gia_Man_t * pMiter, * pNew; + Gia_Man_t * pNew; int RetValue; // compute equivalences of the miter - pMiter = Gia_ManChoiceMiter( vGias ); - RetValue = Cec_ManChoiceComputation_int( pMiter, pPars ); +// pMiter = Gia_ManChoiceMiter( vGias ); + RetValue = Cec_ManChoiceComputation_int( pGia, pPars ); // derive AIG with choices - pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) ); + pNew = Gia_ManEquivToChoices( pGia, nGias ); Gia_ManHasChoices( pNew ); - Gia_ManStop( pMiter ); +// Gia_ManStop( pMiter ); // report the results if ( pPars->fVerbose ) { @@ -422,11 +422,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc Gia_Man_t * pGia; if ( 0 ) { - Vec_Ptr_t * vGias; - vGias = Vec_PtrAlloc( 1 ); - Vec_PtrPush( vGias, pAig ); - pGia = Cec_ManChoiceComputationVec( vGias, pParsChc ); - Vec_PtrFree( vGias ); + pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc ); } else { @@ -439,7 +435,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc pManNew = Dar_ManChoiceNew( pMan, pPars ); pGia = Gia_ManFromAig( pManNew ); Aig_ManStop( pManNew ); - Aig_ManStop( pMan ); +// Aig_ManStop( pMan ); } return pGia; } @@ -455,13 +451,10 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc SeeAlso [] ***********************************************************************/ -Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) { Cec_ParChc_t ParsChc, * pParsChc = &ParsChc; - Vec_Ptr_t * vGias; - Gia_Man_t * pGia; Aig_Man_t * pAig; - int i; if ( pPars->fVerbose ) ABC_PRT( "Synthesis time", pPars->timeSynth ); Cec_ManChcSetDefaultParams( pParsChc ); @@ -470,14 +463,8 @@ Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 ) pParsChc->nBTLimit = 100; pParsChc->fVerbose = pPars->fVerbose; - vGias = Vec_PtrAlloc( 10 ); - Vec_PtrForEachEntry( vAigs, pAig, i ) - Vec_PtrPush( vGias, Gia_ManFromAig(pAig) ); - pGia = Cec_ManChoiceComputationVec( vGias, pParsChc ); - Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) ); - Vec_PtrForEachEntry( vGias, pAig, i ) - Gia_ManStop( (Gia_Man_t *)pAig ); - Vec_PtrFree( vGias ); + pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc ); + Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) ); pAig = Gia_ManToAig( pGia, 1 ); Gia_ManStop( pGia ); return pAig; diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c index dc0fc0d0..9820c05c 100644 --- a/src/aig/cec/cecCore.c +++ b/src/aig/cec/cecCore.c @@ -49,6 +49,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p ) p->fPolarFlip = 1; // flops polarity of variables p->fCheckMiter = 0; // the circuit is the miter p->fFirstStop = 0; // stop on the first sat output + p->fLearnCls = 0; // perform clause learning p->fVerbose = 0; // verbose stats } diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c index b4076916..96af801d 100644 --- a/src/aig/cec/cecCorr.c +++ b/src/aig/cec/cecCorr.c @@ -797,7 +797,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr } pParsSat->nBTLimit *= 10; if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); // refine classes with these counter-examples @@ -831,8 +831,9 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr ***********************************************************************/ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) { - int nIterMax = 100000; - int nAddFrames = 1; // additional timeframes to simulate + int nIterMax = 100000; + int nAddFrames = 1; // additional timeframes to simulate + int fRunBmcFirst = 0; Vec_Str_t * vStatus; Vec_Int_t * vOutputs; Vec_Int_t * vCexStore; @@ -875,8 +876,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk ); } // check the base case - if ( !pPars->fLatchCorr || pPars->nFrames > 1 ) - Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); + if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) + Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); // perform refinement of equivalence classes for ( r = 0; r < nIterMax; r++ ) { @@ -926,6 +927,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) if ( r == nIterMax ) printf( "The refinement was not finished. The result may be incorrect.\n" ); Cec_ManSimStop( pSim ); + // check the base case + if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) ) + Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 ); clkTotal = clock() - clkTotal; // report the results if ( pPars->fVerbose ) diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h index 1fd48d55..9c012f73 100644 --- a/src/aig/cec/cecInt.h +++ b/src/aig/cec/cecInt.h @@ -199,6 +199,10 @@ extern int Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pO extern void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars ); extern Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats ); extern Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus ); +extern int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ); +extern int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); +extern void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ); +extern Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * p ); /*=== ceFraeep.c ============================================================*/ extern Gia_Man_t * Cec_ManFraSpecReduction( Cec_ManFra_t * p ); extern int Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew ); diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c index 3a8d8588..1aaf54ff 100644 --- a/src/aig/cec/cecSolve.c +++ b/src/aig/cec/cecSolve.c @@ -404,9 +404,9 @@ void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMi float dActConeBumpMax = 20.0; int iVar; // skip visited variables - if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) ) + if ( Gia_ObjIsTravIdCurrentArray(p->pAig, pObj) ) return; - Gia_ObjSetTravIdCurrent(p->pAig, pObj); + Gia_ObjSetTravIdCurrentArray(p->pAig, pObj); // add the PI to the list if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) ) return; @@ -440,7 +440,7 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj ) // reset the active variables veci_resize(&p->pSat->act_vars, 0); // prepare for traversal - Gia_ManIncrementTravId( p->pAig ); + Gia_ManIncrementTravIdArray( p->pAig ); // determine the min and max level to visit assert( dActConeRatio > 0 && dActConeRatio < 1 ); LevelMax = Gia_ObjLevel(p->pAig,pObj); @@ -465,9 +465,18 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj ) ***********************************************************************/ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) { + Gia_Obj_t * pObjR = Gia_Regular(pObj); int nBTLimit = p->pPars->nBTLimit; int Lit, RetValue, status, clk, clk2, nConflicts; + if ( pObj == Gia_ManConst0(p->pAig) ) + return 1; + if ( pObj == Gia_ManConst1(p->pAig) ) + { + assert( 0 ); + return 0; + } + p->nCallsSince++; // experiment with this!!! p->nSatTotal++; @@ -480,12 +489,12 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj ) // if the nodes do not have SAT variables, allocate them clk2 = clock(); - Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) ); + Cec_CnfNodeAddToSolver( p, pObjR ); //ABC_PRT( "cnf", clock() - clk2 ); //printf( "%d \n", p->pSat->size ); clk2 = clock(); -// Cec_SetActivityFactors( p, Gia_ObjFanin0(pObj) ); +// Cec_SetActivityFactors( p, pObjR ); //ABC_PRT( "act", clock() - clk2 ); // propage unit clauses @@ -498,10 +507,10 @@ clk2 = clock(); // solve under assumptions // A = 1; B = 0 OR A = 1; B = 1 - Lit = toLitCond( Cec_ObjSatNum(p,Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) ); + Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) ); if ( p->pPars->fPolarFlip ) { - if ( Gia_ObjFanin0(pObj)->fPhase ) Lit = lit_neg( Lit ); + if ( pObjR->fPhase ) Lit = lit_neg( Lit ); } //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); clk = clock(); @@ -541,6 +550,110 @@ p->timeSatUndec += clock() - clk; } } +/**Function************************************************************* + + Synopsis [Runs equivalence test for the two nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ) +{ + Gia_Obj_t * pObjR1 = Gia_Regular(pObj1); + Gia_Obj_t * pObjR2 = Gia_Regular(pObj2); + int nBTLimit = p->pPars->nBTLimit; + int Lits[2], RetValue, status, clk, clk2, nConflicts; + + if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) ) + return 1; + if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) ) + { + assert( 0 ); + return 0; + } + + p->nCallsSince++; // experiment with this!!! + p->nSatTotal++; + + // check if SAT solver needs recycling + if ( p->pSat == NULL || + (p->pPars->nSatVarMax && + p->nSatVars > p->pPars->nSatVarMax && + p->nCallsSince > p->pPars->nCallsRecycle) ) + Cec_ManSatSolverRecycle( p ); + + // if the nodes do not have SAT variables, allocate them +clk2 = clock(); + Cec_CnfNodeAddToSolver( p, pObjR1 ); + Cec_CnfNodeAddToSolver( p, pObjR2 ); +//ABC_PRT( "cnf", clock() - clk2 ); +//printf( "%d \n", p->pSat->size ); + +clk2 = clock(); +// Cec_SetActivityFactors( p, pObjR1 ); +// Cec_SetActivityFactors( p, pObjR2 ); +//ABC_PRT( "act", clock() - clk2 ); + + // propage unit clauses + if ( p->pSat->qtail != p->pSat->qhead ) + { + status = sat_solver_simplify(p->pSat); + assert( status != 0 ); + assert( p->pSat->qtail == p->pSat->qhead ); + } + + // solve under assumptions + // A = 1; B = 0 OR A = 1; B = 1 + Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) ); + Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) ); + if ( p->pPars->fPolarFlip ) + { + if ( pObjR1->fPhase ) Lits[0] = lit_neg( Lits[0] ); + if ( pObjR2->fPhase ) Lits[1] = lit_neg( Lits[1] ); + } +//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 ); +clk = clock(); + nConflicts = p->pSat->stats.conflicts; + +clk2 = clock(); + RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2, + (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); +//ABC_PRT( "sat", clock() - clk2 ); + + if ( RetValue == l_False ) + { +p->timeSatUnsat += clock() - clk; + Lits[0] = lit_neg( Lits[0] ); + Lits[1] = lit_neg( Lits[1] ); + RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 ); + assert( RetValue ); + p->nSatUnsat++; + p->nConfUnsat += p->pSat->stats.conflicts - nConflicts; +//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); + return 1; + } + else if ( RetValue == l_True ) + { +p->timeSatSat += clock() - clk; + p->nSatSat++; + p->nConfSat += p->pSat->stats.conflicts - nConflicts; +//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); + return 0; + } + else // if ( RetValue == l_Undef ) + { +p->timeSatUndec += clock() - clk; + p->nSatUndec++; + p->nConfUndec += p->pSat->stats.conflicts - nConflicts; +//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts ); + return -1; + } +} + /**Function************************************************************* @@ -570,7 +683,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar } Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); - Gia_ManResetTravId( pAig ); + Gia_ManResetTravIdArray( pAig ); p = Cec_ManSatCreate( pAig, pPars ); pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); Gia_ManForEachCo( pAig, pObj, i ) @@ -583,7 +696,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar } Bar_ProgressUpdate( pProgress, i, "SAT..." ); clk2 = clock(); - status = Cec_ManSatCheckNode( p, pObj ); + status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); pObj->fMark0 = (status == 0); pObj->fMark1 = (status == 1); /* @@ -619,6 +732,22 @@ clk2 = clock(); /**Function************************************************************* + Synopsis [Returns the pattern stored.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat ) +{ + return pSat->vCex; +} + +/**Function************************************************************* + Synopsis [Save values in the cone of influence.] Description [] @@ -630,9 +759,9 @@ clk2 = clock(); ***********************************************************************/ void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs ) { - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + if ( Gia_ObjIsTravIdCurrentArray(p, pObj) ) return; - Gia_ObjSetTravIdCurrent(p, pObj); + Gia_ObjSetTravIdCurrentArray(p, pObj); if ( Gia_ObjIsCi(pObj) ) { unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) ); @@ -670,7 +799,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts); Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); - Gia_ManResetTravId( pAig ); + Gia_ManResetTravIdArray( pAig ); p = Cec_ManSatCreate( pAig, pPars ); vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) ); @@ -691,7 +820,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat } continue; } - status = Cec_ManSatCheckNode( p, pObj ); + status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); //printf( "output %d status = %d\n", i, status ); Vec_StrPush( vStatus, (char)status ); if ( status != 0 ) @@ -707,7 +836,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat if ( iPat % nPatsInit == 0 ) iPat++; // save the pattern - Gia_ManIncrementTravId( pAig ); + Gia_ManIncrementTravIdArray( pAig ); // Vec_IntClear( p->vCex ); Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs ); // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits ); @@ -771,9 +900,9 @@ void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out ) ***********************************************************************/ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj ) { - if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + if ( Gia_ObjIsTravIdCurrentArray(p, pObj) ) return; - Gia_ObjSetTravIdCurrent(p, pObj); + Gia_ObjSetTravIdCurrentArray(p, pObj); if ( Gia_ObjIsCi(pObj) ) { pSat->nCexLits++; @@ -787,6 +916,26 @@ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * p /**Function************************************************************* + Synopsis [Save patterns.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 ) +{ + Vec_IntClear( p->vCex ); + Gia_ManIncrementTravIdArray( p->pAig ); + Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) ); + if ( pObj2 ) + Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) ); +} + +/**Function************************************************************* + Synopsis [Performs one round of solving for the POs of the AIG.] Description [Labels the nodes that have been proved (pObj->fMark1) @@ -808,7 +957,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St // prepare AIG Gia_ManSetPhase( pAig ); Gia_ManLevelNum( pAig ); - Gia_ManResetTravId( pAig ); + Gia_ManResetTravIdArray( pAig ); // create resulting data-structures vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) ); vCexStore = Vec_IntAlloc( 10000 ); @@ -834,7 +983,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St } continue; } - status = Cec_ManSatCheckNode( p, pObj ); + status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) ); Vec_StrPush( vStatus, (char)status ); if ( status == -1 ) { @@ -845,8 +994,9 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St continue; assert( status == 0 ); // save the pattern - Gia_ManIncrementTravId( pAig ); - Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) ); +// Gia_ManIncrementTravIdArray( pAig ); +// Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) ); + Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL ); // Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits ); Cec_ManSatAddToStore( vCexStore, p->vCex, i ); } diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 66e6371d..0209165a 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -19,12 +19,16 @@ ***********************************************************************/ #include "darInt.h" -//#include "ioa.h" +#include "dch.h" +#include "gia.h" +#include "giaAig.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + extern void * Tim_ManDup( void * p, int fDiscrete ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -419,7 +423,313 @@ ABC_PRT( "Choicing time ", clock() - clk ); // return NULL; } -#include "dch.h" + +/**Function************************************************************* + + Synopsis [Duplicates the AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return pObj->Value; + Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjIsCo(pObj) ) + return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) ); + return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Derives the miter of several AIGs for choice computation.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Dar_ManChoiceMiter( Vec_Ptr_t * vGias ) +{ + Gia_Man_t * pNew, * pGia, * pGia0; + int i, k, iNode, nNodes; + // make sure they have equal parameters + assert( Vec_PtrSize(vGias) > 0 ); + pGia0 = Vec_PtrEntry( vGias, 0 ); + Vec_PtrForEachEntry( vGias, pGia, i ) + { + assert( Gia_ManCiNum(pGia) == Gia_ManCiNum(pGia0) ); + assert( Gia_ManCoNum(pGia) == Gia_ManCoNum(pGia0) ); + assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) ); + Gia_ManFillValue( pGia ); + Gia_ManConst0(pGia)->Value = 0; + } + // start the new manager + pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) ); + pNew->pName = Gia_UtilStrsav( pGia0->pName ); + // create new CIs and assign them to the old manager CIs + for ( k = 0; k < Gia_ManCiNum(pGia0); k++ ) + { + iNode = Gia_ManAppendCi(pNew); + Vec_PtrForEachEntry( vGias, pGia, i ) + Gia_ManCi( pGia, k )->Value = iNode; + } + // create internal nodes + Gia_ManHashAlloc( pNew ); + for ( k = 0; k < Gia_ManCoNum(pGia0); k++ ) + { + Vec_PtrForEachEntry( vGias, pGia, i ) + Dar_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) ); + } + Gia_ManHashStop( pNew ); + // check the presence of dangling nodes + nNodes = Gia_ManHasDandling( pNew ); + assert( nNodes == 0 ); + // finalize + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Reproduces script "compress".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_NewCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose ) +//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fUpdateLevel = fUpdateLevel; + pParsRef->fUpdateLevel = fUpdateLevel; + + pParsRwr->fPower = fPower; + + pParsRwr->fVerbose = 0;//fVerbose; + pParsRef->fVerbose = 0;//fVerbose; + +// pAig = Aig_ManDupDfs( pAig ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // balance + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + return pAig; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fUpdateLevel = fUpdateLevel; + pParsRef->fUpdateLevel = fUpdateLevel; + pParsRwr->fFanout = fFanout; + pParsRwr->fPower = fPower; + + pParsRwr->fVerbose = 0;//fVerbose; + pParsRef->fVerbose = 0;//fVerbose; + +// pAig = Aig_ManDupDfs( pAig ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // skip if lighter synthesis is requested + if ( !fLightSynth ) + { + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } + + // balance + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // skip if lighter synthesis is requested + if ( !fLightSynth ) + { + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // skip if lighter synthesis is requested + if ( !fLightSynth ) + { + // balance + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } + } + + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + + // skip if lighter synthesis is requested + if ( !fLightSynth ) + { + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDupDfs( pTemp = pAig ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } + + // balance + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + if ( fVerbose ) Aig_ManPrintStats( pAig ); + } + return pAig; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [Takes AIG manager, consumes it, and produces GIA manager.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose ) +//alias resyn "b; rw; rwz; b; rwz; b" +//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" +{ + Vec_Ptr_t * vGias; + Gia_Man_t * pGia, * pTemp; + int i; + + vGias = Vec_PtrAlloc( 3 ); + pGia = Gia_ManFromAig(pAig); + Vec_PtrPush( vGias, pGia ); + + pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose ); + pGia = Gia_ManFromAig(pAig); + Vec_PtrPush( vGias, pGia ); +//Aig_ManPrintStats( pAig ); + + pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose ); + pGia = Gia_ManFromAig(pAig); + Vec_PtrPush( vGias, pGia ); +//Aig_ManPrintStats( pAig ); + + Aig_ManStop( pAig ); + + // swap around the first and the last + pTemp = Vec_PtrPop( vGias ); + Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) ); + Vec_PtrWriteEntry( vGias, 0, pTemp ); + +// Aig_Man_t * pAig; +// int i; +// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) ); +// Vec_PtrForEachEntry( p->vAigs, pAig, i ) +// Aig_ManPrintStats( pAig ); + + // derive the miter + pGia = Dar_ManChoiceMiter( vGias ); + + // cleanup + Vec_PtrForEachEntry( vGias, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vGias ); + return pGia; +} /**Function************************************************************* @@ -432,6 +742,7 @@ ABC_PRT( "Choicing time ", clock() - clk ); SeeAlso [] ***********************************************************************/ +/* Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); @@ -465,12 +776,6 @@ if ( fVerbose ) pPars->timeSynth = clock() - clk; clk = clock(); -/* - if ( fConstruct ) - pMan = Aig_ManChoiceConstructive( vAigs, fVerbose ); - else - pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose ); -*/ // perform choice computation if ( pPars->fUseGia ) pMan = Cec_ComputeChoices( vAigs, pPars ); @@ -506,6 +811,144 @@ if ( fVerbose ) return pMan; // return NULL; } +*/ + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [Consumes the input AIG to reduce memory usage.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); + extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); + int fVerbose = pPars->fVerbose; + Aig_Man_t * pMan, * pTemp; + Vec_Ptr_t * vAigs; + Vec_Ptr_t * vPios; + void * pManTime; + char * pName, * pSpec; + int i, clk; + +clk = clock(); + vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose ); +pPars->timeSynth = clock() - clk; + // swap the first and last network + // this should lead to the primary choice being "better" because of synthesis + // (it is also important when constructing choices) + pMan = Vec_PtrPop( vAigs ); + Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); + Vec_PtrWriteEntry( vAigs, 0, pMan ); + + // derive the total AIG + pMan = Dch_DeriveTotalAig( vAigs ); + // cleanup + Vec_PtrForEachEntry( vAigs, pTemp, i ) + Aig_ManStop( pTemp ); + Vec_PtrFree( vAigs ); + + // compute choices + pMan = Dch_ComputeChoices( pTemp = pMan, pPars ); + Aig_ManStop( pTemp ); + + // save useful things + pManTime = pAig->pManTime; pAig->pManTime = NULL; + pName = Aig_UtilStrsav( pAig->pName ); + pSpec = Aig_UtilStrsav( pAig->pSpec ); + + // create guidence + vPios = Aig_ManOrderPios( pMan, pAig ); + Aig_ManStop( pAig ); + + // reconstruct the network + pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vPios ); + + // reset levels + pMan->pManTime = pManTime; + Aig_ManChoiceLevel( pMan ); + + // copy names + ABC_FREE( pMan->pName ); + ABC_FREE( pMan->pSpec ); + pMan->pName = pName; + pMan->pSpec = pSpec; + return pMan; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [Consumes the input AIG to reduce memory usage.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ) +{ + extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ); + extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); + extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); + int fVerbose = pPars->fVerbose; + Aig_Man_t * pMan, * pTemp; + Gia_Man_t * pGia; + Vec_Ptr_t * vPios; + void * pManTime; + char * pName, * pSpec; + int clk; + + // save useful things + pManTime = pAig->pManTime; pAig->pManTime = NULL; + pName = Aig_UtilStrsav( pAig->pName ); + pSpec = Aig_UtilStrsav( pAig->pSpec ); + + // perform synthesis +clk = clock(); + pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, 0 ); +pPars->timeSynth = clock() - clk; + + // perform choice computation + if ( pPars->fUseGia ) + pMan = Cec_ComputeChoices( pGia, pPars ); + else + { + pMan = Gia_ManToAigSkip( pGia, 3 ); + Gia_ManStop( pGia ); + pMan = Dch_ComputeChoices( pTemp = pMan, pPars ); + Aig_ManStop( pTemp ); + } + + // create guidence + vPios = Aig_ManOrderPios( pMan, pAig ); + Aig_ManStop( pAig ); + + // reconstruct the network + pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios ); + Aig_ManStop( pTemp ); + Vec_PtrFree( vPios ); + + // reset levels + pMan->pManTime = pManTime; + Aig_ManChoiceLevel( pMan ); + + // copy names + ABC_FREE( pMan->pName ); + ABC_FREE( pMan->pSpec ); + pMan->pName = pName; + pMan->pSpec = pSpec; + return pMan; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h index 6157a811..38978164 100644 --- a/src/aig/dch/dch.h +++ b/src/aig/dch/dch.h @@ -50,6 +50,7 @@ struct Dch_Pars_t_ int fPower; // uses power-aware rewriting int fUseGia; // uses GIA package int fUseCSat; // uses circuit-based solver + int fLightSynth; // uses lighter version of synthesis int fVerbose; // verbose stats int timeSynth; // synthesis runtime int nNodesAhead; // the lookahead in terms of nodes @@ -66,7 +67,7 @@ struct Dch_Pars_t_ /*=== dchCore.c ==========================================================*/ extern void Dch_ManSetDefaultParams( Dch_Pars_t * p ); -extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); #ifdef __cplusplus diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c index 8e854355..4a8d8b53 100644 --- a/src/aig/dch/dchCore.c +++ b/src/aig/dch/dchCore.c @@ -49,6 +49,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) p->fPolarFlip = 1; // uses polarity adjustment p->fSimulateTfo = 1; // simulate TFO p->fPower = 0; // power-aware rewriting + p->fLightSynth = 0; // uses lighter version of synthesis p->fVerbose = 0; // verbose stats p->nNodesAhead = 1000; // the lookahead in terms of nodes p->nCallsRecycle = 100; // calls to perform before recycling SAT solver @@ -65,37 +66,35 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; Aig_Man_t * pResult; int clk, clkTotal = clock(); - assert( Vec_PtrSize(vAigs) > 0 ); // reset random numbers Aig_ManRandom(1); // start the choicing manager - p = Dch_ManCreate( vAigs, pPars ); + p = Dch_ManCreate( pAig, pPars ); // compute candidate equivalence classes clk = clock(); - p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose ); + p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose ); p->timeSimInit = clock() - clk; // Dch_ClassesPrint( p->ppClasses, 0 ); p->nLits = Dch_ClassesLitNum( p->ppClasses ); // perform SAT sweeping Dch_ManSweep( p ); - // count the number of representatives - p->nReprs = Dch_DeriveChoiceCountReprs( p->pAigTotal ); - // create choices -clk = clock(); - pResult = Dch_DeriveChoiceAig( p->pAigTotal ); -p->timeChoice = clock() - clk; -// Aig_ManCleanup( p->pAigTotal ); -// pResult = Aig_ManDupSimpleDfs( p->pAigTotal ); - // count the number of equivalences and choices - p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult ); - p->nChoices = Aig_ManChoiceNum( pResult ); + // free memory ahead of time p->timeTotal = clock() - clkTotal; Dch_ManStop( p ); + // create choices + ABC_FREE( pAig->pTable ); + pResult = Dch_DeriveChoiceAig( pAig ); + // count the number of representatives + if ( pPars->fVerbose ) + printf( "STATS: Reprs = %6d. Equivs = %6d. Choices = %6d.\n", + Dch_DeriveChoiceCountReprs( pAig ), + Dch_DeriveChoiceCountEquivs( pResult ), + Aig_ManChoiceNum( pResult ) ); return pResult; } diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h index 4e6315a4..a419335d 100644 --- a/src/aig/dch/dchInt.h +++ b/src/aig/dch/dchInt.h @@ -51,7 +51,7 @@ struct Dch_Man_t_ // parameters Dch_Pars_t * pPars; // choicing parameters // AIGs used in the package - Vec_Ptr_t * vAigs; // user-given AIGs +// Vec_Ptr_t * vAigs; // user-given AIGs Aig_Man_t * pAigTotal; // intermediate AIG Aig_Man_t * pAigFraig; // final AIG // equivalence classes @@ -142,7 +142,7 @@ extern int Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vR /*=== dchCnf.c ===================================================*/ extern void Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj ); /*=== dchMan.c ===================================================*/ -extern Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); +extern Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ); extern void Dch_ManStop( Dch_Man_t * p ); extern void Dch_ManSatSolverRecycle( Dch_Man_t * p ); /*=== dchSat.c ===================================================*/ diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c index caed0ed5..c8bd8533 100644 --- a/src/aig/dch/dchMan.c +++ b/src/aig/dch/dchMan.c @@ -39,15 +39,14 @@ SeeAlso [] ***********************************************************************/ -Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) +Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; // create interpolation manager p = ABC_ALLOC( Dch_Man_t, 1 ); memset( p, 0, sizeof(Dch_Man_t) ); p->pPars = pPars; - p->vAigs = vAigs; - p->pAigTotal = Dch_DeriveTotalAig( vAigs ); + p->pAigTotal = pAig; //Dch_DeriveTotalAig( vAigs ); Aig_ManFanoutStart( p->pAigTotal ); // SAT solving p->nSatVars = 1; @@ -74,18 +73,14 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ) ***********************************************************************/ void Dch_ManPrintStats( Dch_Man_t * p ) { -// Aig_Man_t * pAig; -// int i; -// printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) ); -// Vec_PtrForEachEntry( p->vAigs, pAig, i ) -// Aig_ManPrintStats( pAig ); + int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3; printf( "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax ); printf( "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", Aig_ManNodeNum(p->pAigTotal), - Aig_ManNodeNum(p->pAigTotal)-Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)), - Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)), - 100.0 * Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0))/Aig_ManNodeNum(p->pAigTotal) ); + Aig_ManNodeNum(p->pAigTotal)-nNodeNum, + nNodeNum, + 100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) ); printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", p->nSatVars, p->nConeMax, p->nRecycles ); printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", @@ -108,7 +103,7 @@ void Dch_ManPrintStats( Dch_Man_t * p ) { ABC_PRT( "Synthesis ", p->pPars->timeSynth ); } -} +} /**Function************************************************************* @@ -123,10 +118,9 @@ void Dch_ManPrintStats( Dch_Man_t * p ) ***********************************************************************/ void Dch_ManStop( Dch_Man_t * p ) { + Aig_ManFanoutStop( p->pAigTotal ); if ( p->pPars->fVerbose ) Dch_ManPrintStats( p ); - if ( p->pAigTotal ) - Aig_ManStop( p->pAigTotal ); if ( p->pAigFraig ) Aig_ManStop( p->pAigFraig ); if ( p->ppClasses ) diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index a2c10367..f661d2e5 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -128,13 +128,17 @@ struct Fra_Sec_t_ int fFraiging; // enables fraiging at the beginning int fInduction; // enable the use of induction int fInterpolation; // enables interpolation + int fInterSeparate; // enables interpolation for each outputs separately int fReachability; // enables BDD based reachability + int fReorderImage; // enables BDD reordering during image computation int fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove int fUseNewProver; // the new prover int fSilent; // disables all output int fVerbose; // enables verbose reporting of statistics int fVeryVerbose; // enables very verbose reporting int TimeLimit; // enables the timeout + int fReadUnsolved; // inserts the unsolved model back + int nSMnumber; // the number of model written // internal parameters int fRecursive; // set to 1 when SEC is called recursively int fReportSolution; // enables report solution in a special form diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 8064d2ee..72af2466 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -61,7 +61,9 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) p->fFraiging = 1; // enables fraiging at the beginning p->fInduction = 1; // enables the use of induction (signal correspondence) p->fInterpolation = 1; // enables interpolation + p->fInterSeparate = 0; // enables interpolation for each outputs separately p->fReachability = 1; // enables BDD based reachability + p->fReorderImage = 0; // enables variable reordering during image computation p->fStopOnFirstFail = 1; // enables stopping after first output of a miter has failed to prove p->fUseNewProver = 0; // enables new prover p->fSilent = 0; // disables all output @@ -93,6 +95,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult ) int TimeOut = 0; int fLatchCorr = 0; float TimeLeft = 0.0; + pParSec->nSMnumber = -1; // try the miter before solving pNew = Aig_ManDupSimple( p ); @@ -466,14 +469,68 @@ clk = clock(); { Inter_ManParams_t Pars, * pPars = &Pars; int Depth; - + ABC_FREE( pNew->pSeqModel ); Inter_ManSetDefaultParams( pPars ); +// pPars->nBTLimit = 100; pPars->nBTLimit = pParSec->nBTLimitInter; pPars->fVerbose = pParSec->fVeryVerbose; if ( Saig_ManPoNum(pNew) == 1 ) { RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth ); } + else if ( pParSec->fInterSeparate ) + { + Aig_Man_t * pTemp, * pAux; + Aig_Obj_t * pObjPo; + int i, Counter = 0; + Saig_ManForEachPo( pNew, pObjPo, i ) + { + if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) ) + continue; + pTemp = Aig_ManDupOneOutput( pNew, i, 1 ); + pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 ); + Aig_ManStop( pAux ); + if ( Saig_ManRegNum(pTemp) > 0 ) + { + RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth ); + if ( pTemp->pSeqModel ) + { + Ssw_Cex_t * pCex; + pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; + pCex->iPo = i; + Aig_ManStop( pTemp ); + break; + } + // if solved, remove the output + if ( RetValue == 1 ) + { + Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) ); + // printf( "Output %3d : Solved ", i ); + } + else + { + Counter++; + // printf( "Output %3d : Undec ", i ); + } + } + else + Counter++; +// Aig_ManPrintStats( pTemp ); + Aig_ManStop( pTemp ); + printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) ); + } + Aig_ManCleanup( pNew ); + if ( pNew->pSeqModel == NULL ) + { + printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pNew) ); + if ( Counter ) + RetValue = -1; + } + pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 ); + Aig_ManStop( pTemp ); + pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0 ); + Aig_ManStop( pTemp ); + } else { Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew ); @@ -481,7 +538,6 @@ clk = clock(); if ( pNewOrpos->pSeqModel ) { Ssw_Cex_t * pCex; - ABC_FREE( pNew->pSeqModel ); pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL; pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel ); } @@ -505,10 +561,10 @@ ABC_PRT( "Time", clock() - clk ); // try reachability analysis if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax ) { - extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); - RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, 0, pParSec->fSilent ); + RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, pParSec->fReorderImage, 0, pParSec->fSilent ); } finish: @@ -541,6 +597,11 @@ ABC_PRT( "Time", clock() - clkTotal ); } else { + /////////////////////////////////// + // save intermediate result + extern void Abc_FrameSetSave1( void * pAig ); + Abc_FrameSetSave1( Aig_ManDupSimple(pNew) ); + /////////////////////////////////// if ( !pParSec->fSilent ) { printf( "Networks are UNDECIDED. " ); @@ -555,7 +616,8 @@ ABC_PRT( "Time", clock() - clkTotal ); { static int Counter = 1; char pFileName[1000]; - sprintf( pFileName, "sm%03d.aig", Counter++ ); + pParSec->nSMnumber = Counter; + sprintf( pFileName, "sm%02d.aig", Counter++ ); Ioa_WriteAiger( pNew, pFileName, 0, 0 ); printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); } diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 571a6ef8..af92acc9 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -82,7 +82,7 @@ struct Gia_Obj_t_ unsigned Value; // application-specific value }; -// Value is currently use to store several types of information +// Value is currently used to store several types of information // - pointer to the next node in the hash table during structural hashing // - pointer to the node copy during duplication // - traversal ID of the node during traversal @@ -135,6 +135,7 @@ struct Gia_Man_t_ Vec_Int_t * vFlopClasses; // classes of flops for retiming/merging/etc unsigned char* pSwitching; // switching activity for each object Gia_Plc_t * pPlacement; // placement of the objects + int * pTravIds; // separate traversal ID representation }; @@ -309,13 +310,22 @@ static inline void Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){ static inline void Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj)); } static inline void Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj)); } -static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; } -static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; } -static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; } -static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; } -static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; } -static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); } -static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); } +static inline void Gia_ManResetTravId( Gia_Man_t * p ) { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1; } +static inline void Gia_ManIncrementTravId( Gia_Man_t * p ) { p->nTravIds++; } +static inline void Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId ) { pObj->Value = TravId; } +static inline void Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds; } +static inline void Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { pObj->Value = p->nTravIds - 1; } +static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds); } +static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { return ((int)pObj->Value == p->nTravIds - 1); } + +static inline void Gia_ManResetTravIdArray( Gia_Man_t * p ) { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1; } +static inline void Gia_ManIncrementTravIdArray( Gia_Man_t * p ) { p->nTravIds++; } +static inline void Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds; } +static inline void Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1; } +static inline int Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds); } +static inline int Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } +static inline void Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { p->pTravIds[Id] = p->nTravIds; } +static inline int Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id ) { return (p->pTravIds[Id] == p->nTravIds); } // AIG construction extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout ); @@ -402,6 +412,7 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr ); } static inline int Gia_ObjRepr( Gia_Man_t * p, int Id ) { return p->pReprs[Id].iRepr; } static inline void Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num ) { p->pReprs[Id].iRepr = Num; } +static inline void Gia_ObjUnsetRepr( Gia_Man_t * p, int Id ) { p->pReprs[Id].iRepr = GIA_VOID; } static inline int Gia_ObjProved( Gia_Man_t * p, int Id ) { return p->pReprs[Id].fProved; } static inline void Gia_ObjSetProved( Gia_Man_t * p, int Id ) { p->pReprs[Id].fProved = 1; } @@ -423,12 +434,15 @@ static inline int Gia_ObjNext( Gia_Man_t * p, int Id ) { r static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p->pNexts[Id] = Num; } static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } +static inline int Gia_ObjIsUsed( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; } static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); } +static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0; } +static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); } #define Gia_ManForEachConst( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else @@ -466,7 +480,9 @@ static inline int * Gia_ObjGateFanins( Gia_Man_t * p, int Id ) { re #define Gia_ManForEachObjReverse( p, pObj, i ) \ for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) #define Gia_ManForEachAnd( p, pObj, i ) \ - for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else + for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ ) if ( !Gia_ObjIsAnd(pObj) ) {} else +#define Gia_ManForEachAndReverse( p, pObj, i ) \ + for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- ) if ( !Gia_ObjIsAnd(pObj) ) {} else #define Gia_ManForEachCi( p, pObj, i ) \ for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ ) #define Gia_ManForEachCo( p, pObj, i ) \ @@ -498,6 +514,8 @@ extern void Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int extern Vec_Int_t * Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCsat.c ============================================================*/ extern Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); +/*=== giaCTas.c ============================================================*/ +extern Vec_Int_t * Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose ); /*=== giaCof.c =============================================================*/ extern void Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes ); extern Gia_Man_t * Gia_ManDupCof( Gia_Man_t * p, int iVar ); @@ -508,6 +526,7 @@ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int n extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes ); extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ); +extern Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p ); /*=== giaDup.c ============================================================*/ extern Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupOrderDfsReverse( Gia_Man_t * p ); @@ -620,6 +639,7 @@ extern void Gia_ManCheckMark1( Gia_Man_t * p ); extern void Gia_ManCleanValue( Gia_Man_t * p ); extern void Gia_ManFillValue( Gia_Man_t * p ); extern void Gia_ManSetPhase( Gia_Man_t * p ); +extern void Gia_ManCleanPhase( Gia_Man_t * p ); extern int Gia_ManLevelNum( Gia_Man_t * p ); extern void Gia_ManSetRefs( Gia_Man_t * p ); extern int * Gia_ManCreateMuxRefs( Gia_Man_t * p ); @@ -636,6 +656,14 @@ extern void Gia_ManPrintCounterExample( Gia_Cex_t * p ); extern int Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode ); extern int Gia_ManHasChoices( Gia_Man_t * p ); extern int Gia_ManHasDandling( Gia_Man_t * p ); +/*=== giaUtil.c ===========================================================*/ +typedef struct Tas_Man_t_ Tas_Man_t; +extern Tas_Man_t * Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit ); +extern void Tas_ManStop( Tas_Man_t * p ); +extern Vec_Int_t * Tas_ReadModel( Tas_Man_t * p ); +extern void Tas_ManSatPrintStats( Tas_Man_t * p ); +extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); + #ifdef __cplusplus } diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 4b3692e4..07e74e34 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -271,6 +271,47 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ) SeeAlso [] ***********************************************************************/ +Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ) +{ + Aig_Man_t * pNew; + Aig_Obj_t ** ppNodes; + Gia_Obj_t * pObj; + int i; + assert( p->pNexts == NULL && p->pReprs == NULL ); + assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 ); + // create the new manager + pNew = Aig_ManStart( Gia_ManAndNum(p) ); + pNew->pName = Gia_UtilStrsav( p->pName ); +// pNew->pSpec = Gia_UtilStrsav( p->pName ); + // create the PIs + ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) ); + ppNodes[0] = Aig_ManConst0(pNew); + Gia_ManForEachCi( p, pObj, i ) + ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew ); + // add logic for the POs + Gia_ManForEachCo( p, pObj, i ) + { + Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) ); + if ( i % nOutDelta != 0 ) + continue; + ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) ); + } + Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + ABC_FREE( ppNodes ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit ) { Aig_Man_t * pMan; diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h index 507e5143..0e29bf06 100644 --- a/src/aig/gia/giaAig.h +++ b/src/aig/gia/giaAig.h @@ -50,6 +50,7 @@ extern Gia_Man_t * Gia_ManFromAig( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSimple( Aig_Man_t * p ); extern Gia_Man_t * Gia_ManFromAigSwitch( Aig_Man_t * p ); extern Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices ); +extern Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta ); extern void Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia ); #ifdef __cplusplus diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c index e005dfc2..644ccda5 100644 --- a/src/aig/gia/giaCSat.c +++ b/src/aig/gia/giaCSat.c @@ -1020,6 +1020,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt // solve for each output Gia_ManForEachCo( pAig, pRoot, i ) { +// printf( "\n" ); + Vec_IntClear( vCex ); if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) ) { diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c index 8a3aef92..bcc1748f 100644 --- a/src/aig/gia/giaDfs.c +++ b/src/aig/gia/giaDfs.c @@ -264,6 +264,33 @@ int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes ) return Counter; } +/**Function************************************************************* + + Synopsis [Levelizes the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + Vec_Vec_t * vLevels; + int nLevels, Level, i; + nLevels = Gia_ManLevelNum( p ); + vLevels = Vec_VecStart( nLevels + 1 ); + Gia_ManForEachAnd( p, pObj, i ) + { + Level = Gia_ObjLevel( p, pObj ); + assert( Level <= nLevels ); + Vec_VecPush( vLevels, Level, pObj ); + } + return vLevels; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 041be0f5..8458268c 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -277,6 +277,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) assert( Gia_ManEquivCheckLits( p, nLits ) ); if ( fVerbose ) { + int Ent; +/* printf( "Const0 = " ); Gia_ManForEachConst( p, i ) printf( "%d ", i ); @@ -284,6 +286,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) Counter = 0; Gia_ManForEachClass( p, i ) Gia_ManEquivPrintOne( p, i, ++Counter ); +*/ + Gia_ManLevelNum( p ); + Gia_ManForEachClass( p, i ) + if ( i % 100 == 0 ) + { +// printf( "%d ", Gia_ManEquivCountOne(p, i) ); + Gia_ClassForEachObj( p, i, Ent ) + { + printf( "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) ); + } + printf( "\n" ); + } } } @@ -370,6 +384,15 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } + // check if there are any equivalences defined + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + if ( i == Gia_ManObjNum(p) ) + { + printf( "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" ); + return NULL; + } /* if ( !Gia_ManCheckTopoOrder( p ) ) { @@ -720,6 +743,16 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose ) printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" ); return NULL; } + // check if there are any equivalences defined + Gia_ManForEachObj( p, pObj, i ) + if ( Gia_ObjReprObj(p, i) != NULL ) + break; + if ( i == Gia_ManObjNum(p) ) + { + printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" ); + return NULL; + } + /* if ( !Gia_ManCheckTopoOrder( p ) ) { diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 7f4da081..37afde13 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -70,6 +70,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFree( p->vFlopClasses ); Vec_IntFree( p->vCis ); Vec_IntFree( p->vCos ); + ABC_FREE( p->pTravIds ); ABC_FREE( p->pPlacement ); ABC_FREE( p->pSwitching ); ABC_FREE( p->pCexSeq ); @@ -203,10 +204,10 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch ) void Gia_ManPrintStatsShort( Gia_Man_t * p ) { printf( "i/o =%7d/%7d ", Gia_ManPiNum(p), Gia_ManPoNum(p) ); -// printf( "ff =%7d ", Gia_ManRegNum(p) ); + printf( "ff =%7d ", Gia_ManRegNum(p) ); printf( "and =%8d ", Gia_ManAndNum(p) ); printf( "lev =%5d ", Gia_ManLevelNum(p) ); - printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); +// printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) ); printf( "\n" ); } diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index 54bc98dd..938c6363 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -317,6 +317,25 @@ void Gia_ManSetPhase( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Sets phases of the internal nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCleanPhase( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int i; + Gia_ManForEachObj( p, pObj, i ) + pObj->fPhase = 0; +} + +/**Function************************************************************* + Synopsis [Assigns levels.] Description [] @@ -883,17 +902,32 @@ int Gia_ManHasChoices( Gia_Man_t * p ) Gia_ManForEachObj( p, pObj, i ) { if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) + { +// printf( "%d ", i ); Counter1++; + } +// if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) +// Counter2++; + } +// printf( "\n" ); + Gia_ManForEachObj( p, pObj, i ) + { +// if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) ) +// Counter1++; if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) ) + { +// printf( "%d ", i ); Counter2++; + } } +// printf( "\n" ); if ( Counter1 == 0 ) { printf( "Warning: AIG has repr data-strucure but not reprs.\n" ); return 0; } -// printf( "%d nodes have reprs.\n", Counter1 ); -// printf( "%d nodes have nexts.\n", Counter2 ); + printf( "%d nodes have reprs.\n", Counter1 ); + printf( "%d nodes have nexts.\n", Counter2 ); // check if there are any internal nodes without fanout // make sure all nodes without fanout have representatives // make sure all nodes with fanout have no representatives diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 6f70f7d3..79bfa2fb 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -4,6 +4,7 @@ SRC += src/aig/gia/gia.c \ src/aig/gia/giaCof.c \ src/aig/gia/giaCSatOld.c \ src/aig/gia/giaCSat.c \ + src/aig/gia/giaCTas.c \ src/aig/gia/giaDfs.c \ src/aig/gia/giaDup.c \ src/aig/gia/giaEmbed.c \ diff --git a/src/aig/int/int.h b/src/aig/int/int.h index c9c5cd1a..1487b9bf 100644 --- a/src/aig/int/int.h +++ b/src/aig/int/int.h @@ -57,6 +57,7 @@ struct Inter_ManParams_t_ int fCheckKstep; // check using K-step induction int fUseBias; // bias decisions to global variables int fUseBackward; // perform backward interpolation + int fUseSeparate; // solve each output separately int fVerbose; // print verbose statistics }; diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c index cab0302f..6d29dfb9 100644 --- a/src/aig/int/intCore.c +++ b/src/aig/int/intCore.c @@ -53,6 +53,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p ) p->fCheckKstep = 1; // check using K-step induction p->fUseBias = 0; // bias decisions to global variables p->fUseBackward = 0; // perform backward interpolation + p->fUseSeparate = 0; // solve each output separately p->fVerbose = 0; // print verbose statistics } diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make index 7f885a90..2af0f4e0 100644 --- a/src/aig/ntl/module.make +++ b/src/aig/ntl/module.make @@ -6,6 +6,7 @@ SRC += src/aig/ntl/ntlCheck.c \ src/aig/ntl/ntlInsert.c \ src/aig/ntl/ntlMan.c \ src/aig/ntl/ntlMap.c \ + src/aig/ntl/ntlNames.c \ src/aig/ntl/ntlObj.c \ src/aig/ntl/ntlReadBlif.c \ src/aig/ntl/ntlSweep.c \ diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h index a82b4d6c..0955214e 100644 --- a/src/aig/ntl/ntl.h +++ b/src/aig/ntl/ntl.h @@ -76,6 +76,7 @@ struct Ntl_Man_t_ Vec_Ptr_t * vVisNodes; // the nodes of the abstracted part Vec_Int_t * vBox1Cios; // the first COs of the boxes Vec_Int_t * vRegClasses; // the classes of registers in the AIG + Vec_Int_t * vRstClasses; // the classes of reset registers in the AIG Aig_Man_t * pAig; // the extracted AIG Tim_Man_t * pManTime; // the timing manager int iLastCi; // the last true CI @@ -83,6 +84,7 @@ struct Ntl_Man_t_ void (*pNalF)(void *); // additional data void (*pNalD)(void *,void *); // additional data void (*pNalW)(void *,void *); // additional data + void (*pNalR)(void *); // additional data // hashing names into models Ntl_Mod_t ** pModTable; // the hash table of names into models int nModTableSize; // the allocated table size @@ -112,6 +114,9 @@ struct Ntl_Mod_t_ // clocks of the model Vec_Ptr_t * vClocks; // the clock signals Vec_Vec_t * vClockFlops; // the flops of each clock + // resets of the model + Vec_Ptr_t * vResets; // the reset signals + Vec_Vec_t * vResetFlops; // the ASYNC flops of each reset // delay information Vec_Int_t * vDelays; Vec_Int_t * vTimeInputs; @@ -121,7 +126,7 @@ struct Ntl_Mod_t_ Ntl_Mod_t * pNext; void * pCopy; int nUsed, nRems; -}; +}; struct Ntl_Reg_t_ { @@ -139,6 +144,7 @@ struct Ntl_Obj_t_ unsigned Id : 28; // object ID int nFanins; // the number of fanins int nFanouts; // the number of fanouts + int Reset; // reset of the flop union { // functionality Ntl_Mod_t * pImplem; // model (for boxes) char * pSop; // SOP (for logic nodes) @@ -162,9 +168,10 @@ struct Ntl_Net_t_ int iTemp; // other data }; Ntl_Obj_t * pDriver; // driver of the net - unsigned NetId : 28; // unique ID of the net + unsigned NetId : 27; // unique ID of the net unsigned nVisits : 2; // the number of times the net is visted unsigned fMark : 1; // temporary mark + unsigned fMark2 : 1; // temporary mark unsigned fFixed : 1; // the fixed net char pName[0]; // the name of this net }; @@ -329,11 +336,18 @@ extern ABC_DLL void Ntl_ManFree( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManPrintStats( Ntl_Man_t * p ); extern ABC_DLL Tim_Man_t * Ntl_ManReadTimeMan( Ntl_Man_t * p ); extern ABC_DLL void Ntl_ManPrintTypes( Ntl_Man_t * p ); +extern ABC_DLL int Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 ); +extern ABC_DLL void Ntl_ManPrintClocks( Ntl_Man_t * p ); +extern ABC_DLL void Ntl_ManPrintResets( Ntl_Man_t * p ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern ABC_DLL Ntl_Mod_t * Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld ); extern ABC_DLL void Ntl_ModelFree( Ntl_Mod_t * p ); extern ABC_DLL Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ); +extern ABC_DLL int Ntl_ModelCountLut0( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCountLut1( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCountBuf( Ntl_Mod_t * p ); +extern ABC_DLL int Ntl_ModelCountInv( Ntl_Mod_t * p ); /*=== ntlMap.c ============================================================*/ extern ABC_DLL Vec_Ptr_t * Ntl_MappingAlloc( int nLuts, int nVars ); extern ABC_DLL Vec_Ptr_t * Ntl_MappingFromAig( Aig_Man_t * p ); @@ -350,6 +364,7 @@ extern ABC_DLL Ntl_Obj_t * Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, ch extern ABC_DLL char * Ntl_ManStoreName( Ntl_Man_t * p, char * pName ); extern ABC_DLL char * Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop ); extern ABC_DLL char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName ); +extern ABC_DLL int Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout ); /*=== ntlSweep.c ==========================================================*/ extern ABC_DLL int Ntl_ManSweep( Ntl_Man_t * p, int fVerbose ); /*=== ntlTable.c ==========================================================*/ @@ -374,7 +389,6 @@ extern ABC_DLL Ntl_Man_t * Ioa_ReadBlif( char * pFileName, int fCheck ); extern ABC_DLL void Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName ); extern ABC_DLL void Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName ); /*=== ntlUtil.c ==========================================================*/ -extern ABC_DLL int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot ); extern ABC_DLL int Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot ); extern ABC_DLL Ntl_Net_t * Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo ); extern ABC_DLL int Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p ); diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c index 6afeba26..55a961df 100644 --- a/src/aig/ntl/ntlExtract.c +++ b/src/aig/ntl/ntlExtract.c @@ -371,6 +371,7 @@ int Ntl_ManCollapseBoxSeq1_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq ) pNet->nVisits = 2; // remember the class of this register Vec_IntPush( p->vRegClasses, p->pNal ? pBox->iTemp : pObj->LatchId.regClass ); + Vec_IntPush( p->vRstClasses, p->pNal ? pBox->Reset : -1 ); } // compute AIG for the internal nodes Ntl_ModelForEachPo( pModel, pObj, i ) @@ -505,6 +506,7 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq ) assert( Vec_PtrSize(p->vCos) != 0 ); Vec_IntClear( p->vBox1Cios ); Vec_IntClear( p->vRegClasses ); + Vec_IntClear( p->vRstClasses ); // clear net visited flags pRoot = Ntl_ManRootModel(p); assert( Ntl_ModelLatchNum(pRoot) == 0 ); @@ -797,6 +799,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan { pNet->pCopy2 = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); Nwk_ObjAddFanin( pNode, pNet->pCopy2 ); + pNode->fInvert = (Nwk_ObjFanin0(pNode)->pFunc == Hop_ManConst0(pNtk->pManHop)); // fixed on June 7, 2009 } } } diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c index e98a3b46..64af98f4 100644 --- a/src/aig/ntl/ntlFraig.c +++ b/src/aig/ntl/ntlFraig.c @@ -423,6 +423,171 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev /**Function************************************************************* + Synopsis [Counts the number of resets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManAigCountResets( Ntl_Man_t * pNtl ) +{ + Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl); + Ntl_Obj_t * pBox; + int i, Counter = -1; + Ntl_ModelForEachObj( pModel, pBox, i ) + Counter = ABC_MAX( Counter, pBox->Reset ); + return Counter + 1; +} + +/**Function************************************************************* + + Synopsis [Transforms sequential AIG to allow for async reset.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ntl_ManAigToRst( Ntl_Man_t * pNtl, Aig_Man_t * p ) +{ + Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl); + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i, iRegNum, iRstNum, Counter = 0; + int nResets = Ntl_ManAigCountResets( pNtl ); + assert( pNtl->pNal != NULL ); + assert( Aig_ManRegNum(p) > 0 ); + assert( Vec_IntSize(pNtl->vRstClasses) == Aig_ManRegNum(p) ); +//printf( "Number of resets before synthesis = %d.\n", nResets ); + // create the PIs + Aig_ManCleanData( p ); + Aig_ManSetPioNumbers( p ); + // create the new manager + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + pNew->pSpec = Aig_UtilStrsav( p->pSpec ); + // create special PIs + for ( i = 0; i < nResets; i++ ) + Aig_ObjCreatePi( pNew ); + // duplicate internal nodes + Aig_ManForEachPi( p, pObj, i ) + pObj->pData = Aig_ObjCreatePi( pNew ); + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjIsNode(pObj) ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + else if ( Aig_ObjIsPo(pObj) ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + else if ( Aig_ObjIsPi(pObj) ) + { +// pObj->pData = Aig_ObjCreatePi( pNew ); + iRegNum = Aig_ObjPioNum(pObj) - (Aig_ManPiNum(p) - Aig_ManRegNum(p)); + if ( iRegNum < 0 ) + continue; + iRstNum = Vec_IntEntry(pNtl->vRstClasses, iRegNum); + if ( iRstNum < 0 ) + continue; + assert( iRstNum < nResets ); + pObj->pData = Aig_And( pNew, pObj->pData, Aig_ManPi(pNew, iRstNum) ); // could be NOT(pi) + Counter++; + } + else if ( Aig_ObjIsConst1(pObj) ) + pObj->pData = Aig_ManConst1(pNew); + else + assert( 0 ); + } + assert( Aig_ManNodeNum(p) + Counter == Aig_ManNodeNum(pNew) ); + if ( (Counter = Aig_ManCleanup( pNew )) ) + printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", Counter ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Remaps equivalence classes from the new nodes to the old ones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManRemapClassesLcorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew ) +{ + Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl); + Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr; + int i, nResets = Ntl_ManAigCountResets( pNtl ); + int nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p); + assert( pNew->pReprs != NULL ); + assert( nResets == Aig_ManPiNum(pNew) - Aig_ManPiNum(p) ); + Aig_ManReprStart( p, Aig_ManObjNumMax(p) ); + Aig_ManForEachLoSeq( pNew, pObjNew, i ) + { + pObj = Aig_ManPi( p, i - nResets ); + pObjNewRepr = pNew->pReprs[pObjNew->Id]; + if ( pObjNewRepr == NULL ) + continue; + if ( pObjNewRepr == Aig_ManConst1(pNew) ) + { + Aig_ObjCreateRepr( p, Aig_ManConst1(p), pObj ); + continue; + } + assert( Aig_ObjIsPi(pObjNewRepr) ); + // find the corresponding representative node + pObjRepr = Aig_ManPi( p, Aig_ObjPioNum(pObjNewRepr) - nResets ); + // if they belong to different domains, quit + if ( Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObj) - nTruePis ) != + Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObjRepr) - nTruePis ) ) + continue; + Aig_ObjCreateRepr( p, pObjRepr, pObj ); + } +} + +/**Function************************************************************* + + Synopsis [Remaps equivalence classes from the new nodes to the old ones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManRemapClassesScorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew ) +{ + Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr; + int i; + // map things back + Aig_ManForEachObj( p, pObj, i ) + { + pObjNew = pObj->pData; + assert( pObjNew != NULL && !Aig_IsComplement(pObjNew) ); + pObjNew->pData = pObj; + } + // remap the classes + Aig_ManForEachObj( pNew, pObjNew, i ) + { + pObjNewRepr = pNew->pReprs[pObjNew->Id]; + if ( pObjNewRepr == NULL ) + continue; + pObj = pObjNew->pData; + pObjRepr = pObjNewRepr->pData; + assert( Aig_ObjId(pObjRepr) < Aig_ObjId(pObj) ); + Aig_ObjCreateRepr( p, pObjRepr, pObj ); + } +} + + +/**Function************************************************************* + Synopsis [Performs sequential cleanup.] Description [] @@ -451,9 +616,21 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe //Ntl_ManPrintStats( pNew ); //Aig_ManPrintStats( pAigCol ); - // perform SCL for the given design - pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); - Aig_ManStop( pTemp ); + // perform SCL + if ( p->pNal ) + { + Aig_Man_t * pAigRst; + pAigRst = Ntl_ManAigToRst( pNew, pAigCol ); + pTemp = Aig_ManScl( pAigRst, fLatchConst, fLatchEqual, fVerbose ); + Aig_ManStop( pTemp ); + Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst ); + Aig_ManStop( pAigRst ); + } + else + { + pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose ); + Aig_ManStop( pTemp ); + } // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); @@ -493,11 +670,23 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fScorrGia, int fUseCS return pNew; } - // perform LCORR for the given design + // perform LCORR pPars->fScorrGia = fScorrGia; pPars->fUseCSat = fUseCSat; - pTemp = Ssw_LatchCorrespondence( pAigCol, pPars ); - Aig_ManStop( pTemp ); + if ( p->pNal ) + { + Aig_Man_t * pAigRst; + pAigRst = Ntl_ManAigToRst( pNew, pAigCol ); + pTemp = Ssw_LatchCorrespondence( pAigRst, pPars ); + Aig_ManStop( pTemp ); + Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst ); + Aig_ManStop( pAigRst ); + } + else + { + pTemp = Ssw_LatchCorrespondence( pAigCol, pPars ); + Aig_ManStop( pTemp ); + } // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose ); @@ -522,6 +711,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars ) { Ntl_Man_t * pNew, * pAux; Aig_Man_t * pAig, * pAigCol, * pTemp; + assert( 0 ); // not updated for nal // collapse the AIG pAig = Ntl_ManExtract( p ); @@ -571,9 +761,21 @@ Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars ) return pNew; } - // perform SCL for the given design - pTemp = Ssw_SignalCorrespondence( pAigCol, pPars ); - Aig_ManStop( pTemp ); + // perform SCL + if ( p->pNal ) + { + Aig_Man_t * pAigRst; + pAigRst = Ntl_ManAigToRst( pNew, pAigCol ); + pTemp = Ssw_SignalCorrespondence( pAigRst, pPars ); + Aig_ManStop( pTemp ); + Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst ); + Aig_ManStop( pAigRst ); + } + else + { + pTemp = Ssw_SignalCorrespondence( pAigCol, pPars ); + Aig_ManStop( pTemp ); + } // finalize the transformation pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose ); diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c index eb967bdc..750eb8f7 100644 --- a/src/aig/ntl/ntlInsert.c +++ b/src/aig/ntl/ntlInsert.c @@ -290,6 +290,190 @@ void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName ) SeeAlso [] ***********************************************************************/ +Ntl_Man_t * Ntl_ManInsertNtk2( Ntl_Man_t * p, Nwk_Man_t * pNtk ) +{ + int fWriteConstants = 1; + char Buffer[1000]; + Vec_Ptr_t * vObjs; + Vec_Int_t * vTruth; + Vec_Int_t * vCover; + Ntl_Mod_t * pRoot; + Ntl_Obj_t * pNode; + Ntl_Net_t * pNet, * pNetCo; + Nwk_Obj_t * pObj, * pFanin; + int i, k, nDigits; + unsigned * pTruth; + assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) ); + assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) ); + p = Ntl_ManStartFrom( p ); + pRoot = Ntl_ManRootModel( p ); + assert( Ntl_ModelNodeNum(pRoot) == 0 ); + // set the correspondence between the PI/PO nodes + Ntl_ManForEachCiNet( p, pNet, i ) + Nwk_ManCi( pNtk, i )->pCopy = pNet; + // create a new node for each LUT + vTruth = Vec_IntAlloc( 1 << 16 ); + vCover = Vec_IntAlloc( 1 << 16 ); + nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) ); + // go through the nodes in the topological order + vObjs = Nwk_ManDfs( pNtk ); + Vec_PtrForEachEntry( vObjs, pObj, i ) + { + if ( !Nwk_ObjIsNode(pObj) ) + continue; +/* + if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 ) + { + pObj->pCopy = NULL; + continue; + } +*/ + // skip constant drivers if they only drive COs + if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 ) + { + Nwk_Obj_t * pFanout; + int i; + Nwk_ObjForEachFanout( pObj, pFanout, i ) + if ( Nwk_ObjIsNode(pFanout) ) + break; + if ( i == Nwk_ObjFanoutNum(pObj) ) + { + pObj->pCopy = NULL; + continue; + } + } + + pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) ); + pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 ); + if ( Hop_IsComplement(pObj->pFunc) ) + Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) ); + if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) ) + { + Nwk_ObjForEachFanin( pObj, pFanin, k ) + { + pNet = pFanin->pCopy; + if ( pNet == NULL ) + { + printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" ); + return 0; + } + Ntl_ObjSetFanin( pNode, pNet, k ); + } + } + else if ( Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) ) + { + pObj->pFunc = Hop_ManConst0(pNtk->pManHop); + pNode->nFanins = 0; + } + else if ( Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) ) + { + pObj->pFunc = Hop_ManConst1(pNtk->pManHop); + pNode->nFanins = 0; + } + pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover ); + sprintf( Buffer, "lut%0*d", nDigits, i ); + if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) ) + { + printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" ); + return 0; + } + pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer ); + if ( !Ntl_ModelSetNetDriver( pNode, pNet ) ) + { + printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" ); + return 0; + } + pObj->pCopy = pNet; + } + Vec_PtrFree( vObjs ); + Vec_IntFree( vCover ); + Vec_IntFree( vTruth ); + // mark the nets driving special boxes + if ( p->pNalR ) + p->pNalR( p ); + // mark CIs and outputs of the registers + Ntl_ManForEachCiNet( p, pNetCo, i ) + pNetCo->fMark = 1; + // update the CO pointers + Ntl_ManForEachCoNet( p, pNetCo, i ) + { + if ( pNetCo->fMark ) + continue; + pNetCo->fMark = 1; + // get the corresponding PO and its driver + pObj = Nwk_ManCo( pNtk, i ); + pFanin = Nwk_ObjFanin0( pObj ); + // get the net driving this PO + pNet = pFanin->pCopy; + if ( pNet == NULL ) // constant net + { + assert( fWriteConstants ); + pNode = Ntl_ModelCreateNode( pRoot, 0 ); + pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" ); + } + else + if ( Nwk_ObjFanoutNum(pFanin) == 1 && Ntl_ObjIsNode(pNet->pDriver) && !pNet->fMark2 ) + { + pNode = pNet->pDriver; + if ( !Ntl_ModelClearNetDriver( pNode, pNet ) ) + { + printf( "Ntl_ManInsertNtk(): Internal error! Net already has no driver.\n" ); + return NULL; + } + // remove this net + Ntl_ModelDeleteNet( pRoot, pNet ); + Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL ); + // update node's function + if ( pObj->fInvert ) + Kit_PlaComplement( pNode->pSop ); + } + else + { +/* + if ( fWriteConstants && Ntl_ObjFaninNum(pNet->pDriver) == 0 ) + { + pNode = Ntl_ModelCreateNode( pRoot, 0 ); + pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" ); + } + else +*/ + { +// assert( Ntl_ObjFaninNum(pNet->pDriver) != 0 ); + pNode = Ntl_ModelCreateNode( pRoot, 1 ); + pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" ); + Ntl_ObjSetFanin( pNode, pNet, 0 ); + } + } + // update the CO driver net + assert( pNetCo->pDriver == NULL ); + if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) ) + { + printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" ); + return NULL; + } + } + // clean CI/CO marks + Ntl_ManUnmarkCiCoNets( p ); + if ( !Ntl_ManCheck( p ) ) + { + printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName ); + return NULL; + } + return p; +} + + +/**Function************************************************************* + + Synopsis [Inserts the given mapping into the netlist.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) { char Buffer[1000]; @@ -418,7 +602,6 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk ) return p; } - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c index da7e2317..a95c2352 100644 --- a/src/aig/ntl/ntlMan.c +++ b/src/aig/ntl/ntlMan.c @@ -51,6 +51,7 @@ Ntl_Man_t * Ntl_ManAlloc() p->vVisNodes = Vec_PtrAlloc( 1000 ); p->vBox1Cios = Vec_IntAlloc( 1000 ); p->vRegClasses = Vec_IntAlloc( 1000 ); + p->vRstClasses = Vec_IntAlloc( 1000 ); // start the manager p->pMemObjs = Aig_MmFlexStart(); p->pMemSops = Aig_MmFlexStart(); @@ -123,6 +124,7 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld ) { ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy; ((Ntl_Obj_t *)pBox->pCopy)->iTemp = pBox->iTemp; + ((Ntl_Obj_t *)pBox->pCopy)->Reset = pBox->Reset; } Ntl_ManForEachCiNet( pOld, pNet, i ) Vec_PtrPush( pNew->vCis, pNet->pCopy ); @@ -197,6 +199,7 @@ void Ntl_ManFree( Ntl_Man_t * p ) if ( p->vCos ) Vec_PtrFree( p->vCos ); if ( p->vVisNodes ) Vec_PtrFree( p->vVisNodes ); if ( p->vRegClasses) Vec_IntFree( p->vRegClasses ); + if ( p->vRstClasses) Vec_IntFree( p->vRstClasses ); if ( p->vBox1Cios ) Vec_IntFree( p->vBox1Cios ); if ( p->pMemObjs ) Aig_MmFlexStop( p->pMemObjs, 0 ); if ( p->pMemSops ) Aig_MmFlexStop( p->pMemSops, 0 ); @@ -294,14 +297,14 @@ void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk ) SeeAlso [] ***********************************************************************/ -int Nwk_ManStatsRegs( Ntl_Man_t * p ) +int Ntl_ManStatsRegs( Ntl_Man_t * p ) { Ntl_Mod_t * pRoot; Ntl_Obj_t * pObj; int i, Counter = 0; pRoot = Ntl_ManRootModel( p ); Ntl_ModelForEachBox( pRoot, pObj, i ) - if ( strcmp(pObj->pImplem->pName, "dff") == 0 ) + if ( strcmp(pObj->pImplem->pName, "m_dff") == 0 ) Counter++; return Counter; } @@ -317,6 +320,22 @@ int Nwk_ManStatsRegs( Ntl_Man_t * p ) SeeAlso [] ***********************************************************************/ +int Ntl_ManStatsLuts( Ntl_Man_t * p ) +{ + return Ntl_ModelLut1Num( Ntl_ManRootModel(p) ) + Ntl_ModelNodeNum( Ntl_ManRootModel(p) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Nwk_ManStatsLuts( Nwk_Man_t * pNtk ) { return pNtk ? Nwk_ManNodeNum(pNtk) : -1; @@ -353,13 +372,13 @@ int Nwk_ManStatsLevs( Nwk_Man_t * pNtk ) void Nwk_ManPrintStatsUpdate( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk, int nRegInit, int nLutInit, int nLevInit, int Time ) { - printf( "FF =%7d (%4.1f%%) ", Nwk_ManStatsRegs(p), 100.0*(nRegInit-Nwk_ManStatsRegs(p))/nRegInit ); + printf( "FF =%7d (%5.1f%%) ", Ntl_ManStatsRegs(p), nRegInit ? (100.0*(nRegInit-Ntl_ManStatsRegs(p))/nRegInit) : 0.0 ); if ( pNtk == NULL ) - printf( "Mapping is not available. " ); + printf( "Mapping is not available. " ); else { - printf( "Lut =%7d (%4.1f%%) ", Nwk_ManStatsLuts(pNtk), 100.0*(nLutInit-Nwk_ManStatsLuts(pNtk))/nLutInit ); - printf( "Lev =%4d (%4.1f%%) ", Nwk_ManStatsLevs(pNtk), 100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit ); + printf( "Lut =%7d (%5.1f%%) ", Ntl_ManStatsLuts(p), nLutInit ? (100.0*(nLutInit-Ntl_ManStatsLuts(p))/nLutInit) : 0.0 ); + printf( "Lev =%4d (%5.1f%%) ", Nwk_ManStatsLevs(pNtk), nLevInit ? (100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit) : 0.0 ); } ABC_PRT( "Time", clock() - Time ); } @@ -461,6 +480,101 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p ) /**Function************************************************************* + Synopsis [Procedure used for sorting the nodes in decreasing order of levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 ) +{ + int Diff = Vec_PtrSize(*pp1) - Vec_PtrSize(*pp2); + if ( Diff > 0 ) + return -1; + if ( Diff < 0 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Saves the model type.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManPrintClocks( Ntl_Man_t * p ) +{ + Vec_Ptr_t * vFlops; + Ntl_Net_t * pNet; + Ntl_Mod_t * pModel; + int i; + pModel = Ntl_ManRootModel( p ); + if ( Ntl_ModelBoxNum(pModel) == 0 ) + return; + if ( pModel->vClockFlops ) + { + printf( "CLOCK STATISTICS:\n" ); + Vec_VecForEachLevel( pModel->vClockFlops, vFlops, i ) + { + pNet = Vec_PtrEntry( pModel->vClocks, i ); + printf( "Clock %2d : Name = %30s Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) ); + if ( i == 10 ) + { + printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vClockFlops) ); + break; + } + } + } +// printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Saves the model type.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ntl_ManPrintResets( Ntl_Man_t * p ) +{ + Vec_Ptr_t * vFlops; + Ntl_Net_t * pNet; + Ntl_Mod_t * pModel; + int i; + pModel = Ntl_ManRootModel( p ); + if ( Ntl_ModelBoxNum(pModel) == 0 ) + return; + if ( pModel->vResetFlops ) + { + printf( "RESET STATISTICS:\n" ); + Vec_VecForEachLevel( pModel->vResetFlops, vFlops, i ) + { + pNet = Vec_PtrEntry( pModel->vResets, i ); + printf( "Reset %2d : Name = %30s Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) ); + if ( i == 10 ) + { + printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vResetFlops) ); + break; + } + } + } +// printf( "\n" ); +} + +/**Function************************************************************* + Synopsis [Allocates the model.] Description [] @@ -643,6 +757,8 @@ void Ntl_ModelFree( Ntl_Mod_t * p ) if ( p->vDelays ) Vec_IntFree( p->vDelays ); if ( p->vClocks ) Vec_PtrFree( p->vClocks ); if ( p->vClockFlops ) Vec_VecFree( p->vClockFlops ); + if ( p->vResets ) Vec_PtrFree( p->vResets ); + if ( p->vResetFlops ) Vec_VecFree( p->vResetFlops ); Vec_PtrFree( p->vNets ); Vec_PtrFree( p->vObjs ); Vec_PtrFree( p->vPis ); @@ -699,6 +815,90 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init ) } +/**Function************************************************************* + + Synopsis [Count constant nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCountLut0( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pNode; + int i, Counter = 0; + Ntl_ModelForEachNode( p, pNode, i ) + if ( Ntl_ObjFaninNum(pNode) == 0 ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Count single-output nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCountLut1( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pNode; + int i, Counter = 0; + Ntl_ModelForEachNode( p, pNode, i ) + if ( Ntl_ObjFaninNum(pNode) == 1 ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Count buffers] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCountBuf( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pNode; + int i, Counter = 0; + Ntl_ModelForEachNode( p, pNode, i ) + if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '1' ) + Counter++; + return Counter; +} + +/**Function************************************************************* + + Synopsis [Count inverters.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ModelCountInv( Ntl_Mod_t * p ) +{ + Ntl_Obj_t * pNode; + int i, Counter = 0; + Ntl_ModelForEachNode( p, pNode, i ) + if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '0' ) + Counter++; + return Counter; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c index 55924db9..4946c4e3 100644 --- a/src/aig/ntl/ntlObj.c +++ b/src/aig/ntl/ntlObj.c @@ -160,6 +160,7 @@ Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts ) p->Type = NTL_OBJ_BOX; p->nFanins = nFanins; p->nFanouts = nFanouts; + p->Reset = -1; pModel->nObjs[NTL_OBJ_BOX]++; return p; } @@ -285,6 +286,27 @@ char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName ) } +/**Function************************************************************* + + Synopsis [Returns the index of the fanin in the fanin list of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout ) +{ + Ntl_Net_t * pObj; + int i; + Ntl_ObjForEachFanout( pNode, pObj, i ) + if ( pObj == pFanout ) + return i; + return -1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c index 6d1b6c83..6a4b18d5 100644 --- a/src/aig/ntl/ntlUtil.c +++ b/src/aig/ntl/ntlUtil.c @@ -30,27 +30,6 @@ /**Function************************************************************* - Synopsis [Counts COs that are connected to the internal nodes through invs/bufs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot ) -{ - Ntl_Obj_t * pObj; - int i, Counter = 0; - Ntl_ModelForEachNode( pRoot, pObj, i ) - if ( Ntl_ObjFaninNum(pObj) == 1 ) - Counter++; - return Counter; -} - -/**Function************************************************************* - Synopsis [Reads the maximum number of fanins.] Description [] @@ -370,6 +349,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer if ( Vec_IntSize(pMan->vRegClasses) == 0 ) { printf( "Ntl_ManReportRegClasses(): Register classes are not defined.\n" ); +// return (Vec_Vec_t *)Vec_PtrAlloc(0); return NULL; } // find the largest class diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c index e6865840..5812358b 100644 --- a/src/aig/nwk/nwkMap.c +++ b/src/aig/nwk/nwkMap.c @@ -321,6 +321,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI pObjNew = Nwk_ManCreateCo( pNtk ); pObjNew->fInvert = Aig_ObjFaninC0(pObj); Nwk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData ); +//printf( "%d ", pObjNew->Id ); } else if ( Aig_ObjIsConst1(pObj) ) { @@ -331,6 +332,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI assert( 0 ); pObj->pData = pObjNew; } +//printf( "\n" ); Vec_PtrFree( vIfToAig ); pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 ); Nwk_ManMinimumBase( pNtk, 0 ); diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c index 10b7b462..9fc292ea 100644 --- a/src/aig/nwk/nwkUtil.c +++ b/src/aig/nwk/nwkUtil.c @@ -513,6 +513,49 @@ int Nwk_ManMinimumBaseNode( Nwk_Obj_t * pObj, Vec_Int_t * vTruth, int fVerbose ) SeeAlso [] ***********************************************************************/ +int Nwk_ManMinimumBaseInt( Nwk_Man_t * pNtk, int fVerbose ) +{ + Vec_Int_t * vTruth; + Nwk_Obj_t * pObj; + int i, Counter = 0; + vTruth = Vec_IntAlloc( 1 << 16 ); + Nwk_ManForEachNode( pNtk, pObj, i ) + Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose ); + if ( fVerbose && Counter ) + printf( "Support minimization reduced support of %d nodes.\n", Counter ); + Vec_IntFree( vTruth ); + return Counter; +} + +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nwk_ManMinimumBaseRec( Nwk_Man_t * pNtk, int fVerbose ) +{ + int i, clk = clock(); + for ( i = 0; Nwk_ManMinimumBaseInt( pNtk, fVerbose ); i++ ); + ABC_PRT( "Minbase", clock() - clk ); +} + +/**Function************************************************************* + + Synopsis [Minimizes the support of all nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose ) { Vec_Int_t * vTruth; @@ -585,6 +628,7 @@ void Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose ) } } Vec_IntFree( vTruth ); +// Nwk_ManMinimumBase( pNtk, fVerbose ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index f6845acd..3da92fc0 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -24,6 +24,7 @@ #include "satSolver.h" #include "satStore.h" #include "ssw.h" +#include "ioa.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -681,7 +682,7 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex } return pCex; } - + /**Function************************************************************* Synopsis [Performs proof-based abstraction using BMC of the given depth.] @@ -859,6 +860,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, printf( "Refining abstraction...\n" ); for ( Iter = 0; ; Iter++ ) { + char FileName[100]; pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose ); if ( pTemp == NULL ) break; @@ -869,9 +871,16 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, Aig_ManPrintStats( pResult ); else printf( " -----------------------------------------------------\n" ); + // output the intermediate result of abstraction + sprintf( FileName, "gabs%02d.aig", Iter ); + Ioa_WriteAiger( pResult, FileName, 0, 0 ); + printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName ); + // check if the ratio is reached if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio ) { printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio ); + Aig_ManStop( pResult ); + pResult = NULL; break; } } diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index d56d97a9..57759594 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -87,7 +87,7 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, Saig_Bmc_t * p; Aig_Obj_t * pObj; int i, Lit; - assert( Aig_ManRegNum(pAig) > 0 ); +// assert( Aig_ManRegNum(pAig) > 0 ); p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) ); memset( p, 0, sizeof(Saig_Bmc_t) ); // set parameters @@ -589,7 +589,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) ); printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll ); - } + } for ( Iter = 0; ; Iter++ ) { clk2 = clock(); diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index f8799e38..240168e6 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -162,6 +162,8 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax return pFrames; } +#include "utilMem.h" + /**Function************************************************************* Synopsis [Performs BMC for the given AIG.] @@ -228,6 +230,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim // create the SAT solver clk = clock(); pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) ); +//if ( s_fInterrupt ) +//return -1; pSat = sat_solver_new(); sat_solver_setnvars( pSat, pCnf->nVars ); for ( i = 0; i < pCnf->nClauses; i++ ) @@ -255,6 +259,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim int clkPart = clock(); Aig_ManForEachPo( pFrames, pObj, i ) { +//if ( s_fInterrupt ) +//return -1; Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 ); if ( fVerbose ) { diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index ead0ece5..97b91b1d 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -251,7 +251,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t { Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; - assert( Aig_ManRegNum(p) > 0 ); +// assert( Aig_ManRegNum(p) > 0 ); assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) ); // start simulation data Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL ); diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c index deb8d5d4..0e99b1e8 100644 --- a/src/aig/ssw/sswSim.c +++ b/src/aig/ssw/sswSim.c @@ -1280,11 +1280,11 @@ void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex ) ***********************************************************************/ int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p ) -{ +{ Ssw_Sml_t * pSml; Aig_Obj_t * pObj; int RetValue, i, k, iBit; - assert( Aig_ManRegNum(pAig) > 0 ); +// assert( Aig_ManRegNum(pAig) > 0 ); assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) ); // start a new sequential simulator pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 ); diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 6973bb64..ae345467 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -1334,7 +1334,7 @@ Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk ) // filter POs k = m = 0; Abc_NtkForEachCo( pNtk, pObj, i ) - { + { if ( Abc_ObjIsPo(pObj) ) { // remove constant nodes and PI pointers diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 660bf3e1..9d04c0bf 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -153,6 +153,7 @@ static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDProve2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSimSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMatch ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -311,6 +312,7 @@ static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9If ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Era ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Dch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbcTestNew ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -543,6 +545,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dsec", Abc_CommandDSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "dprove", Abc_CommandDProve, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "dprove2", Abc_CommandDProve2, 0 ); Cmd_CommandAdd( pAbc, "Verification", "absec", Abc_CommandAbSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "simsec", Abc_CommandSimSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "match", Abc_CommandMatch, 0 ); @@ -631,6 +634,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "AIG", "&embed", Abc_CommandAbc9Embed, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&if", Abc_CommandAbc9If, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&era", Abc_CommandAbc9Era, 0 ); + Cmd_CommandAdd( pAbc, "AIG", "&dch", Abc_CommandAbc9Dch, 0 ); Cmd_CommandAdd( pAbc, "AIG", "&test", Abc_CommandAbc9Test, 0 ); Cmd_CommandAdd( pAbc, "Various", "testnew", Abc_CommandAbcTestNew, 0 ); @@ -672,6 +676,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) void For_ManFileExperiment(); // For_ManFileExperiment(); } + { + } } @@ -5437,7 +5443,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pNtkRes == NULL ) { fprintf( pErr, "Miter computation has failed.\n" ); - return 1; + return 0; } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); @@ -6539,23 +6545,24 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv ) int nIterMax; int fPartition; int fReorder; + int fReorderImage; int fVerbose; int c; - extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); - extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ); + extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nBddMax = 50000; - nIterMax = 1000; - fPartition = 1; - fReorder = 1; - fVerbose = 0; + nBddMax = 50000; + nIterMax = 1000; + fPartition = 1; + fReorder = 1; + fReorderImage = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "BFprovh" ) ) != EOF ) { switch ( c ) { @@ -6587,6 +6594,9 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'r': fReorder ^= 1; break; + case 'o': + fReorderImage ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -6626,16 +6636,17 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv ) } */ // Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); - Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); + Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose ); return 0; usage: - fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" ); + fprintf( pErr, "usage: reach [-BF num] [-provh]\n" ); fprintf( pErr, "\t verifies sequential miter using BDD-based reachability\n" ); fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax ); fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax ); fprintf( pErr, "\t-p : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" ); fprintf( pErr, "\t-r : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" ); + fprintf( pErr, "\t-o : toggles BDD variable reordering during image computation [default = %s]\n", fReorderImage? "yes": "no" ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -9554,7 +9565,6 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; - extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars ); pNtk = Abc_FrameReadNtk(pAbc); @@ -9564,7 +9574,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfvh" ) ) != EOF ) { switch ( c ) { @@ -9616,6 +9626,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'c': pPars->fUseCSat ^= 1; break; + case 'f': + pPars->fLightSynth ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -9646,7 +9659,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" ); + fprintf( pErr, "usage: dch [-WCS num] [-sptgcfvh]\n" ); fprintf( pErr, "\t computes structural choices using a new approach\n" ); fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -9656,6 +9669,7 @@ usage: fprintf( pErr, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" ); fprintf( pErr, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); fprintf( pErr, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); + fprintf( pErr, "\t-f : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -16581,7 +16595,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Fra_SecSetDefaultParams( pSecPar ); // pSecPar->TimeLimit = 300; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijkouwvh" ) ) != EOF ) { switch ( c ) { @@ -16686,6 +16700,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'j': pSecPar->fInterpolation ^= 1; break; + case 'k': + pSecPar->fInterSeparate ^= 1; + break; + case 'o': + pSecPar->fReorderImage ^= 1; + break; + case 'u': + pSecPar->fReadUnsolved ^= 1; + break; case 'w': pSecPar->fVeryVerbose ^= 1; break; @@ -16712,12 +16735,21 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_NtkDarProve( pNtk, pSecPar ); pAbc->pCex = pNtk->pSeqModel; // temporary ??? - // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p ) - + // read back the resulting unsolved reduced sequential miter + if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 ) + { + char FileName[100]; + sprintf( FileName, "sm%02d.aig", pSecPar->nSMnumber ); + pNtk = Io_Read( FileName, Io_ReadFileType(FileName), 1 ); + if ( pNtk == NULL ) + printf( "Cannot read back unsolved reduced sequential miter \"%s\",\n", FileName ); + else + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + } return 0; usage: - fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" ); + fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijouwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax ); fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit ); @@ -16734,11 +16766,105 @@ usage: fprintf( pErr, "\t-f : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" ); fprintf( pErr, "\t-i : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" ); fprintf( pErr, "\t-j : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" ); -// fprintf( pErr, "\t-n : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" ); + fprintf( pErr, "\t-k : toggles applying interpolation to each output [default = %s]\n", pSecPar->fInterSeparate? "yes": "no" ); + fprintf( pErr, "\t-o : toggles using BDD variable reordering during image computation [default = %s]\n", pSecPar->fReorderImage? "yes": "no" ); + fprintf( pErr, "\t-u : toggles reading back unsolved reduced sequential miter [default = %s]\n", pSecPar->fReadUnsolved? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDProve2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int nConfLast; + int fSeparate; + int fVeryVerbose; + int fVerbose; + int c; + + extern int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nConfLast = 75000; + fSeparate = 0; + fVeryVerbose = 0; + fVerbose = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ckwvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLast = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLast < 0 ) + goto usage; + break; + case 'k': + fSeparate ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + printf( "This command works only for structrally hashed networks. Run \"st\".\n" ); + return 0; + } + if ( Abc_NtkLatchNum(pNtk) == 0 ) + { + printf( "This command works only for sequential networks.\n" ); + return 0; + } + // perform verification + Abc_NtkDProve2( pNtk, nConfLast, fSeparate, fVeryVerbose, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: dprove2 [-C num] [-kwvh]\n" ); + fprintf( pErr, "\t improved integrated solver of sequential miters\n" ); + fprintf( pErr, "\t-C num : the conflict limit during final BMC [default = %d]\n", nConfLast ); + fprintf( pErr, "\t-k : toggles solving each output separately [default = %s]\n", fSeparate? "yes": "no" ); + fprintf( pErr, "\t-w : toggles very verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; } /**Function************************************************************* @@ -18098,7 +18224,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Inter_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbkvh" ) ) != EOF ) { switch ( c ) { @@ -18159,6 +18285,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': pPars->fUseBackward ^= 1; break; + case 'k': + pPars->fUseSeparate ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -18174,7 +18303,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } if ( !Abc_NtkIsStrash(pNtk) ) - { + { fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); return 0; } @@ -18185,10 +18314,29 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( Abc_NtkPoNum(pNtk) != 1 ) { - fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" ); - return 0; + if ( pPars->fUseSeparate ) + { + printf( "Each of %d outputs will be solved separately.\n", Abc_NtkPoNum(pNtk) ); + Abc_NtkDarBmcInter( pNtk, pPars ); + } + else + { + Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk ); + printf( "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) ); + if ( !Abc_NtkCombinePos( pNtkNew, 0 ) ) + { + Abc_NtkDelete( pNtkNew ); + printf( "ORing outputs has failed.\n" ); + return 0; + } + Abc_NtkDarBmcInter( pNtkNew, pPars ); + Abc_NtkDelete( pNtkNew ); + } + } + else + { + Abc_NtkDarBmcInter( pNtk, pPars ); } - Abc_NtkDarBmcInter( pNtk, pPars ); return 0; usage: @@ -18205,6 +18353,7 @@ usage: fprintf( pErr, "\t-c : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" ); fprintf( pErr, "\t-g : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" ); fprintf( pErr, "\t-b : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" ); + fprintf( pErr, "\t-k : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -18585,7 +18734,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: fprintf( pErr, "usage: ind [-FC num] [-vh]\n" ); - fprintf( pErr, "\t runs K-step induction for the property output\n" ); + fprintf( pErr, "\t runs the inductive case of the K-step induction\n" ); fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax ); fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); @@ -19959,7 +20108,7 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfvh" ) ) != EOF ) { switch ( c ) { @@ -20005,6 +20154,9 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': pPars->fSimulateTfo ^= 1; break; + case 'f': + pPars->fLightSynth ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -20027,12 +20179,12 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc8Dch(): Tranformation of the AIG has failed.\n" ); return 1; } - Aig_ManStop( pAbc->pAbc8Aig ); +// Aig_ManStop( pAbc->pAbc8Aig ); pAbc->pAbc8Aig = pAigNew; return 0; usage: - fprintf( stdout, "usage: *dch [-WCS num] [-sptvh]\n" ); + fprintf( stdout, "usage: *dch [-WCS num] [-sptfvh]\n" ); fprintf( stdout, "\t computes structural choices using a new approach\n" ); fprintf( stdout, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -20040,6 +20192,7 @@ usage: fprintf( stdout, "\t-s : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" ); fprintf( stdout, "\t-p : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" ); fprintf( stdout, "\t-t : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" ); + fprintf( stdout, "\t-f : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" ); fprintf( stdout, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -20973,7 +21126,7 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) ) { - fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational (run \"*fraig\").\n" ); + fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational.\n" ); return 0; } @@ -21092,7 +21245,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) ) { - fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational (run \"*fraig\").\n" ); + fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational.\n" ); return 0; } @@ -21285,7 +21438,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) ) { - fprintf( stdout, "The network is combinational (run \"*fraig\").\n" ); + fprintf( stdout, "The network is combinational.\n" ); return 0; } @@ -21518,7 +21671,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) ) { - fprintf( stdout, "The network is combinational (run \"*fraig\").\n" ); + fprintf( stdout, "The network is combinational.\n" ); return 0; } @@ -23890,7 +24043,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCSat = 0; Cec_ManSatSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmftcvh" ) ) != EOF ) { switch ( c ) { @@ -23936,6 +24089,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'f': pPars->fFirstStop ^= 1; break; + case 't': + pPars->fLearnCls ^= 1; + break; case 'c': fCSat ^= 1; break; @@ -23955,7 +24111,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) { Vec_Int_t * vCounters; Vec_Str_t * vStatus; - if ( pPars->fNonChrono ) + if ( pPars->fLearnCls ) + vCounters = Tas_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose ); + else if ( pPars->fNonChrono ) vCounters = Cbs_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose ); else vCounters = Cbs_ManSolveMiter( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose ); @@ -23970,7 +24128,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfcvh]\n" ); + fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfctvh]\n" ); fprintf( stdout, "\t performs SAT solving for the combinational outputs\n" ); fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax ); @@ -23979,6 +24137,7 @@ usage: fprintf( stdout, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" ); fprintf( stdout, "\t-f : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" ); fprintf( stdout, "\t-c : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" ); + fprintf( stdout, "\t-t : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -24139,18 +24298,23 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) { - char * pFileName = "gsrm.aig"; - Gia_Man_t * pTemp; + char * pFileName = "gsrm.aig"; + char * pFileName2 = "gsyn.aig"; + Gia_Man_t * pTemp, * pAux; int c, fVerbose = 0; + int fSynthesis = 0; int fDualOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "dsvh" ) ) != EOF ) { switch ( c ) { case 'd': fDualOut ^= 1; break; + case 's': + fSynthesis ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -24165,22 +24329,38 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Abc_CommandAbc9Srm(): There is no AIG.\n" ); return 1; } -// pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut ); -// Gia_ManStop( pTemp ); pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose ); if ( pTemp ) { + pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); + Gia_ManStop( pAux ); + Gia_WriteAiger( pTemp, pFileName, 0, 0 ); printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName ); Gia_ManPrintStatsShort( pTemp ); Gia_ManStop( pTemp ); } + if ( fSynthesis ) + { + pTemp = Gia_ManEquivReduce( pAbc->pAig, 1, fDualOut, fVerbose ); + if ( pTemp ) + { + pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); + Gia_ManStop( pAux ); + + Gia_WriteAiger( pTemp, pFileName2, 0, 0 ); + printf( "Reduced original network was written into file \"%s\".\n", pFileName2 ); + Gia_ManPrintStatsShort( pTemp ); + Gia_ManStop( pTemp ); + } + } return 0; usage: - fprintf( stdout, "usage: &srm [-dvh]\n" ); + fprintf( stdout, "usage: &srm [-dsvh]\n" ); fprintf( stdout, "\t writes speculatively reduced model into file \"%s\"\n", pFileName ); fprintf( stdout, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" ); + fprintf( stdout, "\t-s : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" ); fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( stdout, "\t-h : print the command usage\n"); return 1; @@ -24765,7 +24945,7 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pTemp = NULL; int c, fVerbose = 0; int fMiter = 0; - int nStatesMax = 1000000; + int nStatesMax = 10000000; extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF ) @@ -24834,6 +25014,75 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ +// extern void Hcd_ComputeChoicesTest( Gia_Man_t * pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose ); + Gia_Man_t * pTemp = NULL; + int nBTLimit = 100; + int fSynthesis = 1; + int fUseMiniSat = 0; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Csmvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( stdout, "Command line switch \"-C\" should be followed by a positive integer.\n" ); + goto usage; + } + nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBTLimit < 0 ) + goto usage; + break; + case 's': + fSynthesis ^= 1; + break; + case 'm': + fUseMiniSat ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pAig == NULL ) + { + printf( "Abc_CommandAbc9Test(): There is no AIG.\n" ); + return 1; + } +// Hcd_ComputeChoicesTest( pAbc->pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose ); + return 0; + +usage: + fprintf( stdout, "usage: &dch [-C num] [-smvh]\n" ); + fprintf( stdout, "\t computing choices using the latest algorithm\n" ); + fprintf( stdout, "\t-C num : the max number of states to traverse (num > 0) [default = %d]\n", nBTLimit ); + fprintf( stdout, "\t-s : toggle printing verbose information [default = %s]\n", fSynthesis? "yes": "no" ); + fprintf( stdout, "\t-m : toggle using MiniSat as a SAT solver [default = %s]\n", fUseMiniSat? "yes": "no" ); + fprintf( stdout, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( stdout, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t * pTemp = NULL; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 873b78d1..1220cb40 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -895,45 +895,37 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in ***********************************************************************/ Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars ) { - extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose ); - extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars ); + extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose ); + extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ); - Vec_Ptr_t * vAigs; Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; - int i, clk; + Gia_Man_t * pGia; + int clk; assert( Abc_NtkIsStrash(pNtk) ); pMan = Abc_NtkToDar( pNtk, 0, 0 ); if ( pMan == NULL ) return NULL; clk = clock(); if ( pPars->fSynthesis ) - { -// vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose ); - vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 ); - Aig_ManStop( pMan ); - // swap around the first and the last - pTemp = Vec_PtrPop( vAigs ); - Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); - Vec_PtrWriteEntry( vAigs, 0, pTemp ); - } + pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 ); else { - vAigs = Vec_PtrAlloc( 1 ); - Vec_PtrPush( vAigs, pMan ); + pGia = Gia_ManFromAig( pMan ); + Aig_ManStop( pMan ); } pPars->timeSynth = clock() - clk; if ( pPars->fUseGia ) - pMan = Cec_ComputeChoices( vAigs, pPars ); + pMan = Cec_ComputeChoices( pGia, pPars ); else - pMan = Dch_ComputeChoices( vAigs, pPars ); + { + pMan = Gia_ManToAigSkip( pGia, 3 ); + Gia_ManStop( pGia ); + pMan = Dch_ComputeChoices( pTemp = pMan, pPars ); + Aig_ManStop( pTemp ); + } pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); -// pNtkAig = Abc_NtkFromDar( pNtk, pMan ); Aig_ManStop( pMan ); - // cleanup - Vec_PtrForEachEntry( vAigs, pTemp, i ) - Aig_ManStop( pTemp ); - Vec_PtrFree( vAigs ); return pNtkAig; } @@ -1535,6 +1527,18 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in return pNtkAig; } +/* +#include <signal.h> +#include "utilMem.h" +static void sigfunc( int signo ) +{ + if (signo == SIGINT) { + printf("SIGINT received!\n"); + s_fInterrupt = 1; + } +} +*/ + /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] @@ -1550,6 +1554,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, { Aig_Man_t * pMan; int status, RetValue = -1, clk = clock(); + +/* + s_fInterrupt = 0; + if ( signal(SIGINT,sigfunc) == SIG_ERR ) + { + printf("Could not setup signal handler for SIGINT!\n"); + return RetValue; + } + printf("Waiting for SIGINT. Press Ctrl+C to exit.\n"); +// while ( !s_fInterrupt ); +// return RetValue; +*/ + // derive the AIG manager pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) @@ -1572,8 +1589,12 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta, printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit ); else // if ( RetValue == 0 ) { + extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex ); + Fra_Cex_t * pCex = pNtk->pSeqModel; printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame ); + + Aig_ManCounterExampleValueTest( pMan, pCex ); } } else @@ -1639,33 +1660,105 @@ ABC_PRT( "Time", clock() - clk ); SeeAlso [] ***********************************************************************/ -int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ) +int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars ) { - Aig_Man_t * pMan; int RetValue, iFrame, clk = clock(); - // derive the AIG manager - pMan = Abc_NtkToDar( pNtk, 0, 1 ); - if ( pMan == NULL ) + assert( pMan->nRegs > 0 ); + if ( pPars->fUseSeparate ) { - printf( "Converting miter into AIG has failed.\n" ); - return -1; + Aig_Man_t * pTemp, * pAux; + Aig_Obj_t * pObjPo; + int i, Counter = 0; + Saig_ManForEachPo( pMan, pObjPo, i ) + { + if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) ) + continue; + pTemp = Aig_ManDupOneOutput( pMan, i, 1 ); + pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 ); + Aig_ManStop( pAux ); + if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) ) + { + Aig_ManStop( pTemp ); + continue; + } + RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame ); + if ( pTemp->pSeqModel ) + { + Ssw_Cex_t * pCex; + pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; + pCex->iPo = i; + Aig_ManStop( pTemp ); + break; + } + // if solved, remove the output + if ( RetValue == 1 ) + { + Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) ); +// printf( "Output %3d : Solved ", i ); + } + else + { + Counter++; +// printf( "Output %3d : Undec ", i ); + } +// Aig_ManPrintStats( pTemp ); + Aig_ManStop( pTemp ); + printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) ); + } + Aig_ManCleanup( pMan ); + if ( pMan->pSeqModel == NULL ) + { + printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pMan) ); + if ( Counter ) + RetValue = -1; + } +/* + pMan = Aig_ManDupUnsolvedOutputs( pTemp = pMan, 1 ); + Aig_ManStop( pTemp ); + pMan = Aig_ManScl( pTemp = pMan, 1, 1, 0 ); + Aig_ManStop( pTemp ); +*/ + } + else + { + RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame ); } - assert( pMan->nRegs > 0 ); - RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame ); if ( RetValue == 1 ) printf( "Property proved. " ); else if ( RetValue == 0 ) - { printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness). ", iFrame ); - ABC_FREE( pNtk->pModel ); - ABC_FREE( pNtk->pSeqModel ); - pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; - } else if ( RetValue == -1 ) printf( "Property UNDECIDED. " ); else assert( 0 ); ABC_PRT( "Time", clock() - clk ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars ) +{ + Aig_Man_t * pMan; + pMan = Abc_NtkToDar( pNtk, 0, 1 ); + if ( pMan == NULL ) + { + printf( "Converting miter into AIG has failed.\n" ); + return -1; + } + Abc_NtkDarBmcInter_int( pMan, pPars ); + ABC_FREE( pNtk->pModel ); + ABC_FREE( pNtk->pSeqModel ); + pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; Aig_ManStop( pMan ); return 1; } @@ -2411,7 +2504,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in else { RetValue = 0; - printf( "Simulation of %d frames with %d words did not assert the outputs. ", + printf( "Simulation of %d frames with %d words did not assert the outputs. ", nFrames, nWords ); } Gia_ManStop( pGia ); @@ -2439,7 +2532,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in else { RetValue = 0; - printf( "Simulation of %d frames with %d words did not assert the outputs. ", + printf( "Simulation of %d frames with %d words did not assert the outputs. ", nFrames, nWords ); } Fra_SmlStop( pSml ); @@ -3187,14 +3280,14 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu SeeAlso [] ***********************************************************************/ -void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose ) +void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose ) { - extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent ); + extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); Aig_Man_t * pMan; pMan = Abc_NtkToDar( pNtk, 0, 1 ); if ( pMan == NULL ) return; - Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 ); + Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 ); ABC_FREE( pNtk->pModel ); ABC_FREE( pNtk->pSeqModel ); pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL; diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c index 36e56e7b..95c7103a 100644 --- a/src/base/abci/abcTiming.c +++ b/src/base/abci/abcTiming.c @@ -157,7 +157,7 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall ) if ( pNtk->pManTime == NULL ) pNtk->pManTime = Abc_ManTimeStart(); pNtk->pManTime->tReqDef.Rise = Rise; - pNtk->pManTime->tReqDef.Rise = Fall; + pNtk->pManTime->tReqDef.Fall = Fall; pNtk->pManTime->tReqDef.Worst = ABC_MAX( Rise, Fall ); } @@ -185,7 +185,7 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall vTimes = pNtk->pManTime->vArrs; pTime = vTimes->pArray[ObjId]; pTime->Rise = Rise; - pTime->Fall = Rise; + pTime->Fall = Fall; pTime->Worst = ABC_MAX( Rise, Fall ); } @@ -213,7 +213,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall vTimes = pNtk->pManTime->vReqs; pTime = vTimes->pArray[ObjId]; pTime->Rise = Rise; - pTime->Fall = Rise; + pTime->Fall = Fall; pTime->Worst = ABC_MAX( Rise, Fall ); } diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 9214bb52..aaea7312 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -12,6 +12,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcDar.c \ src/base/abci/abcDebug.c \ src/base/abci/abcDelay.c \ + src/base/abci/abcDprove2.c \ src/base/abci/abcDress.c \ src/base/abci/abcDsd.c \ src/base/abci/abcExtract.c \ diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c index dae8b783..d1adaf90 100644 --- a/src/base/io/ioWriteBlif.c +++ b/src/base/io/ioWriteBlif.c @@ -579,7 +579,8 @@ void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk ) pTime = Abc_NodeReadArrival(pNode); if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall ) continue; - fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(pNode), pTime->Rise, pTime->Fall ); +// fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(pNode), pTime->Rise, pTime->Fall ); + fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(Abc_ObjFanout0(pNode)), pTime->Rise, pTime->Fall ); } } diff --git a/src/base/main/main.c b/src/base/main/main.c index 738f217c..f74fb21a 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -23,10 +23,12 @@ // this line should be included in the library project //#define ABC_LIB +//#define ABC_USE_BINARY 1 + //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// - + static int TypeCheck( Abc_Frame_t * pAbc, char * s); //////////////////////////////////////////////////////////////////////// @@ -46,7 +48,11 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s); SeeAlso [] ***********************************************************************/ +#if defined(ABC_USE_BINARY) +int main_( int argc, char * argv[] ) +#else int main( int argc, char * argv[] ) +#endif { Abc_Frame_t * pAbc; char sCommandUsr[500], sCommandTmp[100], sReadCmd[20], sWriteCmd[20], c; @@ -67,7 +73,7 @@ int main( int argc, char * argv[] ) pAbc = Abc_FrameGetGlobalFrame(); // default options - fBatch = 0; + fBatch = 0; fInitSource = 1; fInitRead = 0; fFinalWrite = 0; @@ -313,127 +319,6 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s ) -/**Function************************************************************* - - Synopsis [Find the file name.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -char * Abc_MainFileName( char * pFileName ) -{ - static char Buffer[200]; - char * pExtension; - assert( strlen(pFileName) < 190 ); - pExtension = Extra_FileNameExtension( pFileName ); - if ( pExtension == NULL ) - sprintf( Buffer, "%s.opt", pFileName ); - else - { - strncpy( Buffer, pFileName, pExtension-pFileName-1 ); - sprintf( Buffer+(pExtension-pFileName-1), ".opt.%s", pExtension ); - } - return Buffer; -} - -/**Function************************************************************* - - Synopsis [The main() procedure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int main_( int argc, char * argv[] ) -{ - extern void Nwk_ManPrintStatsUpdate( void * p, void * pAig, void * pNtk, - int nRegInit, int nLutInit, int nLevInit, int Time ); - char * pComs[20] = - { -/*00*/ "*r -am ", -/*01*/ "*w -abc 1.aig", -/*02*/ "*lcorr -nc",//; *ps", -/*03*/ "*scorr -nc",//; *ps", -/*04*/ "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", -/*05*/ "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", -/*06*/ "*w ", -/*07*/ "*w -abc 2.aig", -/*08*/ "miter -mc 1.aig 2.aig; sim -F 4 -W 4 -mv" - }; - char Command[1000]; - int i, nComs; - Abc_Frame_t * pAbc; - FILE * pFile; - int nRegInit, nLutInit, nLevInit; - int clkStart = clock(); - - // added to detect memory leaks: -#if defined(_DEBUG) && defined(_MSC_VER) - _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); -#endif - - // check that the file is present - if ( argc != 2 ) - { - printf( "Expecting one command argument (file name).\n" ); - return 0; - } - pFile = fopen( argv[1], "r" ); - if ( pFile == NULL ) - { - printf( "Cannot open file \"%s\".\n", argv[1] ); - return 0; - } - fclose( pFile ); - - // count the number of commands - for ( nComs = 0; nComs < 20; nComs++ ) - if ( pComs[nComs] == NULL ) - break; - // perform the commands - printf( "Reading design \"%s\"...\n", argv[1] ); - pAbc = Abc_FrameGetGlobalFrame(); - for ( i = 0; i < nComs; i++ ) - { - - if ( i == 0 ) - sprintf( Command, "%s%s", pComs[i], argv[1] ); - else if ( i == 6 ) - sprintf( Command, "%s%s", pComs[i], Abc_MainFileName(argv[1]) ); - else - sprintf( Command, "%s", pComs[i] ); - if ( Cmd_CommandExecute( pAbc, Command ) ) - { - printf( "Internal command %d failed.\n", i ); - return 0; - } - if ( i == 0 ) - { - extern int Nwk_ManStatsRegs( void * p ); - extern int Nwk_ManStatsLuts( void * pNtk ); - extern int Nwk_ManStatsLevs( void * pNtk ); - nRegInit = Nwk_ManStatsRegs( pAbc->pAbc8Ntl ); - nLutInit = Nwk_ManStatsLuts( pAbc->pAbc8Nwk ); - nLevInit = Nwk_ManStatsLevs( pAbc->pAbc8Nwk ); - } - if ( i >= 1 && i <= 5 ) - Nwk_ManPrintStatsUpdate( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk, - nRegInit, nLutInit, nLevInit, clkStart ); - } - Abc_Stop(); - printf( "Writing optimized design \"%s\"...\n", Abc_MainFileName(argv[1]) ); - ABC_PRT( "Total time", clock() - clkStart ); - printf( "\n" ); - return 0; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index 31e0afa9..81070bd8 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -28,6 +28,9 @@ static Abc_Frame_t * s_GlobalFrame = NULL; +extern void * Aig_ManDupSimple( void * p ); +extern void Aig_ManStop( void * pAig ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -148,11 +151,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p ) if ( p->pManDec ) Dec_ManStop( p->pManDec ); if ( p->dd ) Extra_StopManager( p->dd ); if ( p->vStore ) Vec_PtrFree( p->vStore ); + if ( p->pSave1 ) Aig_ManStop( p->pSave1 ); + if ( p->pSave2 ) Aig_ManStop( p->pSave2 ); + if ( p->pSave3 ) Aig_ManStop( p->pSave3 ); + if ( p->pSave4 ) Aig_ManStop( p->pSave4 ); Abc_FrameDeleteAllNetworks( p ); ABC_FREE( p ); s_GlobalFrame = NULL; } + /**Function************************************************************* Synopsis [] @@ -513,6 +521,58 @@ Abc_Frame_t * Abc_FrameReadGlobalFrame() return s_GlobalFrame; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FrameSetSave1( void * pAig ) +{ + Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame(); + if ( pFrame->pSave1 ) + Aig_ManStop( pFrame->pSave1 ); + pFrame->pSave1 = pAig; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FrameSetSave2( void * pAig ) +{ + Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame(); + if ( pFrame->pSave2 ) + Aig_ManStop( pFrame->pSave2 ); + pFrame->pSave2 = pAig; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * Abc_FrameReadSave1() { void * pAig = Abc_FrameGetGlobalFrame()->pSave1; Abc_FrameGetGlobalFrame()->pSave1 = NULL; return pAig; } +void * Abc_FrameReadSave2() { void * pAig = Abc_FrameGetGlobalFrame()->pSave2; Abc_FrameGetGlobalFrame()->pSave2 = NULL; return pAig; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index ca8717be..01bf5eb2 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -82,6 +82,11 @@ struct Abc_Frame_t_ void * pAig; void * pCex; + void * pSave1; + void * pSave2; + void * pSave3; + void * pSave4; + // the addition to keep the best Ntl that can be used to restore void * pAbc8NtlBestDelay; // the best delay, Ntl void * pAbc8NtlBestArea; // the best area diff --git a/src/map/amap/amapRule.c b/src/map/amap/amapRule.c index 212f7631..27de49ee 100644 --- a/src/map/amap/amapRule.c +++ b/src/map/amap/amapRule.c @@ -296,7 +296,7 @@ Kit_DsdPrint( stdout, pNtk ); { assert( iNod > 1 ); pNod = Amap_LibNod( pLib, Amap_Lit2Var(iNod) ); - assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins ); +// assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins ); pSet = (Amap_Set_t *)Aig_MmFlexEntryFetch( pLib->pMemSet, sizeof(Amap_Set_t) ); memset( pSet, 0, sizeof(Amap_Set_t) ); pSet->iGate = pGate->Id; diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index fd1078a6..ca57868d 100644 --- a/src/map/if/ifMap.c +++ b/src/map/if/ifMap.c @@ -207,7 +207,9 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP for ( pTemp = pObj->pEquiv; pTemp; pTemp = pTemp->pEquiv ) { assert( pTemp->nRefs == 0 ); - assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 ); +// assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 ); // June 9, 2009 + if ( pTemp->pCutSet->nCuts == 0 ) + continue; // go through the cuts of this node If_ObjForEachCut( pTemp, pCutTemp, i ) { diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c index 942caa8e..cc64d8b8 100644 --- a/src/map/mapper/mapperLib.c +++ b/src/map/mapper/mapperLib.c @@ -174,15 +174,20 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib ) { Abc_Frame_t * pAbc = Abc_FrameGetGlobalFrame(); char * pNameGeneric; - char FileNameGenlib[100]; - char FileNameSuper[100]; - char CommandSuper[500]; - char CommandRead[500]; + char * FileNameGenlib; + char * FileNameSuper; + char * CommandSuper; + char * CommandRead; FILE * pFile; if ( pLib == NULL ) return 0; + FileNameGenlib = ABC_ALLOC( char, 10000 ); + FileNameSuper = ABC_ALLOC( char, 10000 ); + CommandSuper = ABC_ALLOC( char, 10000 ); + CommandRead = ABC_ALLOC( char, 10000 ); + // write the current library into the file sprintf( FileNameGenlib, "%s_temp", Mio_LibraryReadName(pLib) ); pFile = fopen( FileNameGenlib, "w" ); @@ -197,6 +202,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib ) sprintf( CommandSuper, "super -l 1 -i 5 -d 10000000 -a 10000000 -t 100 %s", FileNameGenlib ); if ( Cmd_CommandExecute( pAbc, CommandSuper ) ) { + ABC_FREE( FileNameGenlib ); + ABC_FREE( FileNameSuper ); + ABC_FREE( CommandSuper ); + ABC_FREE( CommandRead ); fprintf( stdout, "Cannot execute command \"%s\".\n", CommandSuper ); return 0; } @@ -215,6 +224,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib ) unlink( FileNameSuper ); #endif fprintf( stdout, "Cannot execute command \"%s\".\n", CommandRead ); + ABC_FREE( FileNameGenlib ); + ABC_FREE( FileNameSuper ); + ABC_FREE( CommandSuper ); + ABC_FREE( CommandRead ); return 0; } @@ -225,6 +238,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib ) unlink( FileNameSuper ); #endif */ + ABC_FREE( FileNameGenlib ); + ABC_FREE( FileNameSuper ); + ABC_FREE( CommandSuper ); + ABC_FREE( CommandRead ); return 1; } diff --git a/src/map/super/superGate.c b/src/map/super/superGate.c index 7bc5e703..cb7d8d78 100644 --- a/src/map/super/superGate.c +++ b/src/map/super/superGate.c @@ -67,8 +67,8 @@ struct Super_ManStruct_t_ int Time; // the runtime of the generation procedure int TimeLimit; // the runtime limit (in seconds) int TimeSec; // the time passed (in seconds) - int TimeStop; // the time to stop computation (in miliseconds) - int TimePrint; // the time to print message + double TimeStop; // the time to stop computation (in miliseconds) + double TimePrint; // the time to print message }; struct Super_GateStruct_t_ @@ -1107,10 +1107,12 @@ void Super_WriteLibrary( Super_Man_t * pMan ) { Super_Gate_t * pGate, * pGateNext; FILE * pFile; - char FileName[100]; + char * FileName; char * pNameGeneric; int i, Counter; + FileName = ABC_ALLOC( char, 10000 ); + // get the file name pNameGeneric = Extra_FileNameGeneric( pMan->pName ); sprintf( FileName, "%s.super_old", pNameGeneric ); @@ -1152,6 +1154,8 @@ if ( pMan->fVerbose ) printf( "The supergates are written using old format \"%s\" ", FileName ); printf( "(%0.3f Mb).\n", ((double)Extra_FileSize(FileName))/(1<<20) ); } + + ABC_FREE( FileName ); } /**Function************************************************************* @@ -1251,11 +1255,13 @@ void Super_WriteLibraryTree( Super_Man_t * pMan ) { Super_Gate_t * pSuper; FILE * pFile; - char FileName[100]; + char * FileName; char * pNameGeneric; int i, Counter; int posStart; + FileName = ABC_ALLOC( char, 10000 ); + // get the file name pNameGeneric = Extra_FileNameGeneric( pMan->pName ); sprintf( FileName, "%s.super", pNameGeneric ); @@ -1286,6 +1292,8 @@ if ( pMan->fVerbose ) printf( "The supergates are written using new format \"%s\" ", FileName ); printf( "(%0.3f Mb).\n", ((double)Extra_FileSize(FileName))/(1<<20) ); } + + ABC_FREE( FileName ); } /**Function************************************************************* diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 35a391ba..f58e3ddf 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -153,6 +153,15 @@ typedef unsigned __int64 ABC_UINT64_T; #define ABC_MIN(a,b) ((a) < (b) ? (a) : (b)) #define ABC_INFINITY (100000000) +#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))) +#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC))) +#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)) +#define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.2f Mb ", 1.0*(f)/(1<<20))) + + +//#define ABC_USE_MEM_REC 1 + +#ifndef ABC_USE_MEM_REC #define ABC_ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) #define ABC_CALLOC(type, num) ((type *) calloc((num), sizeof(type))) #define ABC_FALLOC(type, num) ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num))) @@ -160,11 +169,16 @@ typedef unsigned __int64 ABC_UINT64_T; #define ABC_REALLOC(type, obj, num) \ ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ ((type *) malloc(sizeof(type) * (num)))) - -#define ABC_PRT(a,t) (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC))) -#define ABC_PRTn(a,t) (printf("%s = ", (a)), printf("%6.2f sec ", (float)(t)/(float)(CLOCKS_PER_SEC))) -#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0)) -#define ABC_PRM(a,f) (printf("%s = ", (a)), printf("%7.2f Mb ", 1.0*(f)/(1<<20))) +#else +#include "utilMem.h" +#define ABC_ALLOC(type, num) ((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num)))) +#define ABC_CALLOC(type, num) ((type *) Util_MemRecAlloc(calloc((num), sizeof(type)))) +#define ABC_FALLOC(type, num) ((type *) memset(Util_MemRecAlloc(malloc(sizeof(type) * (num))), 0xff, sizeof(type) * (num))) +#define ABC_FREE(obj) ((obj) ? (free((char *) Util_MemRecFree(obj)), (obj) = 0) : 0) +#define ABC_REALLOC(type, obj, num) \ + ((obj) ? ((type *) Util_MemRecAlloc(realloc((char *)(Util_MemRecFree(obj)), sizeof(type) * (num)))) : \ + ((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num))))) +#endif #ifdef __cplusplus } diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h index 825c8bee..33fb6c6b 100644 --- a/src/misc/util/util_hack.h +++ b/src/misc/util/util_hack.h @@ -58,7 +58,7 @@ extern "C" { # define ARGS(args) args # else # define ARGS(args) () -# endif +# endif #endif extern long Extra_CpuTime(); diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index 915265f3..d6ed53b9 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -37,7 +37,6 @@ /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index c77a3a17..bd10154c 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -572,6 +572,28 @@ static inline char Vec_StrPop( Vec_Str_t * p ) /**Function************************************************************* + Synopsis [Reverses the order of entries.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_StrReverseOrder( Vec_Str_t * p ) +{ + int i, Temp; + for ( i = 0; i < p->nSize/2; i++ ) + { + Temp = p->pArray[i]; + p->pArray[i] = p->pArray[p->nSize-1-i]; + p->pArray[p->nSize-1-i] = Temp; + } +} + +/**Function************************************************************* + Synopsis [Comparison procedure for two clauses.] Description [] diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c index e49fd61d..008b6863 100644 --- a/src/opt/mfs/mfsResub.c +++ b/src/opt/mfs/mfsResub.c @@ -207,7 +207,7 @@ p->timeInt += clock() - clk; printf( "\n" ); } iVar = -1; - while ( 1 ) + while ( 1 ) { if ( fVeryVerbose ) { |