summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/aig/aig.h11
-rw-r--r--src/aig/aig/aigCheck.c41
-rw-r--r--src/aig/aig/aigMan.c11
-rw-r--r--src/aig/aig/aigObj.c3
-rw-r--r--src/aig/aig/aigRepr.c1
-rw-r--r--src/aig/aig/aigTable.c2
-rw-r--r--src/aig/aig/aigUtil.c42
-rw-r--r--src/aig/cnf/cnfCore.c2
-rw-r--r--src/aig/dar/dar.h1
-rw-r--r--src/aig/dar/darBalance.c2
-rw-r--r--src/aig/dar/darCore.c14
-rw-r--r--src/aig/dar/darRefact.c16
-rw-r--r--src/aig/dar/darScript.c24
-rw-r--r--src/aig/fra/fra.h18
-rw-r--r--src/aig/fra/fraClass.c25
-rw-r--r--src/aig/fra/fraCore.c24
-rw-r--r--src/aig/fra/fraInd.c108
-rw-r--r--src/aig/fra/fraMan.c30
-rw-r--r--src/aig/fra/fraSim.c24
-rw-r--r--src/base/abci/abc.c101
-rw-r--r--src/base/abci/abcDar.c69
-rw-r--r--src/base/abci/abcMiter.c4
-rw-r--r--src/base/abci/abcStrash.c65
-rw-r--r--src/base/io/ioReadAiger.c6
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 ) )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 00:51:37 +0000