summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--abc.dsp6
-rw-r--r--src/aig/aig/aig.h1
-rw-r--r--src/aig/aig/aigDup.c2
-rw-r--r--src/aig/aig/aigMan.c2
-rw-r--r--src/aig/aig/aigObj.c6
-rw-r--r--src/aig/aig/aigTsim.c4
-rw-r--r--src/aig/aig/aigUtil.c88
-rw-r--r--src/aig/bbr/bbrImage.c6
-rw-r--r--src/aig/bbr/module.make2
-rw-r--r--src/aig/cnf/cnf.h1
-rw-r--r--src/aig/cnf/cnfMan.c24
-rw-r--r--src/aig/cnf/cnfWrite.c15
-rw-r--r--src/aig/dar/darBalance.c2
-rw-r--r--src/aig/fra/fra.h2
-rw-r--r--src/aig/fra/fraCec.c8
-rw-r--r--src/aig/fra/fraClaus.c15
-rw-r--r--src/aig/fra/fraHot.c3
-rw-r--r--src/aig/fra/fraMan.c3
-rw-r--r--src/aig/fra/fraSec.c24
-rw-r--r--src/aig/saig/module.make1
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigPhase.c14
-rw-r--r--src/aig/saig/saigRetMin.c6
-rw-r--r--src/aig/saig/saigRetStep.c202
-rw-r--r--src/base/abc/abcShow.c2
-rw-r--r--src/base/abci/abc.c26
-rw-r--r--src/base/abci/abcDar.c36
-rw-r--r--src/base/abci/abcDress.c2
-rw-r--r--src/base/cmd/cmd.c2
-rw-r--r--src/base/io/io.c2
-rw-r--r--src/base/io/ioAbc.h (renamed from src/base/io/io.h)4
-rw-r--r--src/base/io/ioReadAiger.c4
-rw-r--r--src/base/io/ioReadBaf.c2
-rw-r--r--src/base/io/ioReadBench.c2
-rw-r--r--src/base/io/ioReadBlif.c2
-rw-r--r--src/base/io/ioReadBlifMv.c2
-rw-r--r--src/base/io/ioReadDsd.c2
-rw-r--r--src/base/io/ioReadEdif.c2
-rw-r--r--src/base/io/ioReadEqn.c2
-rw-r--r--src/base/io/ioReadPla.c2
-rw-r--r--src/base/io/ioReadVerilog.c2
-rw-r--r--src/base/io/ioUtil.c2
-rw-r--r--src/base/io/ioWriteAiger.c2
-rw-r--r--src/base/io/ioWriteBaf.c2
-rw-r--r--src/base/io/ioWriteBench.c2
-rw-r--r--src/base/io/ioWriteBlif.c2
-rw-r--r--src/base/io/ioWriteBlifMv.c2
-rw-r--r--src/base/io/ioWriteCnf.c2
-rw-r--r--src/base/io/ioWriteDot.c2
-rw-r--r--src/base/io/ioWriteEqn.c2
-rw-r--r--src/base/io/ioWriteGml.c2
-rw-r--r--src/base/io/ioWriteList.c2
-rw-r--r--src/base/io/ioWritePla.c2
-rw-r--r--src/base/io/ioWriteVerilog.c2
-rw-r--r--src/base/io/io_.c2
-rw-r--r--src/base/main/main.h2
-rw-r--r--src/opt/fret/fretInit.c2
57 files changed, 488 insertions, 79 deletions
diff --git a/abc.dsp b/abc.dsp
index 4fababfe..a484406a 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -462,7 +462,7 @@ SOURCE=.\src\base\io\io.c
# End Source File
# Begin Source File
-SOURCE=.\src\base\io\io.h
+SOURCE=.\src\base\io\ioabc.h
# End Source File
# Begin Source File
@@ -3266,6 +3266,10 @@ SOURCE=.\src\aig\saig\saigRetMin.c
# End Source File
# Begin Source File
+SOURCE=.\src\aig\saig\saigRetStep.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\aig\saig\saigScl.c
# End Source File
# End Group
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 47696a41..6ecec3f8 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -622,6 +622,7 @@ extern void Aig_ManDumpVerilog( Aig_Man_t * p, char * pFileName );
extern void Aig_ManSetPioNumbers( Aig_Man_t * p );
extern void Aig_ManCleanPioNumbers( Aig_Man_t * p );
extern int Aig_ManCountChoices( Aig_Man_t * p );
+extern unsigned Aig_ManRandom( int fReset );
/*=== 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/aigDup.c b/src/aig/aig/aigDup.c
index e7623739..9dfa2ddf 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -118,6 +118,8 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
pNew->pName = Aig_UtilStrsav( p->pName );
pNew->pSpec = Aig_UtilStrsav( p->pSpec );
pNew->nRegs = p->nRegs;
+ pNew->nTruePis = p->nTruePis;
+ pNew->nTruePos = p->nTruePos;
pNew->nAsserts = p->nAsserts;
if ( p->vFlopNums )
pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 47ee8d4d..2e68e93c 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -216,7 +216,7 @@ void Aig_ManStop( Aig_Man_t * p )
FREE( p->pObjCopies );
FREE( p->pReprs );
FREE( p->pEquivs );
- free( p->pTable );
+// free( p->pTable );
free( p );
}
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 9c7cf2c4..88fb9c9d 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -361,7 +361,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
// the object to be replaced cannot be complemented
assert( !Aig_IsComplement(pObjOld) );
// the object to be replaced cannot be a terminal
- assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
+// assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
+ assert( !Aig_ObjIsPo(pObjOld) );
// the object to be used cannot be a buffer or a PO
assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) );
// the object cannot be the same
@@ -371,7 +372,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
assert( pObjOld != Aig_ObjFanin1(pObjNewR) );
// recursively delete the old node - but leave the object there
pObjNewR->nRefs++;
- Aig_ObjDelete_rec( p, pObjOld, 0 );
+ if ( !Aig_ObjIsPi(pObjOld) )
+ Aig_ObjDelete_rec( p, pObjOld, 0 );
pObjNewR->nRefs--;
// if the new object is complemented or already used, create a buffer
p->nObjs[pObjOld->Type]--;
diff --git a/src/aig/aig/aigTsim.c b/src/aig/aig/aigTsim.c
index d3f78902..7b48a73d 100644
--- a/src/aig/aig/aigTsim.c
+++ b/src/aig/aig/aigTsim.c
@@ -53,13 +53,13 @@ static inline int Aig_XsimAnd( int Value0, int Value1 )
}
static inline int Aig_XsimRand2()
{
- return (rand() & 1) ? AIG_XVS1 : AIG_XVS0;
+ return (Aig_ManRandom(0) & 1) ? AIG_XVS1 : AIG_XVS0;
}
static inline int Aig_XsimRand3()
{
int RetValue;
do {
- RetValue = rand() & 3;
+ RetValue = Aig_ManRandom(0) & 3;
} while ( RetValue == 0 );
return RetValue;
}
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 00e0311d..a01e9582 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -990,6 +990,94 @@ void Aig_ManPrintControlFanouts( Aig_Man_t * p )
}
}
+/**Function*************************************************************
+
+ Synopsis [Creates a sequence or random numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso [http://en.wikipedia.org/wiki/LFSR]
+
+***********************************************************************/
+void Aig_ManRandomTest2()
+{
+ FILE * pFile;
+ unsigned int lfsr = 1;
+ unsigned int period = 0;
+ pFile = fopen( "rand.txt", "w" );
+ do {
+// lfsr = (lfsr >> 1) ^ (-(lfsr & 1u) & 0xd0000001u); // taps 32 31 29 1
+ lfsr = 1; // to prevent the warning
+ ++period;
+ fprintf( pFile, "%10d : %10d ", period, lfsr );
+// Extra_PrintBinary( pFile, &lfsr, 32 );
+ fprintf( pFile, "\n" );
+ if ( period == 20000 )
+ break;
+ } while(lfsr != 1u);
+ fclose( pFile );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates a sequence or random numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
+
+***********************************************************************/
+void Aig_ManRandomTest1()
+{
+ FILE * pFile;
+ unsigned int lfsr;
+ unsigned int period = 0;
+ pFile = fopen( "rand.txt", "w" );
+ do {
+ lfsr = Aig_ManRandom( 0 );
+ ++period;
+ fprintf( pFile, "%10d : %10d ", period, lfsr );
+// Extra_PrintBinary( pFile, &lfsr, 32 );
+ fprintf( pFile, "\n" );
+ if ( period == 20000 )
+ break;
+ } while(lfsr != 1u);
+ fclose( pFile );
+}
+
+
+#define NUMBER1 3716960521
+#define NUMBER2 2174103536
+
+/**Function*************************************************************
+
+ Synopsis [Creates a sequence or random numbers.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso [http://www.codeproject.com/KB/recipes/SimpleRNG.aspx]
+
+***********************************************************************/
+unsigned Aig_ManRandom( int fReset )
+{
+ static unsigned int m_z = NUMBER1;
+ static unsigned int m_w = NUMBER2;
+ if ( fReset )
+ {
+ m_z = NUMBER1;
+ m_w = NUMBER2;
+ }
+ m_z = 36969 * (m_z & 65535) + (m_z >> 16);
+ m_w = 18000 * (m_w & 65535) + (m_w >> 16);
+ return (m_z << 16) + m_w;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
index cfe70d15..234ae3f8 100644
--- a/src/aig/bbr/bbrImage.c
+++ b/src/aig/bbr/bbrImage.c
@@ -89,7 +89,7 @@ struct Bbr_ImageVar_t_
/* Macro declarations */
/*---------------------------------------------------------------------------*/
-#define BDD_BLOW_UP 1000000
+#define BDD_BLOW_UP 2000000
#define b0 Cudd_Not((dd)->one)
#define b1 (dd)->one
@@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
if ( pTree->nNodesMax < nNodes )
pTree->nNodesMax = nNodes;
}
- if ( dd->keys > BDD_BLOW_UP )
+ if ( dd->keys-dd->dead > BDD_BLOW_UP )
return 0;
return 1;
}
@@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
}
*pfStop = 0;
- if ( dd->keys > BDD_BLOW_UP )
+ if ( dd->keys-dd->dead > BDD_BLOW_UP )
{
*pfStop = 1;
return 0;
diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make
index 52a824b9..07a05869 100644
--- a/src/aig/bbr/module.make
+++ b/src/aig/bbr/module.make
@@ -1,3 +1,3 @@
SRC += src/aig/bbr/bbrImage.c \
src/aig/bbr/bbrNtbdd.c \
- src/aig/bdr/bbrReach.c
+ src/aig/bbr/bbrReach.c
diff --git a/src/aig/cnf/cnf.h b/src/aig/cnf/cnf.h
index cf763e67..9a49805b 100644
--- a/src/aig/cnf/cnf.h
+++ b/src/aig/cnf/cnf.h
@@ -138,6 +138,7 @@ extern void Cnf_DataFree( Cnf_Dat_t * p );
extern void Cnf_DataLift( Cnf_Dat_t * p, int nVarsPlus );
extern void Cnf_DataWriteIntoFile( Cnf_Dat_t * p, char * pFileName, int fReadable );
void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit );
+extern void Cnf_DataWriteOrClause( void * pSat, Cnf_Dat_t * pCnf );
/*=== cnfMap.c ========================================================*/
extern void Cnf_DeriveMapping( Cnf_Man_t * p );
extern int Cnf_ManMapForCnf( Cnf_Man_t * p );
diff --git a/src/aig/cnf/cnfMan.c b/src/aig/cnf/cnfMan.c
index 2ee66916..934aab1c 100644
--- a/src/aig/cnf/cnfMan.c
+++ b/src/aig/cnf/cnfMan.c
@@ -326,6 +326,30 @@ void * Cnf_DataWriteIntoSolver( Cnf_Dat_t * p, int nFrames, int fInit )
return pSat;
}
+/**Function*************************************************************
+
+ Synopsis [Adds the OR-clause.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Cnf_DataWriteOrClause( void * p, Cnf_Dat_t * pCnf )
+{
+ sat_solver * pSat = p;
+ Aig_Obj_t * pObj;
+ int i, * pLits;
+ pLits = ALLOC( int, Aig_ManPoNum(pCnf->pMan) );
+ Aig_ManForEachPo( pCnf->pMan, pObj, i )
+ pLits[i] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+ if ( !sat_solver_addclause( pSat, pLits, pLits + Aig_ManPoNum(pCnf->pMan) ) )
+ assert( 0 );
+ free( pLits );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 23b3e8f0..5556ac2e 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -221,9 +221,18 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
Number = 1;
if ( nOutputs )
{
- assert( nOutputs == Aig_ManRegNum(p->pManAig) );
- Aig_ManForEachLiSeq( p->pManAig, pObj, i )
- pCnf->pVarNums[pObj->Id] = Number++;
+ if ( Aig_ManRegNum(p->pManAig) == 0 )
+ {
+ assert( nOutputs == Aig_ManPoNum(p->pManAig) );
+ Aig_ManForEachPo( p->pManAig, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ }
+ else
+ {
+ assert( nOutputs == Aig_ManRegNum(p->pManAig) );
+ Aig_ManForEachLiSeq( p->pManAig, pObj, i )
+ pCnf->pVarNums[pObj->Id] = Number++;
+ }
}
// assign variables to the internal nodes
Vec_PtrForEachEntry( vMapped, pObj, i )
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 5c9a144f..07685c98 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -220,7 +220,7 @@ void Dar_BalancePermute( Aig_Man_t * p, Vec_Ptr_t * vSuper, int LeftBound, int f
/*
// we did not find the node to share, randomize choice
{
- int Choice = rand() % (RightBound - LeftBound + 1);
+ int Choice = Aig_ManRandom(0) % (RightBound - LeftBound + 1);
pObj3 = Vec_PtrEntry( vSuper, LeftBound + Choice );
if ( pObj3 == pObj2 )
return;
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 44cfe847..7311d414 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -226,7 +226,7 @@ struct Fra_Man_t_
////////////////////////////////////////////////////////////////////////
static inline unsigned * Fra_ObjSim( Fra_Sml_t * p, int Id ) { return p->pData + p->nWordsTotal * Id; }
-static inline unsigned Fra_ObjRandomSim() { return (rand() << 24) ^ (rand() << 12) ^ rand(); }
+static inline unsigned Fra_ObjRandomSim() { return Aig_ManRandom(0); }
static inline Aig_Obj_t * Fra_ObjFraig( Aig_Obj_t * pObj, int i ) { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i]; }
static inline void Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
index 05f2493a..e91478a4 100644
--- a/src/aig/fra/fraCec.c
+++ b/src/aig/fra/fraCec.c
@@ -47,14 +47,16 @@ int Fra_FraigSat( Aig_Man_t * pMan, sint64 nConfLimit, sint64 nInsLimit, int fVe
int status, RetValue, clk = clock();
Vec_Int_t * vCiIds;
- assert( Aig_ManPoNum(pMan) == 1 );
+ assert( Aig_ManRegNum(pMan) == 0 );
pMan->pData = NULL;
// derive CNF
- pCnf = Cnf_Derive( pMan, 0 );
-// pCnf = Cnf_DeriveSimple( pMan, 0 );
+ pCnf = Cnf_Derive( pMan, Aig_ManPoNum(pMan) );
+// pCnf = Cnf_DeriveSimple( pMan, Aig_ManPoNum(pMan) );
// convert into the SAT solver
pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ // add the OR clause for the outputs
+ Cnf_DataWriteOrClause( pSat, pCnf );
vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
Cnf_DataFree( pCnf );
// solve SAT
diff --git a/src/aig/fra/fraClaus.c b/src/aig/fra/fraClaus.c
index c9ea4907..6f0a2012 100644
--- a/src/aig/fra/fraClaus.c
+++ b/src/aig/fra/fraClaus.c
@@ -606,7 +606,8 @@ int Fra_ClausProcessClauses( Clu_Man_t * p, int fRefs )
// simulate the AIG
clk = clock();
- srand( 0xAABBAABB );
+// srand( 0xAABBAABB );
+ Aig_ManRandom(1);
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
if ( p->fTarget && pSeq->fNonConstOut )
{
@@ -661,7 +662,8 @@ PRT( "Infoseq", clock() - clk );
// perform combinational simulation
clk = clock();
- srand( 0xAABBAABB );
+// srand( 0xAABBAABB );
+ Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
@@ -728,7 +730,8 @@ int Fra_ClausProcessClauses2( Clu_Man_t * p, int fRefs )
// simulate the AIG
clk = clock();
- srand( 0xAABBAABB );
+// srand( 0xAABBAABB );
+ Aig_ManRandom(1);
pSeq = Fra_SmlSimulateSeq( p->pAig, 0, p->nPref + p->nSimFrames, p->nSimWords/p->nSimFrames );
if ( p->fTarget && pSeq->fNonConstOut )
{
@@ -743,7 +746,8 @@ if ( p->fVerbose )
// perform combinational simulation
clk = clock();
- srand( 0xAABBAABB );
+// srand( 0xAABBAABB );
+ Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, p->nSimWords + p->nSimWordsPref );
if ( p->fVerbose )
{
@@ -1614,7 +1618,8 @@ void Fra_ClausEstimateCoverage( Clu_Man_t * p )
int * pStart, * pVar2Id;
int clk = clock();
// simulate the circuit with nCombSimWords * 32 = 64K patterns
- srand( 0xAABBAABB );
+// srand( 0xAABBAABB );
+ Aig_ManRandom(1);
pComb = Fra_SmlSimulateComb( p->pAig, nCombSimWords );
// create mapping from SAT vars to node IDs
pVar2Id = ALLOC( int, p->pCnf->nVars );
diff --git a/src/aig/fra/fraHot.c b/src/aig/fra/fraHot.c
index 222f5bcc..b2156193 100644
--- a/src/aig/fra/fraHot.c
+++ b/src/aig/fra/fraHot.c
@@ -333,7 +333,8 @@ void Fra_OneHotEstimateCoverage( Fra_Man_t * p, Vec_Int_t * vOneHots )
// generate random sim-info at register outputs
vSimInfo = Vec_PtrAllocSimInfo( nRegs + 1, nSimWords );
- srand( 0xAABBAABB );
+// srand( 0xAABBAABB );
+ Aig_ManRandom(1);
for ( i = 0; i < nRegs; i++ )
{
pSim1 = Vec_PtrEntry( vSimInfo, i );
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index da7c37a3..b8cf13c5 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -120,7 +120,8 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
// set random number generator
- srand( 0xABCABC );
+// srand( 0xABCABC );
+ Aig_ManRandom(1);
// set the pointer to the manager
Aig_ManForEachObj( p->pManAig, pObj, i )
pObj->pData = p;
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 64222a47..9a500680 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -44,21 +44,20 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetime
{
Fra_Ssw_t Pars, * pPars = &Pars;
Fra_Sml_t * pSml;
- Aig_Man_t * pNew = NULL, * pTemp;
+ Aig_Man_t * pNew, * pTemp;
int nFrames, RetValue, nIter, clk, clkTotal = clock();
int fLatchCorr = 0;
// try the miter before solving
- RetValue = Fra_FraigMiterStatus( p );
- if ( RetValue == 0 || RetValue == 1 )
+ pNew = Aig_ManDup( p );
+ RetValue = Fra_FraigMiterStatus( pNew );
+ if ( RetValue >= 0 )
goto finish;
// prepare parameters
memset( pPars, 0, sizeof(Fra_Ssw_t) );
pPars->fLatchCorr = fLatchCorr;
pPars->fVerbose = fVeryVerbose;
-
- pNew = Aig_ManDup( p );
if ( fVerbose )
{
printf( "Original miter: Latches = %5d. Nodes = %6d.\n",
@@ -78,6 +77,9 @@ clk = clock();
Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
PRT( "Time", clock() - clk );
}
+ RetValue = Fra_FraigMiterStatus( pNew );
+ if ( RetValue >= 0 )
+ goto finish;
// perform phase abstraction
clk = clock();
@@ -150,6 +152,13 @@ PRT( "Time", clock() - clk );
}
}
+ if ( pNew->nRegs == 0 )
+ RetValue = Fra_FraigCec( &pNew, 0 );
+
+ RetValue = Fra_FraigMiterStatus( pNew );
+ if ( RetValue >= 0 )
+ goto finish;
+
// perform min-area retiming
if ( fRetimeRegs && pNew->nRegs )
{
@@ -262,9 +271,7 @@ PRT( "Time", clock() - clkTotal );
assert( Aig_ManRegNum(pNew) > 0 );
pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew);
pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew);
-clk = clock();
RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
-PRT( "Time", clock() - clk );
}
finish:
@@ -289,8 +296,7 @@ PRT( "Time", clock() - clkTotal );
Ioa_WriteAiger( pNew, pFileName, 0, 0 );
printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
}
- if ( pNew )
- Aig_ManStop( pNew );
+ Aig_ManStop( pNew );
return RetValue;
}
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 7de3ccdc..c9172024 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -2,4 +2,5 @@ SRC += src/aig/saig/saig_.c \
src/aig/saig/saigPhase.c \
src/aig/saig/saigRetFwd.c \
src/aig/saig/saigRetMin.c \
+ src/aig/saig/saigRetStep.c \
src/aig/saig/saigScl.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f9677cb0..7f6bb292 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -82,6 +82,8 @@ extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, in
/*=== saigRetMin.c ==========================================================*/
extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+/*=== saigRetStep.c ==========================================================*/
+extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
/*=== saigScl.c ==========================================================*/
extern void Saig_ManReportUselessRegisters( Aig_Man_t * pAig );
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index f98bb49b..f19a27b6 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -58,13 +58,13 @@ static inline int Saig_XsimAnd( int Value0, int Value1 )
}
static inline int Saig_XsimRand2()
{
- return (rand() & 1) ? SAIG_XVS1 : SAIG_XVS0;
+ return (Aig_ManRandom(0) & 1) ? SAIG_XVS1 : SAIG_XVS0;
}
static inline int Saig_XsimRand3()
{
int RetValue;
do {
- RetValue = rand() & 3;
+ RetValue = Aig_ManRandom(0) & 3;
} while ( RetValue == 0 );
return RetValue;
}
@@ -601,11 +601,11 @@ void Saig_ManAnalizeControl( Aig_Man_t * p, int Reg )
***********************************************************************/
int Saig_ManFindRegisters( Saig_Tsim_t * pTsi, int nFrames, int fIgnore, int fVerbose )
{
- int Values[256];
+ int Values[257];
unsigned * pState;
int r, i, k, Reg, Value;
int nTests = pTsi->nPrefix + 2 * pTsi->nCycle;
- assert( nFrames < 256 );
+ assert( nFrames <= 256 );
r = 0;
Vec_IntForEachEntry( pTsi->vNonXRegs, Reg, i )
{
@@ -800,6 +800,8 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
printf( "Print-out finished. Phase assignment is not performed.\n" );
else if ( nFrames < 2 )
printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
+ else if ( nFrames > 256 )
+ printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
else if ( pTsi->nCycle == 1 )
printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
else if ( pTsi->nCycle % nFrames != 0 )
@@ -859,6 +861,10 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
{
// printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
}
+ else if ( nFrames > 256 )
+ {
+// printf( "The number of frames is more than 256. Phase assignment is not performed.\n" );
+ }
else if ( pTsi->nCycle == 1 )
{
// printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 324d8867..3935db6c 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -628,6 +628,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
if ( !fBackwardOnly )
for ( i = 0; i < nMaxIters; i++ )
{
+ if ( Saig_ManRegNum(pNew) == 0 )
+ break;
vCut = Nwk_ManDeriveRetimingCut( pNew, 1, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
{
@@ -648,6 +650,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
if ( !fForwardOnly && !fInitial )
for ( i = 0; i < nMaxIters; i++ )
{
+ if ( Saig_ManRegNum(pNew) == 0 )
+ break;
vCut = Nwk_ManDeriveRetimingCut( pNew, 0, fVerbose );
if ( Vec_PtrSize(vCut) >= Aig_ManRegNum(pNew) )
{
@@ -666,6 +670,8 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
else if ( !fForwardOnly && fInitial )
for ( i = 0; i < nMaxIters; i++ )
{
+ if ( Saig_ManRegNum(pNew) == 0 )
+ break;
pCopy = Aig_ManDup( pNew );
pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
Aig_ManStop( pCopy );
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
new file mode 100644
index 00000000..e7ec3c08
--- /dev/null
+++ b/src/aig/saig/saigRetStep.c
@@ -0,0 +1,202 @@
+/**CFile****************************************************************
+
+ FileName [saigRetStep.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Implementation of retiming steps.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: saigRetStep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Performs one retiming step forward.]
+
+ Description [Returns the pointer to the register output after retiming.]
+
+ SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.]
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pFanin0, * pFanin1;
+ Aig_Obj_t * pInput0, * pInput1;
+ Aig_Obj_t * pObjNew, * pObjLi, * pObjLo;
+
+ assert( Saig_ManRegNum(p) > 0 );
+ assert( Aig_ObjIsNode(pObj) );
+
+ // get the fanins
+ pFanin0 = Aig_ObjFanin0(pObj);
+ pFanin1 = Aig_ObjFanin1(pObj);
+ // skip of they are not primary inputs
+ if ( !Aig_ObjIsPi(pFanin0) || !Aig_ObjIsPi(pFanin1) )
+ return NULL;
+
+ // skip of they are not register outputs
+ if ( !Saig_ObjIsLo(p, pFanin0) || !Saig_ObjIsLo(p, pFanin1) )
+ return NULL;
+ assert( Aig_ObjPioNum(pFanin0) > 0 );
+ assert( Aig_ObjPioNum(pFanin1) > 0 );
+
+ // get the inputs of these registers
+ pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) );
+ pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) );
+ pInput0 = Aig_ObjChild0( pInput0 );
+ pInput1 = Aig_ObjChild0( pInput1 );
+ pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
+ pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) );
+
+ // create new node
+ pObjNew = Aig_And( p, pInput0, pInput1 );
+
+ // create new register input
+ pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, pObjNew->fPhase) );
+ pObjLi->PioNum = Aig_ManPoNum(p) - 1;
+ assert( pObjLi->fPhase == 0 );
+
+ // create new register output
+ pObjLo = Aig_ObjCreatePi( p );
+ pObjLo->PioNum = Aig_ManPiNum(p) - 1;
+ p->nRegs++;
+
+ // return register output
+ return Aig_NotCond( pObjLo, pObjNew->fPhase );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs one retiming step backward.]
+
+ Description [Returns the pointer to node after retiming.]
+
+ SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.]
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Obj_t * Saig_ManRetimeNodeBwd( Aig_Man_t * p, Aig_Obj_t * pObjLo )
+{
+ Aig_Obj_t * pFanin0, * pFanin1;
+ Aig_Obj_t * pLo0New, * pLo1New;
+ Aig_Obj_t * pLi0New, * pLi1New;
+ Aig_Obj_t * pObj, * pObjNew, * pObjLi;
+ int fCompl0, fCompl1;
+
+ assert( Saig_ManRegNum(p) > 0 );
+ assert( Aig_ObjPioNum(pObjLo) > 0 );
+ assert( Saig_ObjIsLo(p, pObjLo) );
+
+ // get the corresponding latch input
+ pObjLi = Saig_ManLi( p, Aig_ObjPioNum(pObjLo) - Saig_ManPiNum(p) );
+
+ // get the node
+ pObj = Aig_ObjFanin0(pObjLi);
+ if ( !Aig_ObjIsNode(pObj) )
+ return NULL;
+
+ // get the fanins
+ pFanin0 = Aig_ObjFanin0(pObj);
+ pFanin1 = Aig_ObjFanin1(pObj);
+
+ // get the complemented attributes of the fanins
+ fCompl0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFaninC0(pObjLi);
+ fCompl1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFaninC0(pObjLi);
+
+ // create latch inputs
+ pLi0New = Aig_ObjCreatePo( p, Aig_NotCond(pFanin0, fCompl0) );
+ pLi0New->PioNum = Aig_ManPoNum(p) - 1;
+ pLi1New = Aig_ObjCreatePo( p, Aig_NotCond(pFanin1, fCompl1) );
+ pLi1New->PioNum = Aig_ManPoNum(p) - 1;
+
+ // create latch outputs
+ pLo0New = Aig_ObjCreatePi(p);
+ pLo0New->PioNum = Aig_ManPiNum(p) - 1;
+ pLo1New = Aig_ObjCreatePi(p);
+ pLo1New->PioNum = Aig_ManPiNum(p) - 1;
+ pLo0New = Aig_NotCond( pLo0New, fCompl0 );
+ pLo1New = Aig_NotCond( pLo1New, fCompl1 );
+ p->nRegs += 2;
+
+ // create node
+ pObjNew = Aig_And( p, pLo0New, pLo1New );
+// assert( pObjNew->fPhase == 0 );
+ return pObjNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs the given number of retiming steps.]
+
+ Description [Returns the pointer to node after retiming.]
+
+ SideEffects [Remember to run Aig_ManSetPioNumbers() in advance.]
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
+{
+ Aig_Obj_t * pObj, * pObjNew;
+ int RetValue, s, i;
+ Aig_ManSetPioNumbers( p );
+ Aig_ManFanoutStart( p );
+ if ( fForward )
+ {
+ for ( s = 0; s < nSteps; s++ )
+ {
+ Aig_ManForEachNode( p, pObj, i )
+ {
+ pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
+ if ( pObjNew == NULL )
+ continue;
+ Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+ break;
+ }
+ }
+ }
+ else
+ {
+ for ( s = 0; s < nSteps; s++ )
+ {
+ Saig_ManForEachLo( p, pObj, i )
+ {
+ pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
+ if ( pObjNew == NULL )
+ continue;
+ Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+ break;
+ }
+ }
+ }
+ RetValue = Aig_ManCleanup( p );
+ assert( RetValue == 0 );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c
index 40d1dcad..3bac7316 100644
--- a/src/base/abc/abcShow.c
+++ b/src/base/abc/abcShow.c
@@ -24,7 +24,7 @@
#include "abc.h"
#include "main.h"
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9b3ec291..d3ac7669 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -500,6 +500,11 @@ void Abc_Init( Abc_Frame_t * pAbc )
extern Bdc_ManDecomposeTest( unsigned uTruth, int nVars );
// Bdc_ManDecomposeTest( 0x0f0f0f0f, 3 );
}
+
+ {
+// extern void Aig_ManRandomTest1();
+// Aig_ManRandomTest1();
+ }
}
/**Function*************************************************************
@@ -7253,7 +7258,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// extern void Abc_NtkDarTestBlif( char * pFileName );
// extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
// extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
- extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
+// extern Abc_Ntk_t * Abc_NtkNtkTest( Abc_Ntk_t * pNtk, If_Lib_t * pLutLib );
+ extern Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose );
@@ -7440,7 +7446,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Abc_NtkDarPartition( pNtk );
- pNtkRes = Abc_NtkNtkTest( pNtk, Abc_FrameReadLibLut() );
+ pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -17020,6 +17026,9 @@ int Abc_CommandAbc8Sweep( Abc_Frame_t * pAbc, int argc, char ** argv )
int fVerbose;
int c;
extern int Ntl_ManSweep( void * p, int fVerbose );
+ extern void * Ntl_ManInsertNtk( void * p, void * pNtk );
+ extern Aig_Man_t * Ntl_ManExtract( void * p );
+ extern void * Ntl_ManExtractNwk( void * p, Aig_Man_t * pAig, Tim_Man_t * pManTime );
// set defaults
fMapped = 0;
@@ -17332,12 +17341,13 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
// set defaults
- nFrames = 16;
- fRetimeFirst = 0;
- fRetimeRegs = 0;
- fFraiging = 1;
- fVerbose = 0;
- fVeryVerbose = 0;
+ nFrames = 8;
+ fPhaseAbstract = 0;
+ fRetimeFirst = 0;
+ fRetimeRegs = 0;
+ fFraiging = 1;
+ fVerbose = 0;
+ fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
{
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 88435e3f..329bccf8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -20,6 +20,7 @@
#include "abc.h"
#include "aig.h"
+#include "saig.h"
#include "dar.h"
#include "cnf.h"
#include "fra.h"
@@ -1538,6 +1539,41 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwa
SeeAlso []
***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Abc_Ntk_t * pNtkAig;
+ Aig_Man_t * pMan;
+ assert( Abc_NtkIsStrash(pNtk) );
+ pMan = Abc_NtkToDar( pNtk, 0, 1 );
+ if ( pMan == NULL )
+ return NULL;
+ if ( pMan->vFlopNums )
+ Vec_IntFree( pMan->vFlopNums );
+ pMan->vFlopNums = NULL;
+
+ pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
+ pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
+
+ Aig_ManPrintStats(pMan);
+ Saig_ManRetimeSteps( pMan, 1, 0 );
+ Aig_ManPrintStats(pMan);
+
+ pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
+ Aig_ManStop( pMan );
+ return pNtkAig;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
{
/*
diff --git a/src/base/abci/abcDress.c b/src/base/abci/abcDress.c
index f8182532..f262a5d0 100644
--- a/src/base/abci/abcDress.c
+++ b/src/base/abci/abcDress.c
@@ -19,7 +19,7 @@
***********************************************************************/
#include "abc.h"
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 316dd8ad..313ae0ed 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1085,7 +1085,7 @@ usage:
#ifdef WIN32
-#include <io.h>
+#include <direct.h>
// these structures are defined in <io.h> but are for some reason invisible
typedef unsigned long _fsize_t; // Could be 64 bits for Win32
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 6b802bf1..6efa8b67 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "mainInt.h"
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.h b/src/base/io/ioAbc.h
index eea76efe..e62cc168 100644
--- a/src/base/io/io.h
+++ b/src/base/io/ioAbc.h
@@ -1,6 +1,6 @@
/**CFile****************************************************************
- FileName [io.h]
+ FileName [ioAbc.h]
SystemName [ABC: Logic synthesis and verification system.]
@@ -14,7 +14,7 @@
Date [Ver. 1.0. Started - June 20, 2005.]
- Revision [$Id: io.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+ Revision [$Id: ioAbc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
***********************************************************************/
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index 4820bced..3739205d 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -19,7 +19,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
@@ -327,7 +327,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
}
// read the name of the model if given
- if ( *pCur == 'c' )
+ if ( *pCur == 'c' && pCur < pContents + nFileSize )
{
if ( !strncmp( pCur + 2, ".model", 6 ) )
{
diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c
index 8dce54af..13f644cc 100644
--- a/src/base/io/ioReadBaf.c
+++ b/src/base/io/ioReadBaf.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c
index 007147bc..0742ec1f 100644
--- a/src/base/io/ioReadBench.c
+++ b/src/base/io/ioReadBench.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c
index ffa25c7f..68a0bc35 100644
--- a/src/base/io/ioReadBlif.c
+++ b/src/base/io/ioReadBlif.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "main.h"
#include "mio.h"
diff --git a/src/base/io/ioReadBlifMv.c b/src/base/io/ioReadBlifMv.c
index 84378024..68602e63 100644
--- a/src/base/io/ioReadBlifMv.c
+++ b/src/base/io/ioReadBlifMv.c
@@ -21,7 +21,7 @@
#include "abc.h"
#include "extra.h"
#include "vecPtr.h"
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadDsd.c b/src/base/io/ioReadDsd.c
index 1ab726e5..482b5d06 100644
--- a/src/base/io/ioReadDsd.c
+++ b/src/base/io/ioReadDsd.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c
index 188e5b8c..bea9bf69 100644
--- a/src/base/io/ioReadEdif.c
+++ b/src/base/io/ioReadEdif.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c
index e04f2b1a..6a1360d0 100644
--- a/src/base/io/ioReadEqn.c
+++ b/src/base/io/ioReadEqn.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadPla.c b/src/base/io/ioReadPla.c
index 288c3704..cbee81ef 100644
--- a/src/base/io/ioReadPla.c
+++ b/src/base/io/ioReadPla.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c
index c64e330c..9847c2da 100644
--- a/src/base/io/ioReadVerilog.c
+++ b/src/base/io/ioReadVerilog.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c
index 51a00274..37d57f30 100644
--- a/src/base/io/ioUtil.c
+++ b/src/base/io/ioUtil.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c
index 758e5335..fb107e77 100644
--- a/src/base/io/ioWriteAiger.c
+++ b/src/base/io/ioWriteAiger.c
@@ -19,7 +19,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteBaf.c b/src/base/io/ioWriteBaf.c
index fc0229a4..33487041 100644
--- a/src/base/io/ioWriteBaf.c
+++ b/src/base/io/ioWriteBaf.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteBench.c b/src/base/io/ioWriteBench.c
index df4a6259..147976da 100644
--- a/src/base/io/ioWriteBench.c
+++ b/src/base/io/ioWriteBench.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index c0c29d65..a0105a6b 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "main.h"
#include "mio.h"
diff --git a/src/base/io/ioWriteBlifMv.c b/src/base/io/ioWriteBlifMv.c
index 775a2e07..86891fee 100644
--- a/src/base/io/ioWriteBlifMv.c
+++ b/src/base/io/ioWriteBlifMv.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "main.h"
#include "mio.h"
diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c
index e1b2d956..3df189d1 100644
--- a/src/base/io/ioWriteCnf.c
+++ b/src/base/io/ioWriteCnf.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "satSolver.h"
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 8ae3cc42..b8ca6f67 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "main.h"
#include "mio.h"
diff --git a/src/base/io/ioWriteEqn.c b/src/base/io/ioWriteEqn.c
index 95c54577..94c6e032 100644
--- a/src/base/io/ioWriteEqn.c
+++ b/src/base/io/ioWriteEqn.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteGml.c b/src/base/io/ioWriteGml.c
index dc897300..d84e5f67 100644
--- a/src/base/io/ioWriteGml.c
+++ b/src/base/io/ioWriteGml.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c
index 71af7c53..c06b39d7 100644
--- a/src/base/io/ioWriteList.c
+++ b/src/base/io/ioWriteList.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
/*
-------- Original Message --------
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index b119751c..4b316416 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c
index 9e71e3e4..c704c6a1 100644
--- a/src/base/io/ioWriteVerilog.c
+++ b/src/base/io/ioWriteVerilog.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
#include "main.h"
#include "mio.h"
diff --git a/src/base/io/io_.c b/src/base/io/io_.c
index 62dd60e5..b24d1299 100644
--- a/src/base/io/io_.c
+++ b/src/base/io/io_.c
@@ -18,7 +18,7 @@
***********************************************************************/
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
diff --git a/src/base/main/main.h b/src/base/main/main.h
index 4433a8b4..b5cc0dfe 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -52,7 +52,7 @@ typedef struct Abc_Frame_t_ Abc_Frame_t;
// core packages
#include "abc.h"
#include "cmd.h"
-#include "io.h"
+#include "ioAbc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
diff --git a/src/opt/fret/fretInit.c b/src/opt/fret/fretInit.c
index 47d338cb..bf249035 100644
--- a/src/opt/fret/fretInit.c
+++ b/src/opt/fret/fretInit.c
@@ -20,7 +20,7 @@
#include "abc.h"
#include "vec.h"
-#include "io.h"
+#include "ioAbc.h"
#include "fretime.h"
#include "mio.h"
#include "hop.h"