diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-31 08:01:00 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-07-31 08:01:00 -0700 |
commit | 29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0 (patch) | |
tree | cd06159f7ddf9e75fc8dff354a7ef5c593b56856 | |
parent | fefd8b901d89ad0d977db8896c12123cc747e3d7 (diff) | |
download | abc-29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0.tar.gz abc-29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0.tar.bz2 abc-29c9b0c0c4c66cb09b7c00c5c7290141be2af6a0.zip |
Version abc70731
-rw-r--r-- | src/aig/aig/aig.h | 11 | ||||
-rw-r--r-- | src/aig/aig/aigCheck.c | 41 | ||||
-rw-r--r-- | src/aig/aig/aigMan.c | 11 | ||||
-rw-r--r-- | src/aig/aig/aigObj.c | 3 | ||||
-rw-r--r-- | src/aig/aig/aigRepr.c | 1 | ||||
-rw-r--r-- | src/aig/aig/aigTable.c | 2 | ||||
-rw-r--r-- | src/aig/aig/aigUtil.c | 42 | ||||
-rw-r--r-- | src/aig/cnf/cnfCore.c | 2 | ||||
-rw-r--r-- | src/aig/dar/dar.h | 1 | ||||
-rw-r--r-- | src/aig/dar/darBalance.c | 2 | ||||
-rw-r--r-- | src/aig/dar/darCore.c | 14 | ||||
-rw-r--r-- | src/aig/dar/darRefact.c | 16 | ||||
-rw-r--r-- | src/aig/dar/darScript.c | 24 | ||||
-rw-r--r-- | src/aig/fra/fra.h | 18 | ||||
-rw-r--r-- | src/aig/fra/fraClass.c | 25 | ||||
-rw-r--r-- | src/aig/fra/fraCore.c | 24 | ||||
-rw-r--r-- | src/aig/fra/fraInd.c | 108 | ||||
-rw-r--r-- | src/aig/fra/fraMan.c | 30 | ||||
-rw-r--r-- | src/aig/fra/fraSim.c | 24 | ||||
-rw-r--r-- | src/base/abci/abc.c | 101 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 69 | ||||
-rw-r--r-- | src/base/abci/abcMiter.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcStrash.c | 65 | ||||
-rw-r--r-- | src/base/io/ioReadAiger.c | 6 |
24 files changed, 532 insertions, 112 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 4d23e029..d6a97257 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -92,7 +92,7 @@ struct Aig_Man_t_ Vec_Ptr_t * vBufs; // the array of buffers Aig_Obj_t * pConst1; // the constant 1 node Aig_Obj_t Ghost; // the ghost node - int nRegs; // the number of registers + int nRegs; // the number of registers (registers are last POs) int nAsserts; // the number of asserts among POs (asserts are first POs) // AIG node counters int nObjs[AIG_OBJ_VOID];// the number of objects by type @@ -202,6 +202,7 @@ static inline int Aig_ObjIsTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * p static inline int Aig_ObjTravId( Aig_Obj_t * pObj ) { return (int)pObj->pData; } static inline int Aig_ObjPhase( Aig_Obj_t * pObj ) { return pObj->fPhase; } +static inline int Aig_ObjPhaseReal( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 1; } static inline int Aig_ObjRefs( Aig_Obj_t * pObj ) { return pObj->nRefs; } static inline void Aig_ObjRef( Aig_Obj_t * pObj ) { pObj->nRefs++; } static inline void Aig_ObjDeref( Aig_Obj_t * pObj ) { assert( pObj->nRefs > 0 ); pObj->nRefs--; } @@ -218,7 +219,6 @@ static inline Aig_Obj_t * Aig_ObjChild0Copy( Aig_Obj_t * pObj ) { assert( !Aig static inline Aig_Obj_t * Aig_ObjChild1Copy( Aig_Obj_t * pObj ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL; } static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj->Level; } static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } -static inline int Aig_ObjFaninPhase( Aig_Obj_t * pObj ) { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0; } static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) @@ -335,6 +335,8 @@ static inline int Aig_ObjFanoutNext( Aig_Man_t * p, int iFan ) { assert(iF /*=== aigCheck.c ========================================================*/ extern int Aig_ManCheck( Aig_Man_t * p ); +extern void Aig_ManCheckMarkA( Aig_Man_t * p ); +extern void Aig_ManCheckPhase( Aig_Man_t * p ); /*=== aigDfs.c ==========================================================*/ extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); @@ -356,7 +358,7 @@ extern void Aig_ManFanoutStop( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManStart( int nNodesMax ); extern Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ); extern Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ); -extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); +extern Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ); extern void Aig_ManStop( Aig_Man_t * p ); extern int Aig_ManCleanup( Aig_Man_t * p ); extern void Aig_ManPrintStats( Aig_Man_t * p ); @@ -438,7 +440,7 @@ extern unsigned * Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, extern unsigned Aig_PrimeCudd( unsigned p ); extern void Aig_ManIncrementTravId( Aig_Man_t * p ); extern int Aig_ManLevels( Aig_Man_t * p ); -extern void Aig_ManCheckMarkA( Aig_Man_t * p ); +extern void Aig_ManResetRefs( Aig_Man_t * p ); extern void Aig_ManCleanMarkA( Aig_Man_t * p ); extern void Aig_ManCleanMarkB( Aig_Man_t * p ); extern void Aig_ManCleanData( Aig_Man_t * p ); @@ -452,6 +454,7 @@ extern void Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_ extern void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level ); 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 ); /*=== 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 1a8f108e..dc01f779 100644 --- a/src/aig/aig/aigCheck.c +++ b/src/aig/aig/aigCheck.c @@ -114,6 +114,47 @@ int Aig_ManCheck( Aig_Man_t * p ) return 1; } +/**Function************************************************************* + + Synopsis [Checks if the markA is reset.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCheckMarkA( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + assert( pObj->fMarkA == 0 ); +} + +/**Function************************************************************* + + Synopsis [Checks the consistency of phase assignment.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManCheckPhase( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i; + Aig_ManForEachObj( p, pObj, i ) + if ( Aig_ObjIsPi(pObj) ) + assert( (int)pObj->fPhase == 0 ); + else + assert( (int)pObj->fPhase == (Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) & Aig_ObjPhaseReal(Aig_ObjChild1(pObj))) ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 50093195..818b75fe 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -135,6 +135,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) int i; // create the new manager pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew->nRegs = p->nRegs; + pNew->nAsserts = p->nAsserts; // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -179,12 +181,11 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ) +Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ) { Aig_Man_t * pNew; Aig_Obj_t * pObj; int i; - assert( nNodes == 2 ); // create the new manager pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); // create the PIs @@ -193,10 +194,10 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes Aig_ManForEachPi( p, pObj, i ) pObj->pData = Aig_ObjCreatePi(pNew); // dump the nodes - for ( i = 0; i < nNodes; i++ ) - Aig_ManDup_rec( pNew, p, ppNodes[i] ); + Aig_ManDup_rec( pNew, p, pNode1 ); + Aig_ManDup_rec( pNew, p, pNode2 ); // construct the EXOR - pObj = Aig_Exor( pNew, ppNodes[0]->pData, ppNodes[1]->pData ); + pObj = Aig_Exor( pNew, pNode1->pData, pNode2->pData ); pObj = Aig_NotCond( pObj, Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) ); // add the PO Aig_ObjCreatePo( pNew, pObj ); diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c index a017ff2d..34c07dce 100644 --- a/src/aig/aig/aigObj.c +++ b/src/aig/aig/aigObj.c @@ -135,7 +135,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj } // set level and phase pObj->Level = Aig_ObjLevelNew( pObj ); - pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1); + pObj->fPhase = Aig_ObjPhaseReal(pFan0) & Aig_ObjPhaseReal(pFan1); // add the node to the structural hash table if ( Aig_ObjIsHash(pObj) ) Aig_TableInsert( p, pObj ); @@ -285,6 +285,7 @@ void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, i { assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) ); pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) ); + assert( Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) == Aig_ObjPhaseReal(pFanReal0) ); Aig_ObjPatchFanin0( p, pObj, pFanReal0 ); return; } diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index 47df7982..a862bf97 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -232,6 +232,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) int i; // start the HOP package pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew->nRegs = p->nRegs; Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 ); // map the const and primary inputs Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index 0d4ffd1f..ba359c09 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -99,7 +99,7 @@ clk = clock(); } nEntries = Aig_ManNodeNum(p); assert( Counter == nEntries ); -// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); + printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); PRT( "Time", clock() - clk ); // replace the table and the parameters free( pTableOld ); diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 364c32a3..cdf1fdf7 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -104,7 +104,7 @@ int Aig_ManLevels( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Checks if the markA is reset.] + Synopsis [Reset reference counters.] Description [] @@ -113,17 +113,24 @@ int Aig_ManLevels( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_ManCheckMarkA( Aig_Man_t * p ) +void Aig_ManResetRefs( Aig_Man_t * p ) { Aig_Obj_t * pObj; int i; Aig_ManForEachObj( p, pObj, i ) - assert( pObj->fMarkA == 0 ); + pObj->nRefs = 0; + Aig_ManForEachObj( p, pObj, i ) + { + if ( Aig_ObjFanin0(pObj) ) + Aig_ObjFanin0(pObj)->nRefs++; + if ( Aig_ObjFanin1(pObj) ) + Aig_ObjFanin1(pObj)->nRefs++; + } } /**Function************************************************************* - Synopsis [Checks if the markA is reset.] + Synopsis [Cleans MarkB.] Description [] @@ -142,7 +149,7 @@ void Aig_ManCleanMarkA( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Checks if the markA is reset.] + Synopsis [Cleans MarkB.] Description [] @@ -621,6 +628,27 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig ) /**Function************************************************************* + Synopsis [Write speculative miter for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDump( Aig_Man_t * p ) +{ + static int Counter = 0; + char FileName[20]; + // dump the logic into a file + sprintf( FileName, "aigbug\\%03d.blif", ++Counter ); + Aig_ManDumpBlif( p, FileName ); + printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName ); +} + +/**Function************************************************************* + Synopsis [Writes the AIG into the BLIF file.] Description [] @@ -679,6 +707,10 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) // 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 ); diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c index 13de745b..06731451 100644 --- a/src/aig/cnf/cnfCore.c +++ b/src/aig/cnf/cnfCore.c @@ -75,6 +75,8 @@ clk = clock(); Aig_MmFixedStop( pMemCuts, 0 ); p->timeSave = clock() - clk; + // reset reference counters + Aig_ManResetRefs( pAig ); //PRT( "Cuts ", p->timeCuts ); //PRT( "Map ", p->timeMap ); //PRT( "Saving ", p->timeSave ); diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 44dd2788..923ffc12 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -85,6 +85,7 @@ extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax ); extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ); extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ); /*=== darScript.c ========================================================*/ +extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ); extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 097f1a4d..9c0997b8 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -54,6 +54,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) int i; // create the new manager pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew->nRegs = p->nRegs; + pNew->nAsserts = p->nAsserts; // map the PI nodes Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index b74f570c..dec9bff7 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -42,7 +42,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ) { memset( pPars, 0, sizeof(Dar_RwrPar_t) ); - pPars->nCutsMax = 8; + pPars->nCutsMax = 8; // 8 pPars->nSubgMax = 5; // 5 is a "magic number" pPars->fFanout = 1; pPars->fUpdateLevel = 0; @@ -151,8 +151,8 @@ p->timeCuts += clock() - clk; Dar_ObjSetCuts( pObj, NULL ); // if we end up here, a rewriting step is accepted nNodeBefore = Aig_ManNodeNum( pAig ); - pObjNew = Dar_LibBuildBest( p ); - pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase ); + pObjNew = Dar_LibBuildBest( p ); // pObjNew can be complemented! + pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase ); assert( (int)Aig_Regular(pObjNew)->Level <= Required ); // replace the node Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel ); @@ -183,6 +183,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; } // stop the rewriting manager Dar_ManStop( p ); + Aig_ManCheckPhase( pAig ); // check if ( !Aig_ManCheck( pAig ) ) { @@ -209,9 +210,12 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax ) Dar_RwrPar_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Aig_MmFixed_t * pMemCuts; - int i, clk = 0, clkStart = clock(); + int i, nNodes, clk = 0, clkStart = clock(); // remove dangling nodes - Aig_ManCleanup( pAig ); + if ( nNodes = Aig_ManCleanup( pAig ) ) + { +// printf( "Removing %d nodes.\n", nNodes ); + } // create default parameters Dar_ManDefaultRwrParams( pPars ); pPars->nCutsMax = nCutsMax; diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index fbd12cae..b304fe34 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -361,6 +361,21 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in Aig_ObjCollectCut( pObj, vCut, p->vCutNodes ); // get the truth table pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore ); + if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) ) + { + p->GainBest = Vec_PtrSize(p->vCutNodes); + p->pGraphBest = Kit_GraphCreateConst0(); + Vec_PtrCopy( p->vLeavesBest, vCut ); + return p->GainBest; + } + if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) ) + { + p->GainBest = Vec_PtrSize(p->vCutNodes); + p->pGraphBest = Kit_GraphCreateConst1(); + Vec_PtrCopy( p->vLeavesBest, vCut ); + return p->GainBest; + } + // try the positive phase RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 ); if ( RetValue > -1 ) @@ -559,6 +574,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; // stop the rewriting manager Dar_ManRefStop( p ); + Aig_ManCheckPhase( pAig ); if ( !Aig_ManCheck( pAig ) ) { printf( "Dar_ManRefactor: The network check has failed.\n" ); diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 75076981..2fe39860 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -30,6 +30,30 @@ /**Function************************************************************* + Synopsis [Performs one iteration of AIG rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) +{ + Aig_Man_t * pTemp; + Dar_RwrPar_t Pars, * pPars = &Pars; + Dar_ManDefaultRwrParams( pPars ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + Dar_ManRewrite( pAig, pPars ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + return pAig; +} + +/**Function************************************************************* + Synopsis [Reproduces script "compress2".] Description [] diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 91a1f8b1..5d357290 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -70,6 +70,7 @@ struct Fra_Par_t_ int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output int nFramesK; // the number of timeframes to unroll + int fRewrite; // use rewriting for constraint reduction }; // FRAIG equivalence classes @@ -121,11 +122,13 @@ struct Fra_Man_t_ // statistics int nSimRounds; int nNodesMiter; - int nClassesZero; - int nClassesBeg; - int nClassesEnd; - int nPairsBeg; - int nPairsEnd; + int nLitsZero; + int nLitsBeg; + int nLitsEnd; + int nNodesBeg; + int nNodesEnd; + int nRegsBeg; + int nRegsEnd; int nSatCalls; int nSatCallsSat; int nSatCallsUnsat; @@ -138,6 +141,7 @@ struct Fra_Man_t_ // runtime int timeSim; int timeTrav; + int timeRwr; int timeSat; int timeSatUnsat; int timeSatSat; @@ -182,7 +186,7 @@ static inline Aig_Obj_t * Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( extern Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ); extern void Fra_ClassesStop( Fra_Cla_t * p ); extern void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ); -extern void Fra_ClassesPrint( Fra_Cla_t * p ); +extern void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ); extern void Fra_ClassesPrepare( Fra_Cla_t * p ); extern int Fra_ClassesRefine( Fra_Cla_t * p ); extern int Fra_ClassesRefine1( Fra_Cla_t * p ); @@ -197,7 +201,7 @@ extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); extern void Fra_FraigSweep( Fra_Man_t * pManAig ); /*=== fraDfs.c ========================================================*/ /*=== fraInd.c ========================================================*/ -extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose ); +extern Aig_Man_t * Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose ); /*=== fraMan.c ========================================================*/ extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 05c07889..31d6270a 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -215,25 +215,28 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p ) SeeAlso [] ***********************************************************************/ -void Fra_ClassesPrint( Fra_Cla_t * p ) +void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose ) { Aig_Obj_t ** pClass; Aig_Obj_t * pObj; int i; + printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) ); -/* - printf( "Constants { " ); - Vec_PtrForEachEntry( p->vClasses1, pObj, i ) - printf( "%d ", pObj->Id ); - printf( "}\n" ); - Vec_PtrForEachEntry( p->vClasses, pClass, i ) + + if ( fVeryVerbose ) { - printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); - Fra_PrintClass( pClass ); + printf( "Constants { " ); + Vec_PtrForEachEntry( p->vClasses1, pObj, i ) + printf( "%d ", pObj->Id ); + printf( "}\n" ); + Vec_PtrForEachEntry( p->vClasses, pClass, i ) + { + printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) ); + Fra_PrintClass( pClass ); + } + printf( "\n" ); } - printf( "\n" ); -*/ } /**Function************************************************************* diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 9f2b8ca7..71e12a75 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -39,7 +39,7 @@ SeeAlso [] ***********************************************************************/ -void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig ) +static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig ) { static int Counter = 0; char FileName[20]; @@ -47,8 +47,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr Aig_Obj_t * pNode; int i; // create manager with the logic for these two nodes - Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig }; - pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 ); + pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig ); // dump the logic into a file sprintf( FileName, "aig\\%03d.blif", ++Counter ); Aig_ManDumpBlif( pTemp, FileName ); @@ -70,7 +69,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr SeeAlso [] ***********************************************************************/ -void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) +static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) { Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig; int RetValue; @@ -123,6 +122,8 @@ void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) // simulate the counter-example and return the Fraig node Fra_Resimulate( p ); assert( Fra_ClassObjRepr(pObj) != pObjRepr ); + if ( Fra_ClassObjRepr(pObj) == pObjRepr ) + printf( "Fra_FraigNode(): Error in class refinement!\n" ); } /**Function************************************************************* @@ -141,8 +142,6 @@ void Fra_FraigSweep( Fra_Man_t * p ) ProgressBar * pProgress; Aig_Obj_t * pObj, * pObjNew; int i, k = 0; -p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1); -p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); // duplicate internal nodes pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) ); // fraig latch outputs @@ -163,7 +162,6 @@ p->nClassesBeg = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vC Fra_FraigNode( p, pObj ); } Extra_ProgressBarStop( pProgress ); -p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0); // try to prove the outputs of the miter p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); // Fra_MiterStatus( p->pManFraig ); @@ -196,15 +194,23 @@ clk = clock(); Fra_Simulate( p, 0 ); if ( p->pPars->fChoicing ) Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); + // collect initial states + p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nNodesBeg = Aig_ManNodeNum(pManAig); + p->nRegsBeg = Aig_ManRegNum(pManAig); + // perform fraig sweep Fra_FraigSweep( p ); Fra_ManFinalizeComb( p ); if ( p->pPars->fChoicing ) { + int clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); pManAigNew = Aig_ManDupRepr( p->pManAig ); Aig_ManCreateChoices( pManAigNew ); Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; +p->timeTrav += clock() - clk2; } else { @@ -221,6 +227,10 @@ clk = clock(); */ } p->timeTotal = clock() - clk; + // collect final stats + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nNodesEnd = Aig_ManNodeNum(pManAigNew); + p->nRegsEnd = Aig_ManRegNum(pManAigNew); Fra_ManStop( p ); return pManAigNew; } diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 71e535f7..bb4c4287 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -20,6 +20,7 @@ #include "fra.h" #include "cnf.h" +#include "dar.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -31,6 +32,54 @@ /**Function************************************************************* + Synopsis [Performs AIG rewriting on the constaint manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Fra_FraigInductionRewrite( Fra_Man_t * p ) +{ + Aig_Man_t * pTemp; + Aig_Obj_t * pObj, * pObjPo; + int nTruePis, k, i, clk = clock(); + // perform AIG rewriting on the speculated frames + pTemp = Aig_ManDup( p->pManFraig, 0 ); +// pTemp = Dar_ManRwsat( pTemp, 1, 0 ); + pTemp = Dar_ManRewriteDefault( pTemp ); + +// printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); +//Aig_ManDumpBlif( p->pManFraig, "1.blif" ); +//Aig_ManDumpBlif( pTemp, "2.blif" ); + +// Fra_FramesWriteCone( pTemp ); +// Aig_ManStop( pTemp ); + // transfer PI/register pointers + assert( p->pManFraig->nRegs == pTemp->nRegs ); + assert( p->pManFraig->nAsserts == pTemp->nAsserts ); + nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); + memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); + Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) ); + Aig_ManForEachPiSeq( p->pManAig, pObj, i ) + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) ); + k = 0; + assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts ); + Aig_ManForEachLoSeq( p->pManAig, pObj, i ) + { + pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++); + Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) ); + } + // exchange + Aig_ManStop( p->pManFraig ); + p->pManFraig = pTemp; +p->timeRwr += clock() - clk; +} + +/**Function************************************************************* + Synopsis [Performs speculative reduction for one node.] Description [] @@ -131,6 +180,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) Aig_ManForEachLiSeq( p->pManAig, pObj, i ) Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) ); + // remove dangling nodes + Aig_ManCleanup( pManFraig ); // make sure the satisfying assignment is node assigned assert( pManFraig->pData == NULL ); return pManFraig; @@ -147,35 +198,39 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose ) +Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose ) { Fra_Man_t * p; Fra_Par_t Pars, * pPars = &Pars; Aig_Obj_t * pObj; Cnf_Dat_t * pCnf; Aig_Man_t * pManAigNew; - int nIter, i; + int nIter, i, clk = clock(), clk2; if ( Aig_ManNodeNum(pManAig) == 0 ) return Aig_ManDup(pManAig, 1); assert( Aig_ManLatchNum(pManAig) == 0 ); assert( Aig_ManRegNum(pManAig) > 0 ); assert( nFramesK > 0 ); +//Aig_ManShow( pManAig, 0, NULL ); // get parameters Fra_ParamsDefaultSeq( pPars ); pPars->nFramesK = nFramesK; pPars->fVerbose = fVerbose; + pPars->fRewrite = fRewrite; // start the fraig manager for this run p = Fra_ManStart( pManAig, pPars ); - // derive and refine e-classes using the 1st init frame + // derive and refine e-classes using K initialized frames Fra_Simulate( p, 1 ); -// Fra_ClassesTest( p->pCla, 2, 3 ); -//Aig_ManShow( pManAig, 0, NULL ); - - // refine e-classes using sequential simulation + // refine e-classes using sequential simulation? + p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 ); + p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); + p->nNodesBeg = Aig_ManNodeNum(pManAig); + p->nRegsBeg = Aig_ManRegNum(pManAig); + // iterate the inductive case p->pCla->fRefinement = 1; for ( nIter = 0; p->pCla->fRefinement; nIter++ ) @@ -184,6 +239,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose p->pCla->fRefinement = 0; // derive non-init K-timeframes while implementing e-classes p->pManFraig = Fra_FramesWithClasses( p ); + // perform AIG rewriting + if ( p->pPars->fRewrite ) + Fra_FraigInductionRewrite( p ); + // report the intermediate results if ( fVerbose ) { printf( "%3d : Const = %6d. Class = %6d. L = %6d. LR = %6d. N = %6d. NR = %6d.\n", @@ -191,19 +250,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts, Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) ); } - // perform AIG rewriting on the speculated frames // convert the manager to SAT solver (the last nLatches outputs are inputs) -// pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); - pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); + pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); +// pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) ); //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 ); p->pSat = Cnf_DataWriteIntoSolver( pCnf ); p->nSatVars = pCnf->nVars; + assert( p->pSat != NULL ); + if ( p->pSat == NULL ) + printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" ); // set the pointers to the manager Aig_ManForEachObj( p->pManFraig, pObj, i ) pObj->pData = p; + // transfer PI/LO variable numbers pObj = Aig_ManConst1( p->pManFraig ); Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); @@ -216,20 +278,40 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose Fra_ObjSetFaninVec( pObj, (void *)1 ); } Cnf_DataFree( pCnf ); +/* + Aig_ManForEachObj( p->pManFraig, pObj, i ) + { + Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] ); + Fra_ObjSetFaninVec( pObj, (void *)1 ); + } + Cnf_DataFree( pCnf ); +*/ // perform sweeping Fra_FraigSweep( p ); assert( p->vTimeouts == NULL ); + if ( p->vTimeouts ) + printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); // cleanup Fra_ManClean( p ); } - - // move the classes into representatives + // move the classes into representatives and reduce AIG +clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - // implement the classes pManAigNew = Aig_ManDupRepr( pManAig ); +p->timeTrav += clock() - clk2; +p->timeTotal = clock() - clk; + // get the final stats + p->nLitsEnd = Fra_ClassesCountLits( p->pCla ); + p->nNodesEnd = Aig_ManNodeNum(pManAigNew); + p->nRegsEnd = Aig_ManRegNum(pManAigNew); + // free the manager Fra_ManStop( p ); + // check the output + if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 ) + if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) ) + printf( "Proved output constant 0.\n" ); return pManAigNew; } diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index fdd1ccc5..95cf28d8 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -55,6 +55,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) pPars->nBTLimitMiter = 500000; // conflict limit at an output pPars->nFramesK = 0; // the number of timeframes to unroll pPars->fConeBias = 1; + pPars->fRewrite = 0; } /**Function************************************************************* @@ -71,7 +72,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 4; // the number of words in the simulation info + pPars->nSimWords = 1; // the number of words in the simulation info pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached pPars->fPatScores = 0; // enables simulation pattern scoring pPars->MaxScore = 25; // max score after which resimulation is used @@ -80,10 +81,11 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) // pPars->dActConeBumpMax = 5.0; // the largest bump of activity pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode = 1000000; // conflict limit at a node + pPars->nBTLimitNode =10000000; // conflict limit at a node pPars->nBTLimitMiter = 500000; // conflict limit at an output pPars->nFramesK = 1; // the number of timeframes to unroll pPars->fConeBias = 0; + pPars->fRewrite = 0; } /**Function************************************************************* @@ -165,7 +167,6 @@ void Fra_ManClean( Fra_Man_t * p ) sat_solver_delete( p->pSat ); p->pSat = NULL; - p->nSatVars = 0; } /**Function************************************************************* @@ -268,23 +269,28 @@ void Fra_ManStop( Fra_Man_t * p ) void Fra_ManPrint( Fra_Man_t * p ) { double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20); - printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb. ", p->nSimWords, p->nSimRounds, nMemory ); - printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd ); - printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter ); - printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", - p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero ); - printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", - p->pManFraig? Aig_ManNodeNum(p->pManFraig) : -1, p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars ); + printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", + p->nSimWords, p->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg ); + printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", + p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars ); + printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", + p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg ); if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); PRT( "AIG simulation ", p->timeSim ); - PRT( "AIG traversal ", p->timeTrav ); - PRT( "SAT solving ", p->timeSat ); + PRT( "AIG traversal ", p->timeTrav ); + if ( p->timeRwr ) + { + PRT( "AIG rewriting ", p->timeRwr ); + } + PRT( "SAT solving ", p->timeSat ); PRT( " Unsat ", p->timeSatUnsat ); PRT( " Sat ", p->timeSatSat ); PRT( " Fail ", p->timeSatFail ); PRT( "Class refining ", p->timeRef ); PRT( "TOTAL RUNTIME ", p->timeTotal ); if ( p->time1 ) { PRT( "time1 ", p->time1 ); } + if ( p->nSpeculs ) printf( "Speculations = %d.\n", p->nSpeculs ); } diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 4ae8a686..4a6e0251 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -142,10 +142,14 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat ) Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 ); assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) ); - // flip one bit of the first frame - Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 ); - for ( i = 0; i < Limit; i++ ) - Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 ); + // flip one bit of the last frame + if ( p->nFramesAll == 2 ) + { + Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 ); + for ( i = 0; i < Limit; i++ ) + Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, i) ), i+1 ); +// Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, nTruePis*(p->nFramesAll-2) + i) ), i+1 ); + } } } @@ -261,8 +265,8 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame ) pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame; // get complemented attributes of the children using their random info fCompl = pObj->fPhase; - fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); - fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj)); + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); + fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj)); // simulate if ( fCompl0 && fCompl1 ) { @@ -326,7 +330,7 @@ void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame ) pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame; // get complemented attributes of the children using their random info fCompl = pObj->fPhase; - fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj)); + fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj)); // copy information as it is if ( fCompl0 ) for ( i = 0; i < nSimWords; i++ ) @@ -624,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit ) Fra_AssignRandom( p, fInit ); Fra_SimulateOne( p ); Fra_ClassesPrepare( p->pCla ); -// Fra_ClassesPrint( p->pCla ); +// Fra_ClassesPrint( p->pCla, 0 ); //printf( "Starting classes = %5d. Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) ); // refine classes by walking 0/1 patterns @@ -667,7 +671,7 @@ p->timeRef += clock() - clk; // printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", // Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) ); -// Fra_ClassesPrint( p->pCla ); +// Fra_ClassesPrint( p->pCla, 0 ); } /**Function************************************************************* @@ -729,7 +733,7 @@ int Fra_CheckOutputSims( Fra_Man_t * p ) int i; // make sure the reference simulation pattern does not detect the bug pObj = Aig_ManPo( p->pManAig, 0 ); - assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0 + assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); Aig_ManForEachPo( p->pManAig, pObj, i ) { if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 8ae5bb9e..3a916fdc 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -157,6 +157,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_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 ); @@ -320,6 +321,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", "pipe", Abc_CommandPipe, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 ); @@ -371,6 +373,10 @@ void Abc_End() // Dar_LibDumpPriorities(); { + extern void Cnf_ClearMemory(); + Cnf_ClearMemory(); + } + { extern void Dar_LibStop(); Dar_LibStop(); } @@ -4080,19 +4086,20 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "The network is not strashed.\n" ); return 1; } - +/* if ( Abc_NtkPoNum(pNtk) == 1 ) { fprintf( pErr, "The network already has one PO.\n" ); return 1; } - +*/ +/* if ( Abc_NtkLatchNum(pNtk) ) { fprintf( pErr, "The miter has latches. ORing is not performed.\n" ); return 1; } - +*/ // get the new network if ( !Abc_NtkCombinePos( pNtk, 0 ) ) { @@ -10113,6 +10120,78 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandZero( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + + extern Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ); + + 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_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for AIGs.\n" ); + return 0; + } + + // get the new network + pNtkRes = Abc_NtkRestrashZero( pNtk, 0 ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Converting to sequential AIG has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: zero [-h]\n" ); + fprintf( pErr, "\t converts latches to have const-0 initial value\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; @@ -10736,8 +10815,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) int nFramesK; int fExdc; int fImp; + int fRewrite; int fVerbose; - extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -10747,9 +10827,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) nFramesK = 1; fExdc = 1; fImp = 0; + fRewrite = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF ) { switch ( c ) { @@ -10770,6 +10851,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'i': fImp ^= 1; break; + case 'r': + fRewrite ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -10799,7 +10883,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fVerbose ); + pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Sequential sweeping has failed.\n" ); @@ -10810,11 +10894,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" ); - fprintf( pErr, "\t performs sequential sweep using van Eijk's method\n" ); + fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" ); + fprintf( pErr, "\t performs sequential sweep using K-step induction\n" ); fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK ); // fprintf( pErr, "\t-e : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" ); // fprintf( pErr, "\t-i : toggle computing implications [default = %s]\n", fImp? "yes": "no" ); + fprintf( pErr, "\t-r : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 035daeff..ca80fec8 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -36,24 +36,48 @@ Synopsis [Converts the network from the AIG manager into ABC.] - Description [] + Description [Assumes that registers are ordered after PIs/POs.] SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) +Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) { Aig_Man_t * pMan; + Aig_Obj_t * pObjNew; Abc_Obj_t * pObj; - int i; + int i, nNodes; + // make sure the latches follow PIs/POs + if ( fRegisters ) + { + assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( i < Abc_NtkPiNum(pNtk) ) + assert( Abc_ObjIsPi(pObj) ); + else + assert( Abc_ObjIsBo(pObj) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + if ( i < Abc_NtkPoNum(pNtk) ) + assert( Abc_ObjIsPo(pObj) ); + else + assert( Abc_ObjIsBi(pObj) ); + } // create the manager pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); + // save the number of registers + if ( fRegisters ) + pMan->nRegs = Abc_NtkLatchNum(pNtk); // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); Abc_NtkForEachCi( pNtk, pObj, i ) pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan); + // complement the 1-values registers + if ( fRegisters ) + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Abc_LatchIsInit1(pObj) ) + Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); // perform the conversion of the internal nodes (assumes DFS ordering) Abc_NtkForEachNode( pNtk, pObj, i ) { @@ -63,7 +87,14 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) // create the POs Abc_NtkForEachCo( pNtk, pObj, i ) Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) ); - Aig_ManCleanup( pMan ); + // complement the 1-valued registers + if ( fRegisters ) + Aig_ManForEachLiSeq( pMan, pObjNew, i ) + if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) ) + pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0); + // remove dangling nodes + if ( nNodes = Aig_ManCleanup( pMan ) ) + printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes ); if ( !Aig_ManCheck( pMan ) ) { printf( "Abc_NtkToDar: AIG check has failed.\n" ); @@ -296,8 +327,8 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 ) fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0)); - pMan1 = Abc_NtkToDar( pNtk1 ); - pMan2 = Abc_NtkToDar( pNtk2 ); + pMan1 = Abc_NtkToDar( pNtk1, 0 ); + pMan2 = Abc_NtkToDar( pNtk2, 0 ); Aig_ManPrintStats( pMan1 ); Aig_ManPrintStats( pMan2 ); @@ -342,7 +373,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; if ( !Aig_ManCheck( pMan ) ) @@ -410,7 +441,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in Fra_Par_t Pars, * pPars = &Pars; Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; Fra_ParamsDefault( pPars ); @@ -446,7 +477,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose ); Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose ); @@ -473,7 +504,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars ) Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; // Aig_ManPrintStats( pMan ); @@ -517,7 +548,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars ) Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; // Aig_ManPrintStats( pMan ); @@ -554,7 +585,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; // Aig_ManPrintStats( pMan ); @@ -587,7 +618,7 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ) Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; // Aig_ManPrintStats( pMan ); @@ -696,7 +727,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) assert( Abc_NtkIsStrash(pNtk) ); // convert to the AIG manager - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; if ( !Aig_ManCheck( pMan ) ) @@ -751,7 +782,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer assert( Abc_NtkPoNum(pNtk) == 1 ); // conver to the manager - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); // derive CNF // pCnf = Cnf_Derive( pMan, 0 ); pCnf = Cnf_DeriveSimple( pMan, 0 ); @@ -809,7 +840,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer assert( 0 ); // PRT( "SAT sat_solver time", clock() - clk ); // printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts ); - + // if the problem is SAT, get the counterexample if ( status == l_True ) { @@ -836,16 +867,16 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fVerbose ) +Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose ) { Abc_Ntk_t * pNtkAig; Aig_Man_t * pMan, * pTemp; - pMan = Abc_NtkToDar( pNtk ); + pMan = Abc_NtkToDar( pNtk, 0 ); if ( pMan == NULL ) return NULL; pMan->nRegs = Abc_NtkLatchNum(pNtk); - pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fVerbose ); + pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose ); Aig_ManStop( pTemp ); pNtkAig = Abc_NtkFromDar( pNtk, pMan ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 445c73c1..a33b9875 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -1099,7 +1099,9 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd ) Abc_Obj_t * pNode, * pMiter; int i; assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkLatchNum(pNtk) == 0 ); +// assert( Abc_NtkLatchNum(pNtk) == 0 ); + if ( Abc_NtkPoNum(pNtk) == 1 ) + return 1; // start the result if ( fAnd ) pMiter = Abc_AigConst1(pNtk); diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c index 978b7cdb..4fdb7cbc 100644 --- a/src/base/abci/abcStrash.c +++ b/src/base/abci/abcStrash.c @@ -87,6 +87,71 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup ) /**Function************************************************************* + Synopsis [Reapplies structural hashing to the AIG.] + + Description [Because of the structural hashing, this procedure should not + change the number of nodes. It is useful to detect the bugs in the original AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup ) +{ + extern int timeRetime; + Abc_Ntk_t * pNtkAig; + Abc_Obj_t * pObj; + int i, nNodes;//, RetValue; + assert( Abc_NtkIsStrash(pNtk) ); +//timeRetime = clock(); + // print warning about choice nodes + if ( Abc_NtkGetChoiceNum( pNtk ) ) + printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" ); + // start the new network (constants and CIs of the old network will point to the their counterparts in the new network) + pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // complement the 1-values registers + Abc_NtkForEachLatch( pNtk, pObj, i ) + if ( Abc_LatchIsInit1(pObj) ) + Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy); + // restrash the nodes (assuming a topological order of the old network) + Abc_NtkForEachNode( pNtk, pObj, i ) + pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + // finalize the network + Abc_NtkFinalize( pNtk, pNtkAig ); + // complement the 1-valued registers + Abc_NtkForEachLatch( pNtkAig, pObj, i ) + if ( Abc_LatchIsInit1(pObj) ) + Abc_ObjXorFaninC( Abc_ObjFanin0(pObj), 0 ); + // set all constant-0 values + Abc_NtkForEachLatch( pNtkAig, pObj, i ) + Abc_LatchSetInit0( pObj ); + + // print warning about self-feed latches +// if ( Abc_NtkCountSelfFeedLatches(pNtkAig) ) +// printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) ); + // perform cleanup if requested + if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) + printf( "Abc_NtkRestrash(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes ); + // duplicate EXDC + if ( pNtk->pExdc ) + pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkStrash: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } +//timeRetime = clock() - timeRetime; +// if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) ) +// printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue ); + return pNtkAig; + +} + +/**Function************************************************************* + Synopsis [Transforms logic network into structurally hashed AIG.] Description [] diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index fe519476..23b5b350 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -123,7 +123,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) // assign names to latch and its input Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); - printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); +// printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); } // remember the beginning of latch/PO literals @@ -161,7 +161,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); - printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id ); +// printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id ); } // read the PO driver literals @@ -233,7 +233,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) } // remove the extra nodes -// Abc_AigCleanup( pNtkNew->pManFunc ); + Abc_AigCleanup( pNtkNew->pManFunc ); // check the result if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) ) |