summaryrefslogtreecommitdiffstats
path: root/src/aig/saig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/saig')
-rw-r--r--src/aig/saig/module.make1
-rw-r--r--src/aig/saig/saig.h2
-rw-r--r--src/aig/saig/saigBmc.c29
-rw-r--r--src/aig/saig/saigHaig.c472
-rw-r--r--src/aig/saig/saigPhase.c2
-rw-r--r--src/aig/saig/saigRetMin.c4
-rw-r--r--src/aig/saig/saigRetStep.c19
7 files changed, 511 insertions, 18 deletions
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index ea122bbf..50d6db49 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,6 @@
SRC += src/aig/saig/saigBmc.c \
src/aig/saig/saigCone.c \
+ src/aig/saig/saigHaig.c \
src/aig/saig/saigInter.c \
src/aig/saig/saigIoa.c \
src/aig/saig/saigPhase.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index c8efab40..8ec680b8 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -79,6 +79,8 @@ static inline int Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj ) {
extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
/*=== saigCone.c ==========================================================*/
extern void Saig_ManPrintCones( Aig_Man_t * p );
+/*=== saigHaig.c ==========================================================*/
+extern void Saig_ManHaigRecord( Aig_Man_t * p );
/*=== saigIoa.c ==========================================================*/
extern void Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
extern Aig_Man_t * Saig_ManReadBlif( char * pFileName );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 952094ce..2d5af2d3 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -145,11 +145,11 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
{
pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
- if ( Counter >= nSizeMax )
- {
- Aig_ManCleanup( pFrames );
- return pFrames;
- }
+ }
+ if ( Counter >= nSizeMax )
+ {
+ Aig_ManCleanup( pFrames );
+ return pFrames;
}
if ( f == nFrames - 1 )
break;
@@ -201,6 +201,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames),
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
+ fflush( stdout );
}
// rewrite the timeframes
if ( fRewrite )
@@ -214,6 +215,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
printf( "Time-frames after rewriting: Node = %6d. Lev = %5d. ",
Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
PRT( "Time", clock() - clk );
+ fflush( stdout );
}
}
// create the SAT solver
@@ -230,15 +232,20 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
{
printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
PRT( "Time", clock() - clk );
+ fflush( stdout );
}
status = sat_solver_simplify(pSat);
if ( status == 0 )
{
if ( fVerbose )
+ {
printf( "The BMC problem is trivially UNSAT\n" );
+ fflush( stdout );
+ }
}
else
{
+ int clkPart = clock();
Aig_ManForEachPo( pFrames, pObj, i )
{
Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
@@ -247,12 +254,14 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
clk = clock();
status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
- if ( fVerbose )
+ if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
{
- printf( "Solved output %2d of frame %3d. ",
- i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+ printf( "Solved %2d outputs of frame %3d. ",
+ Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
- PRT( "Time", clock() - clk );
+ PRT( "Time", clock() - clkPart );
+ clkPart = clock();
+ fflush( stdout );
}
if ( status == l_False )
{
@@ -272,7 +281,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
}
else
{
- *piFrame = i;
+ *piFrame = i / Saig_ManPoNum(pAig);
RetValue = -1;
break;
}
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
new file mode 100644
index 00000000..64f4e943
--- /dev/null
+++ b/src/aig/saig/saigHaig.c
@@ -0,0 +1,472 @@
+/**CFile****************************************************************
+
+ FileName [saigHaig.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Sequential AIG package.]
+
+ Synopsis [Experiments with history AIG recording.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - April 28, 2007.]
+
+ Revision [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "satSolver.h"
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the inductive case with speculative reduction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
+{
+ Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+ // skip nodes without representative
+ pObjRepr = pObj->pHaig;
+ if ( pObjRepr == NULL )
+ return;
+ assert( pObjRepr->Id < pObj->Id );
+ // get the new node
+ pObjNew = pObj->pData;
+ // get the new node of the representative
+ pObjReprNew = pObjRepr->pData;
+ // if this is the same node, no need to add constraints
+ if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+ return;
+ // these are different nodes - perform speculative reduction
+ pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+ // set the new node
+ pObj->pData = pObjNew2;
+ // add the constraint
+ pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
+ pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+ assert( Aig_ObjPhaseReal(pMiter) == 1 );
+ Aig_ObjCreatePo( pFrames, pMiter );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Prepares the inductive case with speculative reduction.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
+{
+ Aig_Man_t * pFrames;
+ Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+ int i, f, nAssumptions = 0;
+ assert( nFrames == 1 || nFrames == 2 );
+ assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
+ // start AIG manager for timeframes
+ pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
+ pFrames->pName = Aig_UtilStrsav( pHaig->pName );
+ pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
+ // map the constant node
+ Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
+ // create variables for register outputs
+ Saig_ManForEachLo( pHaig, pObj, i )
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ // add timeframes
+ Aig_ManSetPioNumbers( pHaig );
+ for ( f = 0; f < nFrames; f++ )
+ {
+ Aig_ManForEachObj( pHaig, pObj, i )
+ {
+ if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) )
+ continue;
+ if ( Saig_ObjIsPi(pHaig, pObj) )
+ {
+ pObj->pData = Aig_ObjCreatePi( pFrames );
+ continue;
+ }
+ if ( Saig_ObjIsLo(pHaig, pObj) )
+ {
+ Aig_ManHaigSpeculate( pFrames, pObj );
+ continue;
+ }
+ if ( Aig_ObjIsNode(pObj) )
+ {
+ pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+ Aig_ManHaigSpeculate( pFrames, pObj );
+ continue;
+ }
+ assert( 0 );
+ }
+ if ( f == nFrames - 2 )
+ nAssumptions = Aig_ManPoNum(pFrames);
+ if ( f == nFrames - 1 )
+ break;
+ // save register inputs
+ Saig_ManForEachLi( pHaig, pObj, i )
+ pObj->pData = Aig_ObjChild0Copy(pObj);
+ // transfer to register outputs
+ Saig_ManForEachLiLo( pHaig, pObjLi, pObjLo, i )
+ pObjLo->pData = pObjLi->pData;
+ }
+ Aig_ManCleanup( pFrames );
+ pFrames->nAsserts = Aig_ManPoNum(pFrames) - nAssumptions;
+ Aig_ManSetRegNum( pFrames, 0 );
+ return pFrames;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+ int nBTLimit = 0;
+ Aig_Man_t * pFrames;
+ Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+ Aig_Obj_t * pObj;
+ int i, Lit, RetValue, Counter;
+ int clk = clock();
+
+ // create time frames with speculative reduction and convert them into CNF
+clk = clock();
+ pFrames = Aig_ManHaigFrames( pHaig, nFrames );
+Aig_ManShow( pFrames, 0, NULL );
+
+ printf( "AIG: " );
+ Aig_ManPrintStats( pAig );
+ printf( "HAIG: " );
+ Aig_ManPrintStats( pHaig );
+ printf( "Frames: " );
+ Aig_ManPrintStats( pFrames );
+ printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n",
+ Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts );
+ pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts );
+PRT( "Preparation", clock() - clk );
+
+// pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+ Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+ Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+ // create the SAT solver to be used for this problem
+ pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+ if ( pSat == NULL )
+ {
+ printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+ return -1;
+ }
+
+ // solve each output
+clk = clock();
+ if ( pFrames->nAsserts == 0 )
+ {
+ RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue != l_False )
+ printf( "SAT solver is wrong\n" );
+ }
+ else
+ {
+ Counter = 0;
+ Aig_ManForEachPo( pFrames, pObj, i )
+ {
+ if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+ continue;
+ Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
+ RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue != l_False )
+ Counter++;
+ }
+PRT( "Solving ", clock() - clk );
+ if ( Counter )
+ printf( "Verification failed for %d classes.\n", Counter );
+ else
+ printf( "Verification is successful.\n" );
+ }
+
+ // clean up
+ Aig_ManStop( pFrames );
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+ int nBTLimit = 0;
+ Cnf_Dat_t * pCnf;
+ sat_solver * pSat;
+ Aig_Obj_t * pObj, * pRepr;
+ int i, RetValue, Counter, Lits[2];
+ int nClasses = 0;
+ int clk = clock();
+
+ assert( nFrames == 1 || nFrames == 2 );
+
+clk = clock();
+ pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
+ // create the SAT solver to be used for this problem
+ pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
+ if ( pSat == NULL )
+ {
+ printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+ return -1;
+ }
+
+ if ( nFrames == 2 )
+ {
+ // add clauses for the first frame
+ Aig_ManForEachObj( pHaig, pObj, i )
+ {
+ pRepr = pObj->pHaig;
+ if ( pRepr == NULL )
+ continue;
+ if ( pRepr->fPhase ^ pObj->fPhase )
+ {
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
+ Lits[0]++;
+ Lits[1]++;
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
+ }
+ else
+ {
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
+ Lits[0]++;
+ Lits[1]--;
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+ {
+ sat_solver_delete( pSat );
+ return 0;
+ }
+ }
+ }
+
+ // add clauses for the next timeframe
+ {
+ int nLitsAll = 2 * pCnf->nVars;
+ int * pLits = pCnf->pClauses[0];
+ for ( i = 0; i < pCnf->nLiterals; i++ )
+ pLits[i] += nLitsAll;
+ }
+ }
+PRT( "Preparation", clock() - clk );
+
+
+ // check in the second timeframe
+clk = clock();
+ Counter = 0;
+ nClasses = 0;
+ Aig_ManForEachObj( pHaig, pObj, i )
+ {
+ pRepr = pObj->pHaig;
+ if ( pRepr == NULL )
+ continue;
+ nClasses++;
+ if ( pRepr->fPhase ^ pObj->fPhase )
+ {
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+
+ RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue != l_False )
+ Counter++;
+
+ Lits[0]++;
+ Lits[1]++;
+
+ RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue != l_False )
+ Counter++;
+ }
+ else
+ {
+ Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+ Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+
+ RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue != l_False )
+ Counter++;
+
+ Lits[0]++;
+ Lits[1]--;
+
+ RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+ if ( RetValue != l_False )
+ Counter++;
+ }
+ }
+PRT( "Solving ", clock() - clk );
+ if ( Counter )
+ printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses );
+ else
+ printf( "Verification is successful for all %d classes.\n", nClasses );
+
+ Cnf_DataFree( pCnf );
+ sat_solver_delete( pSat );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Saig_ManHaigRecord( Aig_Man_t * p )
+{
+ extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
+ int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 );
+ Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+ Aig_Man_t * pNew, * pTemp;
+ Aig_Obj_t * pObj;
+ int i;
+ Dar_ManDefaultRwrParams( pParsRwr );
+ // duplicate this manager
+ pNew = Aig_ManDupSimple( p );
+
+ // create its history AIG
+ pNew->pManHaig = Aig_ManDupSimple( pNew );
+ Aig_ManForEachObj( pNew, pObj, i )
+ pObj->pHaig = pObj->pData;
+ // remove structural hashing table
+ Aig_TableClear( pNew->pManHaig );
+
+ // perform retiming
+ if ( fUseRetiming )
+ {
+/*
+ // perform balancing
+ pNew = Dar_ManBalance( pTemp = pNew, 0 );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+
+ // perform rewriting
+ Dar_ManRewrite( pNew, pParsRwr );
+ pNew = Aig_ManDupDfs( pTemp = pNew );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+*/
+ // perform retiming
+ Saig_ManRetimeSteps( pNew, 1000, 1 );
+ pNew = Aig_ManDupSimpleDfs( pTemp = pNew );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+
+ // perform balancing
+ pNew = Dar_ManBalance( pTemp = pNew, 0 );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+
+ // perform rewriting
+ Dar_ManRewrite( pNew, pParsRwr );
+ pNew = Aig_ManDupDfs( pTemp = pNew );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+ }
+ else
+ {
+ // perform balancing
+ pNew = Dar_ManBalance( pTemp = pNew, 0 );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+/*
+ // perform rewriting
+ Dar_ManRewrite( pNew, pParsRwr );
+ pNew = Aig_ManDupDfs( pTemp = pNew );
+ assert( pNew->pManHaig != NULL );
+ assert( pTemp->pManHaig == NULL );
+ Aig_ManStop( pTemp );
+*/
+ }
+
+ // use the haig for verification
+ Aig_ManAntiCleanup( pNew->pManHaig );
+ Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
+//Aig_ManShow( pNew->pManHaig, 0, NULL );
+
+ printf( "AIG: " );
+ Aig_ManPrintStats( pNew );
+ printf( "HAIG: " );
+ Aig_ManPrintStats( pNew->pManHaig );
+
+ if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) )
+ printf( "Constructing SAT solver has failed.\n" );
+
+ // cleanup
+ Aig_ManStop( pNew->pManHaig );
+ pNew->pManHaig = NULL;
+ Aig_ManStop( pNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index f19a27b6..323a230f 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -885,7 +885,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
Saig_TsiStop( pTsi );
if ( pNew == NULL )
- pNew = Aig_ManDup( p );
+ pNew = Aig_ManDupSimple( p );
return pNew;
}
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 3935db6c..0ad6c314 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -622,7 +622,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
Vec_Ptr_t * vCut;
Aig_Man_t * pNew, * pTemp, * pCopy;
int i, fChanges;
- pNew = Aig_ManDup( p );
+ pNew = Aig_ManDupSimple( p );
// perform several iterations of forward retiming
fChanges = 0;
if ( !fBackwardOnly )
@@ -672,7 +672,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
{
if ( Saig_ManRegNum(pNew) == 0 )
break;
- pCopy = Aig_ManDup( pNew );
+ pCopy = Aig_ManDupSimple( pNew );
pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
Aig_ManStop( pCopy );
if ( pTemp == NULL )
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index e7ec3c08..f7c27a93 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -44,6 +44,7 @@ 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;
+ int fCompl;
assert( Saig_ManRegNum(p) > 0 );
assert( Aig_ObjIsNode(pObj) );
@@ -68,22 +69,26 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
pInput1 = Aig_ObjChild0( pInput1 );
pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) );
+ // get the condition when the register should be complemetned
+ fCompl = Aig_ObjFaninC0(pObj) && 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 = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) );
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++;
+//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n",
+// pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
+
// return register output
- return Aig_NotCond( pObjLo, pObjNew->fPhase );
+ return Aig_NotCond( pObjLo, fCompl );
}
/**Function*************************************************************
@@ -163,6 +168,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
int RetValue, s, i;
Aig_ManSetPioNumbers( p );
Aig_ManFanoutStart( p );
+ p->fCreatePios = 1;
if ( fForward )
{
for ( s = 0; s < nSteps; s++ )
@@ -172,7 +178,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
if ( pObjNew == NULL )
continue;
- Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+ Aig_ObjReplace( p, pObj, pObjNew, 0 );
break;
}
}
@@ -186,13 +192,16 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
if ( pObjNew == NULL )
continue;
- Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+ Aig_ObjReplace( p, pObj, pObjNew, 0 );
break;
}
}
}
+ p->fCreatePios = 0;
+ Aig_ManFanoutStop( p );
RetValue = Aig_ManCleanup( p );
assert( RetValue == 0 );
+ Aig_ManSetRegNum( p, p->nRegs );
}
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2024-08-13 18:21:56 +0000