diff options
41 files changed, 846 insertions, 297 deletions
@@ -2798,6 +2798,10 @@ SOURCE=.\src\aig\kit\kit.h # End Source File # Begin Source File +SOURCE=.\src\aig\kit\kitAig.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\kit\kitBdd.c # End Source File # Begin Source File diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index fe237142..63456b5d 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -68,19 +68,23 @@ typedef enum { // the AIG node struct Aig_Obj_t_ // 8 words { - void * pData; // misc (cuts, copy, etc) Aig_Obj_t * pNext; // strashing table Aig_Obj_t * pFanin0; // fanin Aig_Obj_t * pFanin1; // fanin - unsigned long Type : 3; // object type - unsigned long fPhase : 1; // value under 000...0 pattern - unsigned long fMarkA : 1; // multipurpose mask - unsigned long fMarkB : 1; // multipurpose mask - unsigned long nRefs : 26; // reference count + unsigned int Type : 3; // object type + unsigned int fPhase : 1; // value under 000...0 pattern + unsigned int fMarkA : 1; // multipurpose mask + unsigned int fMarkB : 1; // multipurpose mask + unsigned int nRefs : 26; // reference count unsigned Level : 24; // the level of this node unsigned nCuts : 8; // the number of cuts int TravId; // unique ID of last traversal involving the node int Id; // unique ID of the node + union { // temporary store for user's data + void * pData; + int iData; + float dData; + }; }; // the AIG manager @@ -133,6 +137,10 @@ struct Aig_Man_t_ void (*pImpFunc) (void*, void*); // implication checking precedure void * pImpData; // implication checking data Aig_TMan_t * pManTime; // the timing manager + Vec_Int_t * vPiIds; + Vec_Int_t * vPoIds; + Vec_Ptr_t * vMapped; + Vec_Int_t * vFlopNums; // timing statistics int time1; int time2; @@ -497,6 +505,7 @@ extern void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig ); extern void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ); extern void Aig_ManDump( Aig_Man_t * p ); extern void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ); +extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ); /*=== aigWin.c =========================================================*/ extern void Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit ); diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c index f4a6bf6b..8c53e635 100644 --- a/src/aig/aig/aigCheck.c +++ b/src/aig/aig/aigCheck.c @@ -89,7 +89,8 @@ int Aig_ManCheck( Aig_Man_t * p ) } } // count the total number of nodes - if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) ) + if ( Aig_ManObjNum(p) != 1 + Aig_ManPiNum(p) + Aig_ManPoNum(p) + + Aig_ManBufNum(p) + Aig_ManAndNum(p) + Aig_ManExorNum(p) + Aig_ManLatchNum(p) ) { printf( "Aig_ManCheck: The number of created nodes is wrong.\n" ); printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 9cfaf69c..e9821bdc 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -270,22 +270,22 @@ int Aig_ManCountLevels( Aig_Man_t * p ) Aig_Obj_t * pObj; int i, LevelsMax, Level0, Level1; // initialize the levels - Aig_ManConst1(p)->pData = NULL; + Aig_ManConst1(p)->iData = 0; Aig_ManForEachPi( p, pObj, i ) - pObj->pData = NULL; + pObj->iData = 0; // compute levels in a DFS order vNodes = Aig_ManDfs( p ); Vec_PtrForEachEntry( vNodes, pObj, i ) { - Level0 = (int)Aig_ObjFanin0(pObj)->pData; - Level1 = (int)Aig_ObjFanin1(pObj)->pData; - pObj->pData = (void *)(1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1)); + Level0 = Aig_ObjFanin0(pObj)->iData; + Level1 = Aig_ObjFanin1(pObj)->iData; + pObj->iData = 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Level0, Level1); } Vec_PtrFree( vNodes ); // get levels of the POs LevelsMax = 0; Aig_ManForEachPo( p, pObj, i ) - LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->pData ); + LevelsMax = AIG_MAX( LevelsMax, Aig_ObjFanin0(pObj)->iData ); return LevelsMax; } diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 1e0ee278..d2714380 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -139,6 +139,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -226,6 +228,8 @@ void Aig_ManStop( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; + if ( p->vMapped ) + Vec_PtrFree( p->vMapped ); // print time if ( p->time1 ) { PRT( "time1", p->time1 ); } if ( p->time2 ) { PRT( "time2", p->time2 ); } @@ -246,6 +250,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vBufs ) Vec_PtrFree( p->vBufs ); if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); + if ( p->vFlopNums) Vec_IntFree( p->vFlopNums ); FREE( p->pName ); FREE( p->pObjCopies ); FREE( p->pReprs ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 4c879ee8..65e35fc4 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -890,7 +890,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) // start the total fraiged AIG pAigTotal = Aig_ManStartFrom( pAig ); - Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) ); + Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) + 10000 ); vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) ); // set the PI numbers @@ -932,7 +932,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) Aig_ManForEachObj( pAigPart, pObj, k ) ppData[k] = pObj->pData; // report the process - printf( "Fraiging part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", + printf( "Part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) ); // compute equivalence classes (to be stored in pNew->pReprs) diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index 787ede49..6356afd3 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -270,6 +270,8 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered ) pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // map the const and primary inputs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index 2f00a7eb..abd424c1 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -50,6 +50,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -152,6 +154,20 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) // if some latches are removed, update PIs/POs if ( Vec_PtrSize(vNodes) < Aig_ManPoNum(p) ) { + if ( p->vFlopNums ) + { + int nTruePos = Aig_ManPoNum(p)-Aig_ManRegNum(p); + // remember numbers of flops in the flops + Aig_ManForEachLiSeq( p, pObj, i ) + pObj->pNext = (void *)Vec_IntEntry( p->vFlopNums, i - nTruePos ); + // reset the flop numbers + Vec_PtrForEachEntryStart( vNodes, pObj, i, nTruePos ) + Vec_IntWriteEntry( p->vFlopNums, i - nTruePos, (int)pObj->pNext ); + Vec_IntShrink( p->vFlopNums, Vec_PtrSize(vNodes) - nTruePos ); + // clean the next pointer + Aig_ManForEachLiSeq( p, pObj, i ) + pObj->pNext = NULL; + } // collect new CIs/COs vCis = Vec_PtrAlloc( Aig_ManPiNum(p) ); Aig_ManForEachPi( p, pObj, i ) @@ -184,6 +200,7 @@ int Aig_ManSeqCleanup( Aig_Man_t * p ) Vec_PtrFree( p->vPos ); p->vPos = vCos; p->nObjs[AIG_OBJ_PI] = Vec_PtrSize( p->vPis ); p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos ); + } Vec_PtrFree( vNodes ); // remove dangling nodes diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 86cd02ce..2fba3cb1 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -672,13 +672,13 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) // collect nodes in the DFS order vNodes = Aig_ManDfs( p ); // assign IDs to objects - Aig_ManConst1(p)->pData = (void *)Counter++; + Aig_ManConst1(p)->iData = Counter++; Aig_ManForEachPi( p, pObj, i ) - pObj->pData = (void *)Counter++; + pObj->iData = Counter++; Aig_ManForEachPo( p, pObj, i ) - pObj->pData = (void *)Counter++; + pObj->iData = Counter++; Vec_PtrForEachEntry( vNodes, pObj, i ) - pObj->pData = (void *)Counter++; + pObj->iData = Counter++; nDigits = Aig_Base10Log( Counter ); // write the file pFile = fopen( pFileName, "w" ); @@ -688,51 +688,157 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) // write PIs fprintf( pFile, ".inputs" ); Aig_ManForEachPiSeq( p, pObj, i ) - fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData ); + fprintf( pFile, " n%0*d", nDigits, pObj->iData ); fprintf( pFile, "\n" ); // write POs fprintf( pFile, ".outputs" ); Aig_ManForEachPoSeq( p, pObj, i ) - fprintf( pFile, " n%0*d", nDigits, (int)pObj->pData ); + fprintf( pFile, " n%0*d", nDigits, pObj->iData ); fprintf( pFile, "\n" ); // write latches if ( Aig_ManRegNum(p) ) { fprintf( pFile, "\n" ); Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) - fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, (int)pObjLi->pData, nDigits, (int)pObjLo->pData ); + fprintf( pFile, ".latch n%0*d n%0*d 0\n", nDigits, pObjLi->iData, nDigits, pObjLo->iData ); fprintf( pFile, "\n" ); } // write nodes Vec_PtrForEachEntry( vNodes, pObj, i ) { fprintf( pFile, ".names n%0*d n%0*d n%0*d\n", - nDigits, (int)Aig_ObjFanin0(pObj)->pData, - nDigits, (int)Aig_ObjFanin1(pObj)->pData, - nDigits, (int)pObj->pData ); + nDigits, Aig_ObjFanin0(pObj)->iData, + nDigits, Aig_ObjFanin1(pObj)->iData, + nDigits, pObj->iData ); fprintf( pFile, "%d%d 1\n", !Aig_ObjFaninC0(pObj), !Aig_ObjFaninC1(pObj) ); } // write POs Aig_ManForEachPo( p, pObj, i ) { - if ( (int)pObj->pData == 1359 ) - { - int x = 0; - } fprintf( pFile, ".names n%0*d n%0*d\n", - nDigits, (int)Aig_ObjFanin0(pObj)->pData, - nDigits, (int)pObj->pData ); + nDigits, Aig_ObjFanin0(pObj)->iData, + nDigits, pObj->iData ); fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) ); if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) pConst1 = Aig_ManConst1(p); } if ( pConst1 ) - fprintf( pFile, ".names n%0*d\n 1\n", nDigits, (int)pConst1->pData ); + fprintf( pFile, ".names n%0*d\n 1\n", nDigits, pConst1->iData ); fprintf( pFile, ".end\n\n" ); fclose( pFile ); Vec_PtrFree( vNodes ); } +/**Function************************************************************* + + Synopsis [Writes the AIG into the BLIF file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName ) +{ + FILE * pFile; + Vec_Ptr_t * vNodes; + Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pConst1 = NULL; + int i, nDigits, Counter = 0; + if ( Aig_ManPoNum(p) == 0 ) + { + printf( "Aig_ManDumpBlif(): AIG manager does not have POs.\n" ); + return; + } + // collect nodes in the DFS order + vNodes = Aig_ManDfs( p ); + // assign IDs to objects + Aig_ManConst1(p)->iData = Counter++; + Aig_ManForEachPi( p, pObj, i ) + pObj->iData = Counter++; + Aig_ManForEachPo( p, pObj, i ) + pObj->iData = Counter++; + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->iData = Counter++; + nDigits = Aig_Base10Log( Counter ); + // write the file + pFile = fopen( pFileName, "w" ); + fprintf( pFile, "// Verilog file written by procedure Aig_ManDumpVerilog() in ABC\n" ); + fprintf( pFile, "// http://www.eecs.berkeley.edu/~alanmi/abc/\n" ); + fprintf( pFile, "module %s ( clock", p->pName? p->pName: "test" ); + Aig_ManForEachPiSeq( p, pObj, i ) + fprintf( pFile, ", n%0*d", nDigits, pObj->iData ); + Aig_ManForEachPoSeq( p, pObj, i ) + fprintf( pFile, ", n%0*d", nDigits, pObj->iData ); + fprintf( pFile, " );\n" ); + + // write PIs + Aig_ManForEachPiSeq( p, pObj, i ) + fprintf( pFile, "input n%0*d;\n", nDigits, pObj->iData ); + // write POs + Aig_ManForEachPoSeq( p, pObj, i ) + fprintf( pFile, "output n%0*d;\n", nDigits, pObj->iData ); + // write latches + if ( Aig_ManRegNum(p) ) + { + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + fprintf( pFile, "reg n%0*d;\n", nDigits, pObjLo->iData ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + fprintf( pFile, "wire n%0*d;\n", nDigits, pObjLi->iData ); + } + // write nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + fprintf( pFile, "wire n%0*d;\n", nDigits, pObj->iData ); + // write nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + fprintf( pFile, "assign n%0*d = %sn%0*d & %sn%0*d;\n", + nDigits, pObj->iData, + !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData, + !Aig_ObjFaninC1(pObj) ? " " : "~", nDigits, Aig_ObjFanin1(pObj)->iData + ); + } + // write POs + Aig_ManForEachPoSeq( p, pObj, i ) + { + fprintf( pFile, "assign n%0*d = %sn%0*d;\n", + nDigits, pObj->iData, + !Aig_ObjFaninC0(pObj) ? " " : "~", nDigits, Aig_ObjFanin0(pObj)->iData ); + if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) ) + pConst1 = Aig_ManConst1(p); + } + if ( Aig_ManRegNum(p) ) + { + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + { + fprintf( pFile, "assign n%0*d = %sn%0*d;\n", + nDigits, pObjLi->iData, + !Aig_ObjFaninC0(pObjLi) ? " " : "~", nDigits, Aig_ObjFanin0(pObjLi)->iData ); + if ( Aig_ObjIsConst1(Aig_ObjFanin0(pObjLi)) ) + pConst1 = Aig_ManConst1(p); + } + } + if ( pConst1 ) + fprintf( pFile, "assign n%0*d = 1\'b1;\n", nDigits, pConst1->iData ); + + // write initial state + if ( Aig_ManRegNum(p) ) + { + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + fprintf( pFile, "always @ (posedge clock) begin n%0*d <= n%0*d; end\n", + nDigits, pObjLo->iData, + nDigits, pObjLi->iData ); + Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) + fprintf( pFile, "initial begin n%0*d <= 1\'b0; end\n", + nDigits, pObjLo->iData ); + } + + fprintf( pFile, "endmodule\n\n" ); + fclose( pFile ); + Vec_PtrFree( vNodes ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/module.make b/src/aig/aig/module.make index d1b1cd3b..c35e7121 100644 --- a/src/aig/aig/module.make +++ b/src/aig/aig/module.make @@ -13,6 +13,7 @@ SRC += src/aig/aig/aigCheck.c \ src/aig/aig/aigScl.c \ src/aig/aig/aigSeq.c \ src/aig/aig/aigTable.c \ + src/aig/aig/aigTime.c \ src/aig/aig/aigTiming.c \ src/aig/aig/aigTruth.c \ src/aig/aig/aigTsim.c \ diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index d4266103..989535f2 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -57,6 +57,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; + if ( p->vFlopNums ) + pNew->vFlopNums = Vec_IntDup( p->vFlopNums ); // map the PI nodes Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index a5435862..142c7721 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -463,7 +463,7 @@ int Dar_ObjCutLevelAchieved( Vec_Ptr_t * vCut, int nLevelMin ) ***********************************************************************/ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) { - ProgressBar * pProgress; + Bar_Progress_t * pProgress; Ref_Man_t * p; Vec_Ptr_t * vCut, * vCut2; Aig_Obj_t * pObj, * pObjNew; @@ -485,10 +485,10 @@ int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ) vCut2 = Vec_VecEntry( p->vCuts, 1 ); p->nNodesInit = Aig_ManNodeNum(pAig); nNodesOld = Vec_PtrSize( pAig->vObjs ); - pProgress = Extra_ProgressBarStart( stdout, nNodesOld ); + pProgress = Bar_ProgressStart( stdout, nNodesOld ); Aig_ManForEachObj( pAig, pObj, i ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); + Bar_ProgressUpdate( pProgress, i, NULL ); if ( !Aig_ObjIsNode(pObj) ) continue; if ( i > nNodesOld ) @@ -564,7 +564,7 @@ p->timeEval += clock() - clk; p->timeTotal = clock() - clkStart; p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; - Extra_ProgressBarStop( pProgress ); + Bar_ProgressStop( pProgress ); // put the nodes into the DFS order and reassign their IDs // Aig_NtkReassignIds( p ); // fix the levels diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 98025280..f45e8af0 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -147,6 +147,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) ); // add timeframes +// pManFraig->fAddStrash = 1; for ( f = 0; f < p->nFramesAll - 1; f++ ) { // set the constraints on the latch outputs @@ -163,6 +164,7 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k ) Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) ); } +// pManFraig->fAddStrash = 0; // mark the asserts pManFraig->nAsserts = Aig_ManPoNum(pManFraig); // add the POs for the latch outputs of the last frame @@ -348,7 +350,9 @@ PRT( "Time", clock() - clk ); // mark the classes as non-refined p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes +clk2 = clock(); p->pManFraig = Fra_FramesWithClasses( p ); +p->timeTrav += clock() - clk2; //Aig_ManDumpBlif( p->pManFraig, "testaig.blif" ); // perform AIG rewriting @@ -406,6 +410,9 @@ PRT( "Time", clock() - clk ); p->nSatCallsRecent = 0; p->nSatCallsSkipped = 0; Fra_FraigSweep( p ); + +// Sat_SolverPrintStats( stdout, p->pSat ); + // remove FRAIG and SAT solver Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; sat_solver_delete( p->pSat ); p->pSat = NULL; @@ -425,7 +432,7 @@ PRT( "Time", clock() - clk ); } } /* - // check implications using simulation + // verify implications using simulation if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) { int Temp, clk = clock(); diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 0919e035..f9bbfe44 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -169,7 +169,7 @@ PRT( "Time", clock() - clk ); // perform fraiging clk = clock(); - pNew = Fra_FraigEquivence( pTemp = pNew, 1000 ); + pNew = Fra_FraigEquivence( pTemp = pNew, 100 ); Aig_ManStop( pTemp ); if ( fVerbose ) { @@ -199,13 +199,14 @@ PRT( "Time", clock() - clk ); clk = clock(); pNew = Aig_ManDup( pTemp = pNew, 1 ); Aig_ManStop( pTemp ); - pNew = Dar_ManRewriteDefault( pTemp = pNew ); + pNew = Dar_ManRewriteDefault( pNew ); if ( fVerbose ) { printf( "Rewriting: Latches = %5d. Nodes = %6d. ", Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + // perform retiming clk = clock(); pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); @@ -218,6 +219,7 @@ clk = clock(); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + if ( pNew->nRegs ) pNew = Aig_ManConstReduce( pNew, 0 ); diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index d379cf53..b77c775a 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -432,12 +432,11 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat ) // assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) ); // flip one bit of the last frame - if ( fUseDist1 && p->nFrames == 2 ) + if ( fUseDist1 ) //&& p->nFrames == 2 ) { Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 ); for ( i = 0; i < Limit; i++ ) - Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 ); -// Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 ); + Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 ); } } } diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index c5815a2c..e8e916cc 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -67,11 +67,11 @@ struct Hop_Obj_t_ // 6 words Hop_Obj_t * pNext; // strashing table Hop_Obj_t * pFanin0; // fanin Hop_Obj_t * pFanin1; // fanin - unsigned long Type : 3; // object type - unsigned long fPhase : 1; // value under 000...0 pattern - unsigned long fMarkA : 1; // multipurpose mask - unsigned long fMarkB : 1; // multipurpose mask - unsigned long nRefs : 26; // reference count (level) + unsigned int Type : 3; // object type + unsigned int fPhase : 1; // value under 000...0 pattern + unsigned int fMarkA : 1; // multipurpose mask + unsigned int fMarkB : 1; // multipurpose mask + unsigned int nRefs : 26; // reference count (level) int Id; // unique ID of the node }; diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c index 74462bbd..a6c23fd4 100644 --- a/src/aig/ioa/ioaWriteAig.c +++ b/src/aig/ioa/ioaWriteAig.c @@ -249,7 +249,8 @@ void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) */ // write the comment fprintf( pFile, "c\n" ); - fprintf( pFile, "%s\n", pMan->pName ); + if ( pMan->pName ) + fprintf( pFile, ".model %s\n", pMan->pName ); fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() ); fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); fclose( pFile ); diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c index 81ed895e..1ab91dd2 100644 --- a/src/aig/ivy/ivyFraig.c +++ b/src/aig/ivy/ivyFraig.c @@ -2101,8 +2101,8 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); // var 0 is reserved for const1 node - add the clause - pLits[0] = toLit( 0 ); - sat_solver_addclause( p->pSat, pLits, pLits + 1 ); +// pLits[0] = toLit( 0 ); +// sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them @@ -2235,8 +2235,8 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew ) p->nSatVars = 1; sat_solver_setnvars( p->pSat, 1000 ); // var 0 is reserved for const1 node - add the clause - pLits[0] = toLit( 0 ); - sat_solver_addclause( p->pSat, pLits, pLits + 1 ); +// pLits[0] = toLit( 0 ); +// sat_solver_addclause( p->pSat, pLits, pLits + 1 ); } // if the nodes do not have SAT variables, allocate them diff --git a/src/aig/kit/kitAig.c b/src/aig/kit/kitAig.c new file mode 100644 index 00000000..0d5c1686 --- /dev/null +++ b/src/aig/kit/kitAig.c @@ -0,0 +1,121 @@ +/**CFile**************************************************************** + + FileName [kitAig.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Computation kit.] + + Synopsis [Procedures involving AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Dec 6, 2006.] + + Revision [$Id: kitAig.c,v 1.00 2006/12/06 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "kit.h" +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Kit_GraphToAigInternal( Aig_Man_t * pMan, Kit_Graph_t * pGraph ) +{ + Kit_Node_t * pNode; + Aig_Obj_t * pAnd0, * pAnd1; + int i; + // check for constant function + if ( Kit_GraphIsConst(pGraph) ) + return Aig_NotCond( Aig_ManConst1(pMan), Kit_GraphIsComplement(pGraph) ); + // check for a literal + if ( Kit_GraphIsVar(pGraph) ) + return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) ); + // build the AIG nodes corresponding to the AND gates of the graph + Kit_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + pNode->pFunc = Aig_And( pMan, pAnd0, pAnd1 ); + } + // complement the result if necessary + return Aig_NotCond( pNode->pFunc, Kit_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Kit_GraphToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, Kit_Graph_t * pGraph ) +{ + Kit_Node_t * pNode; + int i; + // collect the fanins + Kit_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = pFanins[i]; + // perform strashing + return Kit_GraphToAigInternal( pMan, pGraph ); +} + +/**Function************************************************************* + + Synopsis [Strashed onen logic nodes using its truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Obj_t * Kit_TruthToAig( Aig_Man_t * pMan, Aig_Obj_t ** pFanins, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ) +{ + Aig_Obj_t * pObj; + Kit_Graph_t * pGraph; + // transform truth table into the decomposition tree + if ( vMemory == NULL ) + { + vMemory = Vec_IntAlloc( 0 ); + pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory ); + Vec_IntFree( vMemory ); + } + else + pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory ); + // derive the AIG for the decomposition tree + pObj = Kit_GraphToAig( pMan, pFanins, pGraph ); + Kit_GraphFree( pGraph ); + return pObj; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c index abd07e68..e24a9964 100644 --- a/src/aig/kit/kitDsd.c +++ b/src/aig/kit/kitDsd.c @@ -2058,7 +2058,7 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize ) // recompute the truth table p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) ); pTruthC = Kit_DsdTruthCompute( p, pNtk ); - if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) + if ( !Kit_TruthIsEqual( pTruth, pTruthC, nVars ) ) printf( "Verification failed.\n" ); Kit_DsdManFree( p ); diff --git a/src/aig/kit/kitIsop.c b/src/aig/kit/kitIsop.c index cc61a6bd..42fae2ea 100644 --- a/src/aig/kit/kitIsop.c +++ b/src/aig/kit/kitIsop.c @@ -58,7 +58,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB assert( nVars >= 0 && nVars < 16 ); // if nVars < 5, make sure it does not depend on those vars // for ( i = nVars; i < 5; i++ ) -// assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); +// assert( !Kit_TruthVarInSupport(puTruth, 5, i) ); // prepare memory manager Vec_IntClear( vMemory ); Vec_IntGrow( vMemory, KIT_ISOP_MEM_LIMIT ); @@ -69,7 +69,7 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB vMemory->nSize = -1; return -1; } - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); + assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) ); if ( pcRes->nCubes == 0 || (pcRes->nCubes == 1 && pcRes->pCubes[0] == 0) ) { vMemory->pArray[0] = 0; @@ -79,18 +79,18 @@ int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryB if ( fTryBoth ) { // compute ISOP for the complemented polarity - Extra_TruthNot( puTruth, puTruth, nVars ); + Kit_TruthNot( puTruth, puTruth, nVars ); pResult = Kit_TruthIsop_rec( puTruth, puTruth, nVars, pcRes2, vMemory ); if ( pcRes2->nCubes >= 0 ) { - assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); + assert( Kit_TruthIsEqual( puTruth, pResult, nVars ) ); if ( pcRes->nCubes > pcRes2->nCubes ) { RetValue = 1; pcRes = pcRes2; } } - Extra_TruthNot( puTruth, puTruth, nVars ); + Kit_TruthNot( puTruth, puTruth, nVars ); } // printf( "%d ", vMemory->nSize ); // move the cover representation to the beginning of the memory buffer @@ -117,9 +117,9 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit unsigned * puRes0, * puRes1, * puRes2; unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1; int i, k, Var, nWords, nWordsAll; -// assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) ); +// assert( Kit_TruthIsImply( puOn, puOnDc, nVars ) ); // allocate room for the resulting truth table - nWordsAll = Extra_TruthWordNum( nVars ); + nWordsAll = Kit_TruthWordNum( nVars ); pTemp = Vec_IntFetch( vStore, nWordsAll ); if ( pTemp == NULL ) { @@ -127,14 +127,14 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit return NULL; } // check for constants - if ( Extra_TruthIsConst0( puOn, nVars ) ) + if ( Kit_TruthIsConst0( puOn, nVars ) ) { pcRes->nCubes = 0; pcRes->pCubes = NULL; - Extra_TruthClear( pTemp, nVars ); + Kit_TruthClear( pTemp, nVars ); return pTemp; } - if ( Extra_TruthIsConst1( puOnDc, nVars ) ) + if ( Kit_TruthIsConst1( puOnDc, nVars ) ) { pcRes->nCubes = 1; pcRes->pCubes = Vec_IntFetch( vStore, 1 ); @@ -144,14 +144,14 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit return NULL; } pcRes->pCubes[0] = 0; - Extra_TruthFill( pTemp, nVars ); + Kit_TruthFill( pTemp, nVars ); return pTemp; } assert( nVars > 0 ); // find the topmost var for ( Var = nVars-1; Var >= 0; Var-- ) - if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || - Extra_TruthVarInSupport( puOnDc, nVars, Var ) ) + if ( Kit_TruthVarInSupport( puOn, nVars, Var ) || + Kit_TruthVarInSupport( puOnDc, nVars, Var ) ) break; assert( Var >= 0 ); // consider a simple case when one-word computation can be used @@ -163,30 +163,30 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit return pTemp; } assert( Var >= 5 ); - nWords = Extra_TruthWordNum( Var ); + nWords = Kit_TruthWordNum( Var ); // cofactor puOn0 = puOn; puOn1 = puOn + nWords; puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords; pTemp0 = pTemp; pTemp1 = pTemp + nWords; // solve for cofactors - Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var ); + Kit_TruthSharp( pTemp0, puOn0, puOnDc1, Var ); puRes0 = Kit_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0, vStore ); if ( pcRes0->nCubes == -1 ) { pcRes->nCubes = -1; return NULL; } - Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var ); + Kit_TruthSharp( pTemp1, puOn1, puOnDc0, Var ); puRes1 = Kit_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1, vStore ); if ( pcRes1->nCubes == -1 ) { pcRes->nCubes = -1; return NULL; } - Extra_TruthSharp( pTemp0, puOn0, puRes0, Var ); - Extra_TruthSharp( pTemp1, puOn1, puRes1, Var ); - Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var ); - Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var ); + Kit_TruthSharp( pTemp0, puOn0, puRes0, Var ); + Kit_TruthSharp( pTemp1, puOn1, puRes1, Var ); + Kit_TruthOr( pTemp0, pTemp0, pTemp1, Var ); + Kit_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var ); puRes2 = Kit_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2, vStore ); if ( pcRes2->nCubes == -1 ) { @@ -210,16 +210,16 @@ unsigned * Kit_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Kit pcRes->pCubes[k++] = pcRes2->pCubes[i]; assert( k == pcRes->nCubes ); // create the resulting truth table - Extra_TruthOr( pTemp0, puRes0, puRes2, Var ); - Extra_TruthOr( pTemp1, puRes1, puRes2, Var ); + Kit_TruthOr( pTemp0, puRes0, puRes2, Var ); + Kit_TruthOr( pTemp1, puRes1, puRes2, Var ); // copy the table if needed nWords <<= 1; for ( i = 1; i < nWordsAll/nWords; i++ ) for ( k = 0; k < nWords; k++ ) pTemp[i*nWords + k] = pTemp[k]; // verify in the end -// assert( Extra_TruthIsImply( puOn, pTemp, nVars ) ); -// assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) ); +// assert( Kit_TruthIsImply( puOn, pTemp, nVars ) ); +// assert( Kit_TruthIsImply( pTemp, puOnDc, nVars ) ); return pTemp; } @@ -264,17 +264,17 @@ unsigned Kit_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Kit_Sop_t assert( nVars > 0 ); // find the topmost var for ( Var = nVars-1; Var >= 0; Var-- ) - if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || - Extra_TruthVarInSupport( &uOnDc, 5, Var ) ) + if ( Kit_TruthVarInSupport( &uOn, 5, Var ) || + Kit_TruthVarInSupport( &uOnDc, 5, Var ) ) break; assert( Var >= 0 ); // cofactor uOn0 = uOn1 = uOn; uOnDc0 = uOnDc1 = uOnDc; - Extra_TruthCofactor0( &uOn0, Var + 1, Var ); - Extra_TruthCofactor1( &uOn1, Var + 1, Var ); - Extra_TruthCofactor0( &uOnDc0, Var + 1, Var ); - Extra_TruthCofactor1( &uOnDc1, Var + 1, Var ); + Kit_TruthCofactor0( &uOn0, Var + 1, Var ); + Kit_TruthCofactor1( &uOn1, Var + 1, Var ); + Kit_TruthCofactor0( &uOnDc0, Var + 1, Var ); + Kit_TruthCofactor1( &uOnDc1, Var + 1, Var ); // solve for cofactors uRes0 = Kit_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0, vStore ); if ( pcRes0->nCubes == -1 ) diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c index 65389ef9..5360ad7f 100644 --- a/src/aig/kit/kitTruth.c +++ b/src/aig/kit/kitTruth.c @@ -1634,6 +1634,33 @@ int Kit_TruthCountMinterms( unsigned * pTruth, int nVars, int * pRes, int * pByt /**Function************************************************************* + Synopsis [Prints the hex unsigned into a file.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Kit_PrintHexadecimal( FILE * pFile, unsigned Sign[], int nVars ) +{ + int nDigits, Digit, k; + // write the number into the file + nDigits = (1 << nVars) / 4; + for ( k = nDigits - 1; k >= 0; k-- ) + { + Digit = ((Sign[k/8] >> ((k%8) * 4)) & 15); + if ( Digit < 10 ) + fprintf( pFile, "%d", Digit ); + else + fprintf( pFile, "%c", 'a' + Digit-10 ); + } +// fprintf( pFile, "\n" ); +} + +/**Function************************************************************* + Synopsis [Fast counting minterms for the functions.] Description [Returns 0 if the function is a constant.] @@ -1665,7 +1692,7 @@ void Kit_TruthCountMintermsPrecomp() uWord |= (bit_count[i & 0x33] << 16); uWord |= (bit_count[i & 0x0f] << 24); printf( "0x" ); - Extra_PrintHexadecimal( stdout, &uWord, 5 ); + Kit_PrintHexadecimal( stdout, &uWord, 5 ); printf( ", " ); } } diff --git a/src/aig/kit/module.make b/src/aig/kit/module.make index 25c8e767..ea62381b 100644 --- a/src/aig/kit/module.make +++ b/src/aig/kit/module.make @@ -1,4 +1,5 @@ -SRC += src/aig/kit/kitBdd.c \ +SRC += src/aig/kit/kitAig.c \ + src/aig/kit/kitBdd.c \ src/aig/kit/kitCloud.c src/aig/kit/cloud.c \ src/aig/kit/kitDsd.c \ src/aig/kit/kitFactor.c \ diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index bca3f33a..2e2b379b 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -638,6 +638,8 @@ extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk ); extern int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk ); extern Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk ); extern void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ); +extern Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init ); +extern void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk ); /*=== abcLib.c ==========================================================*/ extern Abc_Lib_t * Abc_LibCreate( char * pName ); extern void Abc_LibFree( Abc_Lib_t * pLib, Abc_Ntk_t * pNtk ); @@ -662,35 +664,6 @@ extern Abc_Ntk_t * Abc_NtkMiterQuantifyPis( Abc_Ntk_t * pNtk ); extern int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ); extern void Abc_NtkMiterReport( Abc_Ntk_t * pMiter ); extern Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ); -/*=== abcObj.c ==========================================================*/ -extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); -extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); -extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); -extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj ); -extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes ); -extern void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj ); -extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName ); -extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName ); -extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode ); -extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ); -extern Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk ); -extern Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); -extern Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); -extern Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); -extern Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); -extern Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); -extern Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 ); -extern bool Abc_NodeIsConst( Abc_Obj_t * pNode ); -extern bool Abc_NodeIsConst0( Abc_Obj_t * pNode ); -extern bool Abc_NodeIsConst1( Abc_Obj_t * pNode ); -extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); -extern bool Abc_NodeIsInv( Abc_Obj_t * pNode ); -extern void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcNames.c ====================================================*/ extern char * Abc_ObjName( Abc_Obj_t * pNode ); extern char * Abc_ObjAssignName( Abc_Obj_t * pObj, char * pName, char * pSuffix ); @@ -737,6 +710,35 @@ extern Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ); extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); extern void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ); extern void Abc_NtkMakeComb( Abc_Ntk_t * pNtk ); +/*=== abcObj.c ==========================================================*/ +extern Abc_Obj_t * Abc_ObjAlloc( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); +extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); +extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); +extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj ); +extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes ); +extern void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj ); +extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName ); +extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName ); +extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode ); +extern Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindNet( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkFindOrCreateNet( Abc_Ntk_t * pNtk, char * pName ); +extern Abc_Obj_t * Abc_NtkCreateNodeConst0( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NtkCreateNodeConst1( Abc_Ntk_t * pNtk ); +extern Abc_Obj_t * Abc_NtkCreateNodeInv( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); +extern Abc_Obj_t * Abc_NtkCreateNodeBuf( Abc_Ntk_t * pNtk, Abc_Obj_t * pFanin ); +extern Abc_Obj_t * Abc_NtkCreateNodeAnd( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); +extern Abc_Obj_t * Abc_NtkCreateNodeOr( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); +extern Abc_Obj_t * Abc_NtkCreateNodeExor( Abc_Ntk_t * pNtk, Vec_Ptr_t * vFanins ); +extern Abc_Obj_t * Abc_NtkCreateNodeMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0 ); +extern bool Abc_NodeIsConst( Abc_Obj_t * pNode ); +extern bool Abc_NodeIsConst0( Abc_Obj_t * pNode ); +extern bool Abc_NodeIsConst1( Abc_Obj_t * pNode ); +extern bool Abc_NodeIsBuf( Abc_Obj_t * pNode ); +extern bool Abc_NodeIsInv( Abc_Obj_t * pNode ); +extern void Abc_NodeComplement( Abc_Obj_t * pNode ); /*=== abcPrint.c ==========================================================*/ extern void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ); extern void Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index cf3ddaba..d96bbfac 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -211,6 +211,113 @@ void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ) pLatch->pData = (void *)(vValues? (Vec_IntEntry(vValues,i)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC); } +/**Function************************************************************* + + Synopsis [Creates latch with the given initial value.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_NtkAddLatch( Abc_Ntk_t * pNtk, Abc_Obj_t * pDriver, Abc_InitType_t Init ) +{ + Abc_Obj_t * pLatchOut, * pLatch, * pLatchIn; + pLatchOut = Abc_NtkCreateBo(pNtk); + pLatch = Abc_NtkCreateLatch(pNtk); + pLatchIn = Abc_NtkCreateBi(pNtk); + Abc_ObjAssignName( pLatchOut, Abc_ObjName(pLatch), "_lo" ); + Abc_ObjAssignName( pLatchIn, Abc_ObjName(pLatch), "_li" ); + Abc_ObjAddFanin( pLatchOut, pLatch ); + Abc_ObjAddFanin( pLatch, pLatchIn ); + Abc_ObjAddFanin( pLatchIn, pDriver ); + pLatch->pData = (void *)Init; + return pLatchOut; +} + +/**Function************************************************************* + + Synopsis [Creates MUX.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkNodeConvertToMux( Abc_Ntk_t * pNtk, Abc_Obj_t * pNodeC, Abc_Obj_t * pNode1, Abc_Obj_t * pNode0, Abc_Obj_t * pMux ) +{ + assert( Abc_NtkIsLogic(pNtk) ); + Abc_ObjAddFanin( pMux, pNodeC ); + Abc_ObjAddFanin( pMux, pNode1 ); + Abc_ObjAddFanin( pMux, pNode0 ); + if ( Abc_NtkHasSop(pNtk) ) + pMux->pData = Abc_SopRegister( pNtk->pManFunc, "11- 1\n0-1 1\n" ); + else if ( Abc_NtkHasBdd(pNtk) ) + pMux->pData = Cudd_bddIte(pNtk->pManFunc,Cudd_bddIthVar(pNtk->pManFunc,0),Cudd_bddIthVar(pNtk->pManFunc,1),Cudd_bddIthVar(pNtk->pManFunc,2)), Cudd_Ref( pMux->pData ); + else if ( Abc_NtkHasAig(pNtk) ) + pMux->pData = Hop_Mux(pNtk->pManFunc,Hop_IthVar(pNtk->pManFunc,0),Hop_IthVar(pNtk->pManFunc,1),Hop_IthVar(pNtk->pManFunc,2)); + else + assert( 0 ); +} + +/**Function************************************************************* + + Synopsis [Converts registers with DC values into additional PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkConvertDcLatches( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pCtrl, * pLatch, * pMux, * pPi; + Abc_InitType_t Init = ABC_INIT_ZERO; + int i, fFound = 0, Counter; + // check if there are latches with DC values + Abc_NtkForEachLatch( pNtk, pLatch, i ) + if ( Abc_LatchIsInitDc(pLatch) ) + { + fFound = 1; + break; + } + if ( !fFound ) + return; + // add control latch + pCtrl = Abc_NtkAddLatch( pNtk, Abc_NtkCreateNodeConst1(pNtk), Init ); + // add fanouts for each latch with DC values + Counter = 0; + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + if ( !Abc_LatchIsInitDc(pLatch) ) + continue; + // change latch value + pLatch->pData = (void *)Init; + // if the latch output has the same name as a PO, rename it + if ( Abc_NodeFindCoFanout( Abc_ObjFanout0(pLatch) ) ) + { + Nm_ManDeleteIdName( pLatch->pNtk->pManName, Abc_ObjFanout0(pLatch)->Id ); + Abc_ObjAssignName( Abc_ObjFanout0(pLatch), Abc_ObjName(pLatch), "_lo" ); + } + // create new PIs + pPi = Abc_NtkCreatePi( pNtk ); + Abc_ObjAssignName( pPi, Abc_ObjName(pLatch), "_pi" ); + // create a new node and transfer fanout from latch output to the new node + pMux = Abc_NtkCreateNode( pNtk ); + Abc_ObjTransferFanout( Abc_ObjFanout0(pLatch), pMux ); + // convert the node into a mux + Abc_NtkNodeConvertToMux( pNtk, pCtrl, Abc_ObjFanout0(pLatch), pPi, pMux ); + Counter++; + } + printf( "The number of converted latches with DC values = %d.\n", Counter ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index bbaa80a4..18fbad38 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -161,6 +161,7 @@ static int Abc_CommandIf ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandScut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandInit ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandZero ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandUndc ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandPipe ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnseq ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -329,6 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 ); Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "zero", Abc_CommandZero, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "undc", Abc_CommandUndc, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); Cmd_CommandAdd( pAbc, "Sequential", "retime", Abc_CommandRetime, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "sfpga", Abc_CommandSeqFpga, 1 ); @@ -6318,12 +6320,18 @@ int Abc_CommandTest( 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; } +*/ + if ( Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for logic circuits.\n" ); + return 0; + } // pNtkRes = Abc_NtkDar( pNtk ); // pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); @@ -10459,6 +10467,69 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandUndc( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "The current network is combinational.\n" ); + return 0; + } + + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "This command works only for logic networks.\n" ); + return 0; + } + + // get the new network + Abc_NtkConvertDcLatches( pNtk ); + return 0; + +usage: + fprintf( pErr, "usage: undc [-h]\n" ); + fprintf( pErr, "\t converts latches with DC init values into free PIs\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 06e425d5..f7616abc 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -85,7 +85,10 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) pMan->pName = Extra_UtilStrsav( pNtk->pName ); // save the number of registers if ( fRegisters ) + { pMan->nRegs = Abc_NtkLatchNum(pNtk); + pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs ); + } // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); Abc_NtkForEachCi( pNtk, pObj, i ) @@ -114,6 +117,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) // remove dangling nodes if ( nNodes = Aig_ManCleanup( pMan ) ) printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes ); +Aig_ManDumpVerilog( pMan, "test.v" ); if ( !Aig_ManCheck( pMan ) ) { printf( "Abc_NtkToDar: AIG check has failed.\n" ); @@ -141,7 +145,7 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_Obj_t * pObjNew; Aig_Obj_t * pObj; int i; - assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); +// assert( Aig_ManRegNum(pMan) == Abc_NtkLatchNum(pNtkOld) ); // perform strashing pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes @@ -192,7 +196,7 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObjNew; + Abc_Obj_t * pObjNew, * pLatch; Aig_Obj_t * pObj, * pObjLo, * pObjLi; int i; // assert( Aig_ManRegNum(pMan) != Abc_NtkLatchNum(pNtkOld) ); @@ -212,7 +216,19 @@ Abc_Ntk_t * Abc_NtkFromDarSeqSweep( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Abc_ObjAddFanin( pObjLo->pData, pObjNew ); Abc_LatchSetInit0( pObjNew ); } - Abc_NtkAddDummyBoxNames( pNtkNew ); + if ( pMan->vFlopNums == NULL ) + Abc_NtkAddDummyBoxNames( pNtkNew ); + else + { + assert( Abc_NtkBoxNum(pNtkOld) == Abc_NtkLatchNum(pNtkOld) ); + Abc_NtkForEachLatch( pNtkNew, pObjNew, i ) + { + pLatch = Abc_NtkBox( pNtkOld, Vec_IntEntry( pMan->vFlopNums, i ) ); + Abc_ObjAssignName( pObjNew, Abc_ObjName(pLatch), NULL ); + Abc_ObjAssignName( Abc_ObjFanin0(pObjNew), Abc_ObjName(Abc_ObjFanin0(pLatch)), NULL ); + Abc_ObjAssignName( Abc_ObjFanout0(pObjNew), Abc_ObjName(Abc_ObjFanout0(pLatch)), NULL ); + } + } // rebuild the AIG vNodes = Aig_ManDfs( pMan ); Vec_PtrForEachEntry( vNodes, pObj, i ) @@ -959,8 +975,8 @@ Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, in // so fraiging does not reduce the number of functions represented by nodes Fraig_ParamsSetDefault( &Params ); Params.nBTLimit = 100000; - pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); -// pNtkFraig = Abc_NtkDup( pNtk ); +// pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 ); + pNtkFraig = Abc_NtkDup( pNtk ); if ( fVerbose ) { PRT( "Initial fraiging time", clock() - clk ); diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index f9b053ba..7c3fb33c 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -314,7 +314,7 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) } else { - if ( Abc_LatchIsInit1(pLatch) == Abc_NodeIsConst1(pLatch) ) + if ( Abc_LatchIsInit1(pLatch) == Abc_NodeIsConst1(Abc_ObjFanin0(Abc_ObjFanin0(pLatch))) ) Counter2++; } } diff --git a/src/base/abci/xaaaa.c b/src/base/abci/xaaaa.c deleted file mode 100644 index ea39ad02..00000000 --- a/src/base/abci/xaaaa.c +++ /dev/null @@ -1,155 +0,0 @@ -/**CFile**************************************************************** - - FileName [abc_.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abc_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" -#include "kit.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkPrintMeasures( unsigned * pTruth, int nVars ) -{ - unsigned uCofs[10][32]; - int i, k, nOnes; - - // total pairs - nOnes = Kit_TruthCountOnes( uCofs[0], nVars ); - printf( "Total = %d.\n", nOnes * ((1 << nVars) - nOnes) ); - - // print measures for individual variables - for ( i = 0; i < nVars; i++ ) - { - Kit_TruthUniqueNew( uCofs[0], pTruth, nVars, i ); - nOnes = Kit_TruthCountOnes( uCofs[0], nVars ); - printf( "%7d ", nOnes ); - } - printf( "\n" ); - - // consider pairs - for ( i = 0; i < nVars; i++ ) - for ( k = 0; k < nVars; k++ ) - { - if ( i == k ) - { - printf( " " ); - continue; - } - Kit_TruthCofactor0New( uCofs[0], pTruth, nVars, i ); - Kit_TruthCofactor1New( uCofs[1], pTruth, nVars, i ); - - Kit_TruthCofactor0New( uCofs[2], uCofs[0], nVars, k ); // 00 - Kit_TruthCofactor1New( uCofs[3], uCofs[0], nVars, k ); // 01 - Kit_TruthCofactor0New( uCofs[4], uCofs[1], nVars, k ); // 10 - Kit_TruthCofactor1New( uCofs[5], uCofs[1], nVars, k ); // 11 - - Kit_TruthAndPhase( uCofs[6], uCofs[2], uCofs[5], nVars, 0, 1 ); // 00 & 11' - Kit_TruthAndPhase( uCofs[7], uCofs[2], uCofs[5], nVars, 1, 0 ); // 00' & 11 - Kit_TruthAndPhase( uCofs[8], uCofs[3], uCofs[4], nVars, 0, 1 ); // 01 & 10' - Kit_TruthAndPhase( uCofs[9], uCofs[3], uCofs[4], nVars, 1, 0 ); // 01' & 10 - - nOnes = Kit_TruthCountOnes( uCofs[6], nVars ) + - Kit_TruthCountOnes( uCofs[7], nVars ) + - Kit_TruthCountOnes( uCofs[8], nVars ) + - Kit_TruthCountOnes( uCofs[9], nVars ); - - printf( "%7d ", nOnes ); - if ( k == nVars - 1 ) - printf( "\n" ); - } - printf( "\n" ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_Ntk4VarTable( Abc_Ntk_t * pNtk ) -{ - static u4VarTts[222] = { - 0x0000, 0x0001, 0x0003, 0x0006, 0x0007, 0x000f, 0x0016, 0x0017, 0x0018, 0x0019, - 0x001b, 0x001e, 0x001f, 0x003c, 0x003d, 0x003f, 0x0069, 0x006b, 0x006f, 0x007e, - 0x007f, 0x00ff, 0x0116, 0x0117, 0x0118, 0x0119, 0x011a, 0x011b, 0x011e, 0x011f, - 0x012c, 0x012d, 0x012f, 0x013c, 0x013d, 0x013e, 0x013f, 0x0168, 0x0169, 0x016a, - 0x016b, 0x016e, 0x016f, 0x017e, 0x017f, 0x0180, 0x0181, 0x0182, 0x0183, 0x0186, - 0x0187, 0x0189, 0x018b, 0x018f, 0x0196, 0x0197, 0x0198, 0x0199, 0x019a, 0x019b, - 0x019e, 0x019f, 0x01a8, 0x01a9, 0x01aa, 0x01ab, 0x01ac, 0x01ad, 0x01ae, 0x01af, - 0x01bc, 0x01bd, 0x01be, 0x01bf, 0x01e8, 0x01e9, 0x01ea, 0x01eb, 0x01ee, 0x01ef, - 0x01fe, 0x033c, 0x033d, 0x033f, 0x0356, 0x0357, 0x0358, 0x0359, 0x035a, 0x035b, - 0x035e, 0x035f, 0x0368, 0x0369, 0x036a, 0x036b, 0x036c, 0x036d, 0x036e, 0x036f, - 0x037c, 0x037d, 0x037e, 0x03c0, 0x03c1, 0x03c3, 0x03c5, 0x03c6, 0x03c7, 0x03cf, - 0x03d4, 0x03d5, 0x03d6, 0x03d7, 0x03d8, 0x03d9, 0x03db, 0x03dc, 0x03dd, 0x03de, - 0x03fc, 0x0660, 0x0661, 0x0662, 0x0663, 0x0666, 0x0667, 0x0669, 0x066b, 0x066f, - 0x0672, 0x0673, 0x0676, 0x0678, 0x0679, 0x067a, 0x067b, 0x067e, 0x0690, 0x0691, - 0x0693, 0x0696, 0x0697, 0x069f, 0x06b0, 0x06b1, 0x06b2, 0x06b3, 0x06b4, 0x06b5, - 0x06b6, 0x06b7, 0x06b9, 0x06bd, 0x06f0, 0x06f1, 0x06f2, 0x06f6, 0x06f9, 0x0776, - 0x0778, 0x0779, 0x077a, 0x077e, 0x07b0, 0x07b1, 0x07b4, 0x07b5, 0x07b6, 0x07bc, - 0x07e0, 0x07e1, 0x07e2, 0x07e3, 0x07e6, 0x07e9, 0x07f0, 0x07f1, 0x07f2, 0x07f8, - 0x0ff0, 0x1668, 0x1669, 0x166a, 0x166b, 0x166e, 0x167e, 0x1681, 0x1683, 0x1686, - 0x1687, 0x1689, 0x168b, 0x168e, 0x1696, 0x1697, 0x1698, 0x1699, 0x169a, 0x169b, - 0x169e, 0x16a9, 0x16ac, 0x16ad, 0x16bc, 0x16e9, 0x177e, 0x178e, 0x1796, 0x1798, - 0x179a, 0x17ac, 0x17e8, 0x18e7, 0x19e1, 0x19e3, 0x19e6, 0x1bd8, 0x1be4, 0x1ee1, - 0x3cc3, 0x6996 - }; - int Counters[222]; - - Vec_Ptr_t * vNodes; - Abc_Obj_t * pObj; - int i; - - // set elementary truth tables - Abc_NtkForEachPi( pNtk, pObj, i ) - pObj - - Abc_NtkForEachPo( pNtk, pObj, i ) - { - vNodes = Abc_NtkDfsNodes( pNtk, &pObj, i ); - Vec_PtrFree( vNodes ); - } -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/base/io/io.c b/src/base/io/io.c index 20caeb57..ca4cab95 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -34,6 +34,7 @@ static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandReadInit ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadPla ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadVerilog ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -86,6 +87,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_eqn", IoCommandReadEqn, 1 ); + Cmd_CommandAdd( pAbc, "I/O", "read_init", IoCommandReadInit, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_pla", IoCommandReadPla, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_truth", IoCommandReadTruth, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_verilog", IoCommandReadVerilog, 1 ); @@ -654,6 +656,65 @@ usage: SeeAlso [] ***********************************************************************/ +int IoCommandReadInit( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + char * pFileName; + int c; + extern void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + // get the input file name + pFileName = argv[globalUtilOptind]; + // read the file using the corresponding file reader + pNtk = Abc_NtkDup( pNtk ); + Io_ReadBenchInit( pNtk, pFileName ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtk ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: read_init [-h] <file>\n" ); + fprintf( pAbc->Err, "\t reads initial state of the network in BENCH format\n" ); + fprintf( pAbc->Err, "\t-h : prints the command summary\n" ); + fprintf( pAbc->Err, "\tfile : the name of a file to read\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk; diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index be80dc82..d3c4c878 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -245,6 +245,21 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) // printf( "Io_ReadAiger(): I/O/register names are not given. Generating short names.\n" ); Abc_NtkShortNames( pNtkNew ); } + + // read the name of the model if given + if ( *pCur == 'c' ) + { + if ( !strncmp( pCur + 2, ".model", 6 ) ) + { + char * pTemp; + for ( pTemp = pCur + 9; *pTemp && *pTemp != '\n'; pTemp++ ); + *pTemp = 0; + free( pNtkNew->pName ); + pNtkNew->pName = Extra_UtilStrsav( pCur + 9 ); + } + } + + // skipping the comments free( pContents ); Vec_PtrFree( vNodes ); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index ba622e40..007147bc 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -66,6 +66,7 @@ Abc_Ntk_t * Io_ReadBench( char * pFileName, int fCheck ) } return pNtk; } + /**Function************************************************************* Synopsis [] @@ -82,7 +83,7 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) ProgressBar * pProgress; Vec_Ptr_t * vTokens; Abc_Ntk_t * pNtk; - Abc_Obj_t * pNode; + Abc_Obj_t * pNode, * pNet; Vec_Str_t * vString; unsigned uTruth[8]; char * pType, ** ppNames, * pString; @@ -241,11 +242,34 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Extra_ProgressBarStop( pProgress ); Vec_StrFree( vString ); - // check if constant have been added -// if ( pNet = Abc_NtkFindNet( pNtk, "vdd" ) ) -// Io_ReadCreateConst( pNtk, "vdd", 1 ); -// if ( pNet = Abc_NtkFindNet( pNtk, "gnd" ) ) -// Io_ReadCreateConst( pNtk, "gnd", 0 ); + // check if constant 0 is present + if ( (pNet = Abc_NtkFindNet( pNtk, "gnd" )) ) + { + if ( Abc_ObjFaninNum(pNet) == 0 ) + Io_ReadCreateConst( pNtk, "gnd", 0 ); + } + if ( (pNet = Abc_NtkFindNet( pNtk, "1" )) ) + { + if ( Abc_ObjFaninNum(pNet) == 0 ) + { + printf( "Io_ReadBenchNetwork(): Adding constant 0 fanin to non-driven net \"1\".\n" ); + Io_ReadCreateConst( pNtk, "1", 0 ); + } + } + // check if constant 1 is present + if ( (pNet = Abc_NtkFindNet( pNtk, "vdd" )) ) + { + if ( Abc_ObjFaninNum(pNet) == 0 ) + Io_ReadCreateConst( pNtk, "vdd", 1 ); + } + if ( (pNet = Abc_NtkFindNet( pNtk, "2" )) ) + { + if ( Abc_ObjFaninNum(pNet) == 0 ) + { + printf( "Io_ReadBenchNetwork(): Adding constant 1 fanin to non-driven net \"2\".\n" ); + Io_ReadCreateConst( pNtk, "2", 1 ); + } + } Abc_NtkFinalizeRead( pNtk ); @@ -269,6 +293,65 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) } +/**Function************************************************************* + + Synopsis [Reads initial state in BENCH format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_ReadBenchInit( Abc_Ntk_t * pNtk, char * pFileName ) +{ + char pBuffer[1000]; + FILE * pFile; + char * pToken; + Abc_Obj_t * pObj; + int Num; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Io_ReadBenchInit(): Failed to open file \"%s\".\n", pFileName ); + return; + } + while ( fgets( pBuffer, 999, pFile ) ) + { + pToken = strtok( pBuffer, " \n\t\r" ); + // find the latch output + Num = Nm_ManFindIdByName( pNtk->pManName, pToken, ABC_OBJ_BO ); + if ( Num < 0 ) + { + printf( "Io_ReadBenchInit(): Cannot find register with output %s.\n", pToken ); + continue; + } + pObj = Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) ); + if ( !Abc_ObjIsLatch(pObj) ) + { + printf( "Io_ReadBenchInit(): The signal is not a register output %s.\n", pToken ); + continue; + } + // assign the new init state + pToken = strtok( NULL, " \n\t\r" ); + if ( pToken[0] == '0' ) + Abc_LatchSetInit0( pObj ); + else if ( pToken[0] == '1' ) + Abc_LatchSetInit1( pObj ); + else if ( pToken[0] == '2' ) + Abc_LatchSetInitDc( pObj ); + else + { + printf( "Io_ReadBenchInit(): The signal %s has unknown initial value (%s).\n", + Abc_ObjName(Abc_ObjFanout0(pObj)), pToken ); + continue; + } + } + fclose( pFile ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index e805fbc2..ff34b177 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -248,7 +248,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) // write the comment fprintf( pFile, "c\n" ); - fprintf( pFile, "%s\n", pNtk->pName ); + if ( pNtk->pName && strlen(pNtk->pName) > 0 ) + fprintf( pFile, ".model %s\n", pNtk->pName ); fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() ); fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); fclose( pFile ); diff --git a/src/misc/st/st.c b/src/misc/st/st.c index c0965a41..872fe51b 100644 --- a/src/misc/st/st.c +++ b/src/misc/st/st.c @@ -31,7 +31,8 @@ #define ST_NUMCMP(x,y) ((x) != (y)) #define ST_NUMHASH(x,size) (ABS((long)x)%(size)) -#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) +//#define ST_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) // 64-bit bug fix 9/17/2007 +#define ST_PTRHASH(x,size) ((int)(((unsigned long)(x)>>2)%size)) #define EQUAL(func, x, y) \ ((((func) == st_numcmp) || ((func) == st_ptrcmp)) ?\ (ST_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0)) diff --git a/src/misc/st/stmm.c b/src/misc/st/stmm.c index 99485c23..8dfacfe4 100644 --- a/src/misc/st/stmm.c +++ b/src/misc/st/stmm.c @@ -17,7 +17,8 @@ #define STMM_NUMCMP(x,y) ((x) != (y)) #define STMM_NUMHASH(x,size) (ABS((long)x)%(size)) -#define STMM_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) +//#define STMM_PTRHASH(x,size) ((int)((unsigned long)(x)>>2)%size) // 64-bit bug fix 9/17/2007 +#define STMM_PTRHASH(x,size) ((int)(((unsigned long)(x)>>2)%size)) #define EQUAL(func, x, y) \ ((((func) == stmm_numcmp) || ((func) == stmm_ptrcmp)) ?\ (STMM_NUMCMP((x),(y)) == 0) : ((*func)((x), (y)) == 0)) diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index 40b46bc5..6a97fcaa 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -27,6 +27,10 @@ extern "C" { #ifdef _WIN32 #define inline __inline // compatible with MS VS 6.0 +#pragma warning(disable : 4152) // warning C4152: nonstandard extension, function/data pointer conversion in expression +#pragma warning(disable : 4244) // warning C4244: '+=' : conversion from 'int ' to 'unsigned short ', possible loss of data +#pragma warning(disable : 4514) // warning C4514: 'Vec_StrPop' : unreferenced inline function has been removed +#pragma warning(disable : 4710) // warning C4710: function 'Vec_PtrGrow' not inlined #endif //////////////////////////////////////////////////////////////////////// @@ -71,6 +75,10 @@ extern "C" { #define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) #endif +#ifndef PRTP +#define PRTP(a,t,T) printf("%s = ", (a)); printf("%6.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0) +#endif + #include "vecInt.h" #include "vecFlt.h" #include "vecStr.h" diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index d1321c62..3afa39af 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -105,6 +105,28 @@ static inline Vec_Int_t * Vec_IntStart( int nSize ) /**Function************************************************************* + Synopsis [Allocates a vector with the given size and cleans it.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Vec_Int_t * Vec_IntStartNatural( int nSize ) +{ + Vec_Int_t * p; + int i; + p = Vec_IntAlloc( nSize ); + p->nSize = nSize; + for ( i = 0; i < nSize; i++ ) + p->pArray[i] = i; + return p; +} + +/**Function************************************************************* + Synopsis [Creates the vector from an integer array of the given size.] Description [] diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index 6ea975aa..8b8028e3 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -507,6 +507,9 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) int i, Iter, nNodes, nNodesPrev, clk = clock(); assert( Abc_NtkIsLogic(pNtk) ); + // sweep dangling nodes as a preprocessing step + Abc_NtkSweep( pNtk, 0 ); + // get the number of inputs pPars->nLutSize = Abc_NtkGetFaninMax( pNtk ); // adjust the number of crossbars based on LUT size diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 512c5751..439d9e76 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -90,9 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[ //================================================================================================= // Encode literals in clause pointers: -static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } -static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } -static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } +static inline clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } +static inline bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } +static inline lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } //================================================================================================= // Simple helpers: @@ -148,7 +148,7 @@ static inline void order_unassigned(sat_solver* s, int v) // undoorder } } -static int order_select(sat_solver* s, float random_var_freq) // selectvar +static inline int order_select(sat_solver* s, float random_var_freq) // selectvar { int* heap; double* activity; @@ -442,7 +442,7 @@ static inline void assume(sat_solver* s, lit l){ } -static inline void sat_solver_canceluntil(sat_solver* s, int level) { +static void sat_solver_canceluntil(sat_solver* s, int level) { lit* trail; lbool* values; clause** reasons; @@ -723,13 +723,14 @@ clause* sat_solver_propagate(sat_solver* s) //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); for (i = j = begin; i < end; ){ if (clause_is_lit(*i)){ +// s->stats.inspects2++; *j++ = *i; if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ confl = s->binary; (clause_begin(confl))[1] = lit_neg(p); (clause_begin(confl))[0] = clause_read_lit(*i++); - // Copy the remaining watches: +// s->stats.inspects2 += end - i; while (i < end) *j++ = *i++; } @@ -770,6 +771,7 @@ clause* sat_solver_propagate(sat_solver* s) if (!enqueue(s,lits[0], *i)){ confl = *i++; // Copy the remaining watches: +// s->stats.inspects2 += end - i; while (i < end) *j++ = *i++; } @@ -1154,6 +1156,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin lit* i; // set the external limits + s->nCalls++; s->nRestarts = 0; s->nConfLimit = 0; s->nInsLimit = 0; @@ -1175,12 +1178,13 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin assume(s, *i); if (sat_solver_propagate(s) == NULL) break; - // falltrough + // fallthrough case -1: /* l_False */ sat_solver_canceluntil(s, 0); return l_False; } } + s->nCalls2++; s->root_level = sat_solver_dlevel(s); diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h index f5424c85..542b9895 100644 --- a/src/sat/bsat/satSolver.h +++ b/src/sat/bsat/satSolver.h @@ -172,6 +172,8 @@ struct sat_solver_t veci act_vars; // variables whose activity has changed double* factors; // the activity factors int nRestarts; // the number of local restarts + int nCalls; // the number of local restarts + int nCalls2; // the number of local restarts Sat_MmStep_t * pMem; diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c index 3001957f..62f3c208 100644 --- a/src/sat/bsat/satUtil.c +++ b/src/sat/bsat/satUtil.c @@ -146,11 +146,13 @@ void Sat_SolverClauseWriteDimacs( FILE * pFile, clause * pC, bool fIncrement ) ***********************************************************************/ void Sat_SolverPrintStats( FILE * pFile, sat_solver * p ) { - printf( "starts : %d\n", (int)p->stats.starts ); - printf( "conflicts : %d\n", (int)p->stats.conflicts ); - printf( "decisions : %d\n", (int)p->stats.decisions ); - printf( "propagations : %d\n", (int)p->stats.propagations ); - printf( "inspects : %d\n", (int)p->stats.inspects ); +// printf( "calls : %8d (%d)\n", (int)p->nCalls, (int)p->nCalls2 ); + printf( "starts : %8d\n", (int)p->stats.starts ); + printf( "conflicts : %8d\n", (int)p->stats.conflicts ); + printf( "decisions : %8d\n", (int)p->stats.decisions ); + printf( "propagations : %8d\n", (int)p->stats.propagations ); + printf( "inspects : %8d\n", (int)p->stats.inspects ); +// printf( "inspects2 : %8d\n", (int)p->stats.inspects2 ); } /**Function************************************************************* |