summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/fra/fra.h3
-rw-r--r--src/aig/fra/fraSim.c147
-rw-r--r--src/aig/ntl/ntlCheck.c3
-rw-r--r--src/aig/ntl/ntlReadBlif.c38
-rw-r--r--src/aig/saig/saig.h1
-rw-r--r--src/aig/saig/saigBmc.c6
-rw-r--r--src/aig/saig/saigHaig.c115
-rw-r--r--src/aig/saig/saigRetStep.c8
8 files changed, 221 insertions, 100 deletions
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7cb846fa..7549dfca 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -370,8 +370,9 @@ extern Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
extern Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p );
extern Fra_Cex_t * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
extern void Fra_SmlFreeCounterExample( Fra_Cex_t * p );
-extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
extern Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut );
+extern int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p );
+extern int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p );
#ifdef __cplusplus
}
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index a8de5e37..00a35fcd 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -846,44 +846,6 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
/**Function*************************************************************
- Synopsis [Resimulates the counter-example.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
-{
- Fra_Sml_t * pSml;
- Aig_Obj_t * pObj;
- int RetValue, i, k, iBit;
- assert( Aig_ManRegNum(pAig) > 0 );
- assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
- // start a new sequential simulator
- pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
- // assign simulation info for the registers
- iBit = 0;
- Aig_ManForEachLoSeq( pAig, pObj, i )
- Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
- // assign simulation info for the primary inputs
- for ( i = 0; i <= p->iFrame; i++ )
- Aig_ManForEachPiSeq( pAig, pObj, k )
- Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
- assert( iBit == p->nBits );
- // run random simulation
- Fra_SmlSimulateOne( pSml );
- // check if the given output has failed
- RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
- Fra_SmlStop( pSml );
- return RetValue;
-}
-
-
-/**Function*************************************************************
-
Synopsis [Allocates a counter-example.]
Description []
@@ -1082,6 +1044,115 @@ Fra_Cex_t * Fra_SmlTrivCounterExample( Aig_Man_t * pAig, int iFrameOut )
return pCex;
}
+/**Function*************************************************************
+
+ Synopsis [Resimulates the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SmlRunCounterExample( Aig_Man_t * pAig, Fra_Cex_t * p )
+{
+ Fra_Sml_t * pSml;
+ Aig_Obj_t * pObj;
+ int RetValue, i, k, iBit;
+ assert( Aig_ManRegNum(pAig) > 0 );
+ assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
+ // start a new sequential simulator
+ pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
+ // assign simulation info for the registers
+ iBit = 0;
+ Aig_ManForEachLoSeq( pAig, pObj, i )
+ Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+ // assign simulation info for the primary inputs
+ for ( i = 0; i <= p->iFrame; i++ )
+ Aig_ManForEachPiSeq( pAig, pObj, k )
+ Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+ assert( iBit == p->nBits );
+ // run random simulation
+ Fra_SmlSimulateOne( pSml );
+ // check if the given output has failed
+ RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
+ Fra_SmlStop( pSml );
+ return RetValue;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resimulates the counter-example.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Fra_SmlWriteCounterExample( FILE * pFile, Aig_Man_t * pAig, Fra_Cex_t * p )
+{
+ Fra_Sml_t * pSml;
+ Aig_Obj_t * pObj;
+ int RetValue, i, k, iBit;
+ unsigned * pSims;
+ assert( Aig_ManRegNum(pAig) > 0 );
+ assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
+ // start a new sequential simulator
+ pSml = Fra_SmlStart( pAig, 0, p->iFrame+1, 1 );
+ // assign simulation info for the registers
+ iBit = 0;
+ Aig_ManForEachLoSeq( pAig, pObj, i )
+// Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), 0 );
+ Fra_SmlAssignConst( pSml, pObj, 0, 0 );
+ // assign simulation info for the primary inputs
+ iBit = p->nRegs;
+ for ( i = 0; i <= p->iFrame; i++ )
+ Aig_ManForEachPiSeq( pAig, pObj, k )
+ Fra_SmlAssignConst( pSml, pObj, Aig_InfoHasBit(p->pData, iBit++), i );
+ assert( iBit == p->nBits );
+ // run random simulation
+ Fra_SmlSimulateOne( pSml );
+ // check if the given output has failed
+ RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, p->iPo) );
+
+ // write the output file
+ fprintf( pFile, "1\n" );
+ for ( i = 0; i <= p->iFrame; i++ )
+ {
+ Aig_ManForEachLoSeq( pAig, pObj, k )
+ {
+ pSims = Fra_ObjSim(pSml, pObj->Id);
+ fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+ }
+ fprintf( pFile, " " );
+ Aig_ManForEachPiSeq( pAig, pObj, k )
+ {
+ pSims = Fra_ObjSim(pSml, pObj->Id);
+ fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+ }
+ fprintf( pFile, " " );
+ Aig_ManForEachPoSeq( pAig, pObj, k )
+ {
+ pSims = Fra_ObjSim(pSml, pObj->Id);
+ fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+ }
+ fprintf( pFile, " " );
+ Aig_ManForEachLiSeq( pAig, pObj, k )
+ {
+ pSims = Fra_ObjSim(pSml, pObj->Id);
+ fprintf( pFile, "%d", (int)(pSims[i] != 0) );
+ }
+ fprintf( pFile, "\n" );
+ }
+
+ Fra_SmlStop( pSml );
+ return RetValue;
+}
+
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlCheck.c b/src/aig/ntl/ntlCheck.c
index c5c62433..d5100312 100644
--- a/src/aig/ntl/ntlCheck.c
+++ b/src/aig/ntl/ntlCheck.c
@@ -123,8 +123,11 @@ int Ntl_ManCheck( Ntl_Man_t * pMan )
}
// check models
Ntl_ManForEachModel( pMan, pMod1, i )
+ {
if ( !Ntl_ModelCheck( pMod1 ) )
fStatus = 0;
+ break;
+ }
return fStatus;
}
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index 3574b61e..a291f8a0 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -534,6 +534,18 @@ static void Ioa_ReadReadPreparse( Ioa_ReadMan_t * p )
fprintf( stdout, "Line %d: Skipping EXDC network.\n", Ioa_ReadGetLine(p, pCur) );
break;
}
+ else if ( !strncmp(pCur, "no_merge", 8) )
+ {
+ }
+ else if ( !strncmp(pCur, "attribute", 9) )
+ {
+ }
+ else if ( !strncmp(pCur, "input_required", 14) )
+ {
+ }
+ else if ( !strncmp(pCur, "output_arrival", 14) )
+ {
+ }
else
{
pCur--;
@@ -682,7 +694,8 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
char * pToken;
Ioa_ReadSplitIntoTokens( vTokens, pLine, '\0' );
pToken = Vec_PtrEntry( vTokens, 0 );
- assert( !strcmp(pToken, "attrib") );
+ assert( !strncmp(pToken, "attrib", 6) );
+/*
if ( Vec_PtrSize(vTokens) != 2 )
{
sprintf( p->pMan->sError, "Line %d: The number of entries (%d) in .attrib line is different from two.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrSize(vTokens) );
@@ -695,6 +708,7 @@ static int Ioa_ReadParseLineAttrib( Ioa_ReadMod_t * p, char * pLine )
sprintf( p->pMan->sError, "Line %d: Unknown attribute (%s) in the .attrib line of model %s.", Ioa_ReadGetLine(p->pMan, pToken), Vec_PtrEntry(vTokens, 1), p->pNtk->pName );
return 0;
}
+*/
return 1;
}
@@ -864,12 +878,28 @@ static int Ioa_ReadParseLineSubckt( Ioa_ReadMod_t * p, char * pLine )
sprintf( p->pMan->sError, "Line %d: Cannot find the model for subcircuit %s.", Ioa_ReadGetLine(p->pMan, pToken), pName );
return 0;
}
-
+/*
+ // temporary fix for splitting the .subckt line
+ if ( nEquals < Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
+ {
+ Vec_Ptr_t * vTokens2 = Vec_PtrAlloc( 10 );
+ // get one additional token
+ pToken = Vec_PtrEntry( vTokens, Vec_PtrSize(vTokens) - 1 );
+ for ( ; *pToken; pToken++ );
+ for ( ; *pToken == 0; pToken++ );
+ Ioa_ReadSplitIntoTokensAndClear( vTokens2, pToken, '\0', '=' );
+// assert( Vec_PtrSize( vTokens2 ) == 2 );
+ Vec_PtrForEachEntry( vTokens2, pToken, i )
+ Vec_PtrPush( vTokens, pToken );
+ nEquals += Vec_PtrSize(vTokens2)/2;
+ Vec_PtrFree( vTokens2 );
+ }
+*/
// check if the number of tokens is correct
if ( nEquals != Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) )
{
- sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt differs from the sum of PIs and POs of the model (%d).",
- Ioa_ReadGetLine(p->pMan, pToken), nEquals, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
+ sprintf( p->pMan->sError, "Line %d: The number of ports (%d) in .subckt %s differs from the sum of PIs and POs of the model (%d).",
+ Ioa_ReadGetLine(p->pMan, pToken), nEquals, pName, Ntl_ModelPiNum(pModel) + Ntl_ModelPoNum(pModel) );
return 0;
}
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 49d3f5ef..67f38758 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -89,6 +89,7 @@ extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int
/*=== saigPhase.c ==========================================================*/
extern Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
/*=== saigRetFwd.c ==========================================================*/
+extern void Saig_ManMarkAutonomous( Aig_Man_t * p );
extern Aig_Man_t * Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
/*=== saigRetMin.c ==========================================================*/
extern Aig_Man_t * Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 2d5af2d3..32b2d186 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -191,7 +191,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else
pFrames = Saig_ManFramesBmc( pAig, nFrames );
- *piFrame = nFrames;
+ if ( piFrame )
+ *piFrame = nFrames;
if ( fVerbose )
{
printf( "AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n",
@@ -281,7 +282,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else
{
- *piFrame = i / Saig_ManPoNum(pAig);
+ if ( piFrame )
+ *piFrame = i / Saig_ManPoNum(pAig);
RetValue = -1;
break;
}
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index 4250ca79..8a75ae1f 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -195,7 +195,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
SeeAlso []
***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth )
{
int nBTLimit = 0;
Aig_Man_t * pFrames, * pTemp;
@@ -203,7 +203,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n
sat_solver * pSat;
Aig_Obj_t * pObj1, * pObj2;
int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
- int clk = clock();
+ int clk = clock(), clkVerif;
nOvers = Aig_ManMapHaigNodes( pHaig );
@@ -226,57 +226,6 @@ clk = clock();
// pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
-/*
- // print the statistic into a file
- {
- FILE * pTable;
- Aig_Man_t * pTemp, * pHaig2;
-
- pHaig2 = pAig->pManHaig;
- pAig->pManHaig = NULL;
- pTemp = Aig_ManDupDfs( pAig );
- pAig->pManHaig = pHaig2;
-
- Aig_ManSeqCleanup( pTemp );
-
- pTable = fopen( "stats.txt", "a+" );
- fprintf( pTable, "%s ", p->pName );
- fprintf( pTable, "%d ", Saig_ManPiNum(p) );
- fprintf( pTable, "%d ", Saig_ManPoNum(p) );
-
- fprintf( pTable, "%d ", Saig_ManRegNum(p) );
- fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
-
- fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
- fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
-
- fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
- fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
- fprintf( pTable, "\n" );
- fclose( pTable );
-
-
- pTable = fopen( "stats2.txt", "a+" );
- fprintf( pTable, "%s ", p->pSpec );
- fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
- fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
-
- fprintf( pTable, "%d ", pCnf->nVars );
- fprintf( pTable, "%d ", pCnf->nClauses );
- fprintf( pTable, "%d ", pCnf->nLiterals );
-
- fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
- fprintf( pTable, "%d ", pFrames->nAsserts/2 );
- fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
- fprintf( pTable, "\n" );
- fclose( pTable );
-
- Aig_ManStop( pTemp );
- }
-*/
// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
@@ -375,11 +324,66 @@ clk = clock();
}
printf( " \r" );
PRT( "Solving ", clock() - clk );
+clkVerif = clock() - clk;
if ( Counter )
printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
else
printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
+ // print the statistic into a file
+ {
+ FILE * pTable;
+ Aig_Man_t * pTemp, * pHaig2;
+
+ pHaig2 = pAig->pManHaig;
+ pAig->pManHaig = NULL;
+ pTemp = Aig_ManDupDfs( pAig );
+ pAig->pManHaig = pHaig2;
+
+ Aig_ManSeqCleanup( pTemp );
+
+ pTable = fopen( "stats.txt", "a+" );
+ fprintf( pTable, "%s ", p->pName );
+ fprintf( pTable, "%d ", Saig_ManPiNum(p) );
+ fprintf( pTable, "%d ", Saig_ManPoNum(p) );
+
+ fprintf( pTable, "%d ", Saig_ManRegNum(p) );
+ fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
+ fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
+
+ fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
+ fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
+ fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
+
+ fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
+ fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
+ fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
+
+ fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
+ fprintf( pTable, "\n" );
+ fclose( pTable );
+
+
+ pTable = fopen( "stats2.txt", "a+" );
+ fprintf( pTable, "%s ", p->pName );
+ fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
+ fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
+
+ fprintf( pTable, "%d ", pCnf->nVars );
+ fprintf( pTable, "%d ", pCnf->nClauses );
+ fprintf( pTable, "%d ", pCnf->nLiterals );
+
+ fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
+ fprintf( pTable, "%d ", pFrames->nAsserts/2 );
+ fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
+
+ fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
+ fprintf( pTable, "\n" );
+ fclose( pTable );
+
+ Aig_ManStop( pTemp );
+ }
+
// clean up
Aig_ManStop( pFrames );
Cnf_DataFree( pCnf );
@@ -617,7 +621,7 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti
Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
Aig_Man_t * pNew, * pTemp;
Aig_Obj_t * pObj;
- int i, k, nStepsReal, clk = clock();
+ int i, k, nStepsReal, clk = clock(), clkSynth;
Dar_ManDefaultRwrParams( pParsRwr );
clk = clock();
@@ -679,6 +683,7 @@ clk = clock();
}
}
PRT( "Synthesis time ", clock() - clk );
+clkSynth = clock() - clk;
// use the haig for verification
// Aig_ManAntiCleanup( pNew->pManHaig );
@@ -699,7 +704,7 @@ PRT( "Synthesis time ", clock() - clk );
}
else
{
- if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
+ if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
printf( "Constructing SAT solver has failed.\n" );
}
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index fe726702..e2502761 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -62,6 +62,10 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
assert( Aig_ObjPioNum(pFanin0) > 0 );
assert( Aig_ObjPioNum(pFanin1) > 0 );
+ // skip latch guns
+ if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) )
+ return NULL;
+
// 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) );
@@ -90,6 +94,9 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
pObjLo->PioNum = Aig_ManPiNum(p) - 1;
p->nRegs++;
+ // make sure the register is retimable.
+ Aig_ObjSetTravIdCurrent(p, pObjLo);
+
//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n",
// pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
@@ -177,6 +184,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
p->fCreatePios = 1;
if ( fForward )
{
+ Saig_ManMarkAutonomous( p );
for ( s = 0; s < nSteps; s++ )
{
Aig_ManForEachNode( p, pObj, i )
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-16 12:08:34 +0000