summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/gia.h5
-rw-r--r--src/aig/gia/giaCCof.c281
-rw-r--r--src/aig/gia/giaFrames.c181
3 files changed, 250 insertions, 217 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index c652f1a0..d97276f5 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -174,6 +174,7 @@ struct Gia_ParFra_t_
{
int nFrames; // the number of frames to unroll
int fInit; // initialize the timeframes
+ int fSaveLastLit; // adds POs for outputs of each frame
int fVerbose; // enables verbose output
};
@@ -700,6 +701,10 @@ extern void Gia_ManFanoutStop( Gia_Man_t * p );
/*=== giaForce.c =========================================================*/
extern void For_ManExperiment( Gia_Man_t * pGia, int nIters, int fClustered, int fVerbose );
/*=== giaFrames.c =========================================================*/
+extern void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
+extern void * Gia_ManUnrollAdd( void * pMan, int fMax );
+extern void Gia_ManUnrollStop( void * pMan );
+extern int Gia_ManUnrollLastLit( void * pMan );
extern void Gia_ManFraSetDefaultParams( Gia_ParFra_t * p );
extern Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars );
/*=== giaFront.c ==========================================================*/
diff --git a/src/aig/gia/giaCCof.c b/src/aig/gia/giaCCof.c
index 5819ee92..7a346030 100644
--- a/src/aig/gia/giaCCof.c
+++ b/src/aig/gia/giaCCof.c
@@ -32,131 +32,22 @@ typedef struct Ccf_Man_t_ Ccf_Man_t; // manager
struct Ccf_Man_t_
{
// user data
- Gia_Man_t * pGia; // single output AIG manager
- int nFrameMax; // maximum number of frames
- int nConfMax; // maximum number of conflicts
- int nTimeMax; // maximum runtime in seconds
- int fVerbose; // verbose flag
+ Gia_Man_t * pGia; // single-output AIG manager
+ int nFrameMax; // maximum number of frames
+ int nConfMax; // maximum number of conflicts
+ int nTimeMax; // maximum runtime in seconds
+ int fVerbose; // verbose flag
// internal data
- sat_solver * pSat; // SAT solver
- Gia_Man_t * pFrames; // unrolled timeframes
- Vec_Int_t * vIdToFra; // maps GIA obj IDs into frame obj IDs
- Vec_Int_t * vOrder; // map Num to Id
- Vec_Int_t * vFraLims; // frame limits
+ void * pUnr; // unrolling manager
+ Gia_Man_t * pFrames; // unrolled timeframes
+ Vec_Int_t * vCopies; // copy pointers of the AIG
+ sat_solver * pSat; // SAT solver
};
-extern Vec_Int_t * Gia_VtaCollect( Gia_Man_t * p, Vec_Int_t ** pvFraLims, Vec_Int_t ** pvRoots );
-
-static inline int Gia_ObjFrames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj ) { assert( Vec_IntEntry(p->vIdToFra, f*Gia_ManObjNum(p->pGia)+Gia_ObjId(p->pGia,pObj)) >= 0 ); return Vec_IntEntry(p->vIdToFra, f*Gia_ManObjNum(p->pGia)+Gia_ObjId(p->pGia,pObj)); }
-static inline void Gia_ObjSetFrames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj, int Lit ) { Vec_IntWriteEntry(p->vIdToFra, f*Gia_ManObjNum(p->pGia)+Gia_ObjId(p->pGia,pObj), Lit); }
-
-static inline int Gia_ObjChild0Frames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjFrames(p, f, Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj)); }
-static inline int Gia_ObjChild1Frames( Ccf_Man_t * p, int f, Gia_Obj_t * pObj ) { return Gia_LitNotCond(Gia_ObjFrames(p, f, Gia_ObjFanin1(pObj)), Gia_ObjFaninC1(pObj)); }
-
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline int sat_solver_add_const( sat_solver * pSat, int iVar, int fCompl )
-{
- lit Lits[1];
- int Cid;
- assert( iVar >= 0 );
-
- Lits[0] = toLitCond( iVar, fCompl );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 1 );
- assert( Cid );
- return 1;
-}
-static inline int sat_solver_add_buffer( sat_solver * pSat, int iVarA, int iVarB, int fCompl )
-{
- lit Lits[2];
- int Cid;
- assert( iVarA >= 0 && iVarB >= 0 );
-
- Lits[0] = toLitCond( iVarA, 0 );
- Lits[1] = toLitCond( iVarB, !fCompl );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVarA, 1 );
- Lits[1] = toLitCond( iVarB, fCompl );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
- assert( Cid );
- return 2;
-}
-static inline int sat_solver_add_and( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 )
-{
- lit Lits[3];
- int Cid;
-
- Lits[0] = toLitCond( iVar, 1 );
- Lits[1] = toLitCond( iVar0, fCompl0 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVar, 1 );
- Lits[1] = toLitCond( iVar1, fCompl1 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVar, 0 );
- Lits[1] = toLitCond( iVar0, !fCompl0 );
- Lits[2] = toLitCond( iVar1, !fCompl1 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
- assert( Cid );
- return 3;
-}
-static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, int iVarC, int fCompl )
-{
- lit Lits[3];
- int Cid;
- assert( iVarA >= 0 && iVarB >= 0 && iVarC >= 0 );
-
- Lits[0] = toLitCond( iVarA, !fCompl );
- Lits[1] = toLitCond( iVarB, 1 );
- Lits[2] = toLitCond( iVarC, 1 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVarA, !fCompl );
- Lits[1] = toLitCond( iVarB, 0 );
- Lits[2] = toLitCond( iVarC, 0 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVarA, fCompl );
- Lits[1] = toLitCond( iVarB, 1 );
- Lits[2] = toLitCond( iVarC, 0 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVarA, fCompl );
- Lits[1] = toLitCond( iVarB, 0 );
- Lits[2] = toLitCond( iVarC, 1 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
- assert( Cid );
- return 4;
-}
-static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int fCompl )
-{
- lit Lits[2];
- int Cid;
- assert( iVar >= 0 );
-
- Lits[0] = toLitCond( iVar, fCompl );
- Lits[1] = toLitCond( iVar+1, 0 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
- assert( Cid );
-
- Lits[0] = toLitCond( iVar, fCompl );
- Lits[1] = toLitCond( iVar+1, 1 );
- Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
- assert( Cid );
- return 2;
-}
-
-
/**Function*************************************************************
Synopsis [Create manager.]
@@ -170,21 +61,25 @@ static inline int sat_solver_add_constraint( sat_solver * pSat, int iVar, int fC
***********************************************************************/
Ccf_Man_t * Ccf_ManStart( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTimeMax, int fVerbose )
{
+ static Gia_ParFra_t Pars, * pPars = &Pars;
Ccf_Man_t * p;
assert( nFrameMax > 0 );
p = ABC_CALLOC( Ccf_Man_t, 1 );
- p->pGia = pGia;
- p->nFrameMax = nFrameMax;
- p->nConfMax = nConfMax;
- p->nTimeMax = nTimeMax;
- p->fVerbose = fVerbose;
+ p->pGia = pGia;
+ p->nFrameMax = nFrameMax;
+ p->nConfMax = nConfMax;
+ p->nTimeMax = nTimeMax;
+ p->fVerbose = fVerbose;
+ // create unrolling manager
+ memset( pPars, 0, sizeof(Gia_ParFra_t) );
+ pPars->fVerbose = fVerbose;
+ pPars->nFrames = nFrameMax;
+ pPars->fSaveLastLit = 1;
+ p->pUnr = Gia_ManUnrollStart( pGia, pPars );
+ p->vCopies = Vec_IntAlloc( 1000 );
// internal data
- p->pFrames = Gia_ManStart( 10000 );
- Gia_ManHashAlloc( p->pFrames );
- p->vOrder = Gia_VtaCollect( pGia, &p->vFraLims, NULL );
- p->vIdToFra = Vec_IntAlloc( 0 );
- p->pSat = sat_solver_new();
- sat_solver_setnvars( p->pSat, 10000 );
+ p->pSat = sat_solver_new();
+// sat_solver_setnvars( p->pSat, 10000 );
return p;
}
@@ -201,9 +96,8 @@ Ccf_Man_t * Ccf_ManStart( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int nTi
***********************************************************************/
void Ccf_ManStop( Ccf_Man_t * p )
{
- Vec_IntFreeP( &p->vIdToFra );
- Vec_IntFreeP( &p->vOrder );
- Vec_IntFreeP( &p->vFraLims );
+ Vec_IntFree( p->vCopies );
+ Gia_ManUnrollStop( p->pUnr );
sat_solver_delete( p->pSat );
Gia_ManStopP( &p->pFrames );
ABC_FREE( p );
@@ -228,7 +122,7 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
// add SAT clauses
for ( i = sat_solver_nvars(p->pSat); i < Gia_ManObjNum(p->pFrames); i++ )
{
- pObj = Gia_ManObj( p->pGia, i );
+ pObj = Gia_ManObj( p->pFrames, i );
if ( Gia_ObjIsAnd(pObj) )
sat_solver_add_and( p->pSat, i,
Gia_ObjFaninId0(pObj, i),
@@ -238,54 +132,11 @@ void Gia_ManCofExtendSolver( Ccf_Man_t * p )
}
}
-/**Function*************************************************************
+static inline int Gia_Obj0Copy( Vec_Int_t * vCopies, Gia_Man_t * pGia, Gia_Obj_t * pObj )
+{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Gia_ObjFaninId0p(pGia, pObj)), Gia_ObjFaninC0(pObj) ); }
- Synopsis [Adds logic of one timeframe to the manager.]
-
- Description [Returns literal of the property output.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Gia_ManCofAddTimeFrame( Ccf_Man_t * p, int fMax )
-{
- Gia_Obj_t * pObj;
- int i, f, Beg, End, Lit;
- assert( fMax > 0 && fMax <= p->nFrameMax );
- assert( Vec_IntSize(p->vIdToFra) == (fMax - 1) * Gia_ManObjNum(p->pGia) );
- // add to the mapping of nodes
- Vec_IntFillExtra( p->vIdToFra, fMax * Gia_ManObjNum(p->pGia), -1 );
- // add nodes to each time-frame
- for ( f = 0; f < fMax; f++ )
- {
- if ( Vec_IntSize(p->vFraLims) >= fMax-f )
- continue;
- Beg = Vec_IntEntry( p->vFraLims, fMax-f-1 );
- End = Vec_IntEntry( p->vFraLims, fMax-f );
- for ( i = Beg; i < End; i++ )
- {
- pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vOrder, i) );
- if ( Gia_ObjIsAnd(pObj) )
- Lit = Gia_ManHashAnd( p->pFrames, Gia_ObjChild0Frames(p, f, pObj), Gia_ObjChild1Frames(p, f, pObj) );
- else if ( Gia_ObjIsRo(p->pGia, pObj) && f > 0 )
- Lit = Gia_ObjChild0Frames(p, f-1, Gia_ObjRoToRi(p->pGia, pObj));
- else if ( Gia_ObjIsCi(pObj) )
- {
- Lit = Gia_ManAppendCi(p->pFrames);
- // mark primary input
- Gia_ManObj(p->pFrames, Gia_Lit2Var(Lit))->fMark0 = Gia_ObjIsPi(p->pGia, pObj);
- }
- else assert( 0 );
- Gia_ObjSetFrames( p, f, pObj, Lit );
- }
- }
- // add SAT clauses
- Gia_ManCofExtendSolver( p );
- // return output literal
- return Gia_ObjChild0Frames( p, fMax-1, Gia_ManPo(p->pGia, 0) );
-}
+static inline int Gia_Obj1Copy( Vec_Int_t * vCopies, Gia_Man_t * pGia, Gia_Obj_t * pObj )
+{ return Gia_LitNotCond( Vec_IntEntry(vCopies, Gia_ObjFaninId1p(pGia, pObj)), Gia_ObjFaninC1(pObj) ); }
/**Function*************************************************************
@@ -298,22 +149,25 @@ int Gia_ManCofAddTimeFrame( Ccf_Man_t * p, int fMax )
SeeAlso []
***********************************************************************/
-int Gia_ManCofOneDerive_rec( Ccf_Man_t * p, Gia_Obj_t * pObj )
+void Gia_ManCofOneDerive_rec( Ccf_Man_t * p, Gia_Obj_t * pObj )
{
- if ( ~pObj->Value )
- return pObj->Value;
+ int Res, Id = Gia_ObjId( p->pFrames, pObj );
+ if ( Vec_IntEntry(p->vCopies, Id) != -1 )
+ return;
assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
if ( Gia_ObjIsAnd(pObj) )
{
Gia_ManCofOneDerive_rec( p, Gia_ObjFanin0(pObj) );
Gia_ManCofOneDerive_rec( p, Gia_ObjFanin1(pObj) );
- pObj->Value = Gia_ManHashAnd( p->pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ Res = Gia_ManHashAnd( p->pFrames,
+ Gia_Obj0Copy(p->vCopies, p->pFrames, pObj),
+ Gia_Obj1Copy(p->vCopies, p->pFrames, pObj) );
}
- else if ( pObj->fMark0 ) // PI
- pObj->Value = sat_solver_var_value( p->pSat, Gia_ObjId(p->pGia, pObj) );
+ else if ( Gia_ObjCioId(pObj) >= Gia_ManRegNum(p->pGia) ) // PI
+ Res = sat_solver_var_value( p->pSat, Id );
else
- pObj->Value = Gia_Var2Lit( Gia_ObjId(p->pGia, pObj), 0 );
- return pObj->Value;
+ Res = Gia_Var2Lit( Id, 0 );
+ Vec_IntWriteEntry( p->vCopies, Id, Res );
}
/**Function*************************************************************
@@ -334,8 +188,9 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
// get the property node
pObj = Gia_ManObj( p->pFrames, Gia_Lit2Var(LitProp) );
// derive the cofactor
- Gia_ManFillValue( p->pFrames );
- LitOut = Gia_ManCofOneDerive_rec( p, pObj );
+ Vec_IntFill( p->vCopies, Gia_ManObjNum(p->pFrames), -1 );
+ Gia_ManCofOneDerive_rec( p, pObj );
+ LitOut = Vec_IntEntry(p->vCopies, Gia_Lit2Var(LitProp));
LitOut = Gia_LitNotCond(LitOut, Gia_LitIsCompl(LitProp));
// add new PO for the cofactor
Gia_ManAppendCo( p->pFrames, LitOut );
@@ -343,7 +198,7 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
Gia_ManCofExtendSolver( p );
// return negative literal of the cofactor
return Gia_LitNot(LitOut);
-}
+}
/**Function*************************************************************
@@ -360,21 +215,32 @@ int Gia_ManCofOneDerive( Ccf_Man_t * p, int LitProp )
***********************************************************************/
int Gia_ManCofGetReachable( Ccf_Man_t * p, int Lit )
{
- int RetValue;
+ int ObjPrev = 0, ConfPrev = 0, clk;
+ int Count = 0, LitOut, RetValue;
// try solving for the first time and quit if converged
RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
if ( RetValue == l_False )
return 1;
// iterate circuit cofactoring
- while ( RetValue == 0 )
+ while ( RetValue == l_True )
{
+ clk = clock();
// derive cofactor
- int LitOut = Gia_ManCofOneDerive( p, Lit );
+ LitOut = Gia_ManCofOneDerive( p, Lit );
// add the blocking clause
RetValue = sat_solver_addclause( p->pSat, &LitOut, &LitOut + 1 );
assert( RetValue );
// try solving again
RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, p->nConfMax, 0, 0, 0 );
+ // derive cofactors
+ if ( p->fVerbose )
+ {
+ printf( "%3d : AIG =%7d Conf =%7d. ", Count++,
+ Gia_ManObjNum(p->pFrames) - ObjPrev, sat_solver_nconflicts(p->pSat) - ConfPrev );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ ObjPrev = Gia_ManObjNum(p->pFrames);
+ ConfPrev = sat_solver_nconflicts(p->pSat);
+ }
}
if ( RetValue == l_Undef )
return -1;
@@ -397,16 +263,22 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
Gia_Man_t * pNew;
Ccf_Man_t * p;
int f, Lit, RetValue;
+ int clk = clock();
assert( Gia_ManPoNum(pGia) == 1 );
+
// create reachability manager
p = Ccf_ManStart( pGia, nFrameMax, nConfMax, nTimeMax, fVerbose );
// perform backward image computation
for ( f = 0; f < nFrameMax; f++ )
{
- if ( fVerbose )
+ if ( fVerbose )
printf( "ITER %3d :\n", f );
- // derives new timeframe and returns the property literal
- Lit = Gia_ManCofAddTimeFrame( p, f+1 );
+ // add to the mapping of nodes
+ p->pFrames = (Gia_Man_t *)Gia_ManUnrollAdd( p->pUnr, f+1 );
+ // add SAT clauses
+ Gia_ManCofExtendSolver( p );
+ // return output literal
+ Lit = Gia_ManUnrollLastLit( p->pUnr );
// derives cofactors of the property literal till all states are blocked
RetValue = Gia_ManCofGetReachable( p, Lit );
if ( RetValue )
@@ -414,22 +286,27 @@ Gia_Man_t * Gia_ManCofTest( Gia_Man_t * pGia, int nFrameMax, int nConfMax, int n
}
// report the result
if ( f == nFrameMax )
- printf( "Completed %d frames without converging.\n", f );
+ printf( "Completed %d frames without converging. ", f );
else if ( RetValue == 1 )
- printf( "Backward reachability converged after %d iterations.\n", f );
+ printf( "Backward reachability converged after %d iterations. ", f-1 );
else if ( RetValue == -1 )
- printf( "Conflict limit or timeout is reached after %d frames.\n", f );
+ printf( "Conflict limit or timeout is reached after %d frames. ", f-1 );
+ Abc_PrintTime( 1, "Runtime", clock() - clk );
// get the resulting AIG manager
Gia_ManHashStop( p->pFrames );
- Gia_ManCleanMark0( p->pFrames );
pNew = p->pFrames; p->pFrames = NULL;
Ccf_ManStop( p );
+
+ // cleanup
+// if ( fVerbose )
+// Gia_ManPrintStats( pNew, 0 );
+
pNew = Gia_ManCleanup( pGia = pNew );
Gia_ManStop( pGia );
// if ( fVerbose )
- Gia_ManPrintStats( pNew, 0 );
+// Gia_ManPrintStats( pNew, 0 );
return pNew;
}
diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c
index 4ab98229..06bea871 100644
--- a/src/aig/gia/giaFrames.c
+++ b/src/aig/gia/giaFrames.c
@@ -52,6 +52,9 @@ struct Gia_ManUnr_t_
Vec_Int_t * vDegDiff; // degree of each node
Vec_Int_t * vFirst; // first entry in the store
Vec_Int_t * vStore; // store for saved data
+ // the resulting AIG
+ Gia_Man_t * pNew; // the resulting AIG
+ int LastLit; // the place to store the last literal
};
////////////////////////////////////////////////////////////////////////
@@ -153,6 +156,8 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
Gia_ManUnr_t * p;
Gia_Obj_t * pObj;
int i, k, iRank, iFanin, Degree, Shift;
+ int clk = clock();
+
p = ABC_CALLOC( Gia_ManUnr_t, 1 );
p->pAig = pAig;
p->pPars = pPars;
@@ -207,6 +212,16 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
// cleanup
Vec_IntFreeP( &p->vRank );
Vec_IntFreeP( &p->vDegree );
+
+ // print verbose output
+ if ( pPars->fVerbose )
+ {
+ printf( "Convergence = %d. Dangling objects = %d. Average degree = %.3f ",
+ Vec_IntSize(p->vLimit) - 1,
+ Gia_ManObjNum(pAig) - Gia_ManObjNum(p->pOrder),
+ 1.0*Vec_IntSize(p->vStore)/Gia_ManObjNum(p->pOrder) - 1.0 );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+ }
return p;
}
@@ -221,8 +236,9 @@ Gia_ManUnr_t * Gia_ManUnrStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
SeeAlso []
***********************************************************************/
-void Gia_ManUnrStop( Gia_ManUnr_t * p )
+void Gia_ManUnrollStop( void * pMan )
{
+ Gia_ManUnr_t * p = (Gia_ManUnr_t *)pMan;
Gia_ManStopP( &p->pOrder );
Vec_IntFreeP( &p->vLimit );
Vec_IntFreeP( &p->vRank );
@@ -279,7 +295,10 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
assert( Gia_ObjIsCi(pObjReal) );
if ( Gia_ObjIsPi(p->pAig, pObjReal) )
{
- pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
+ if ( !p->pPars->fSaveLastLit )
+ pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
+ else
+ pObj = Gia_ManPi( pNew, Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * f + Gia_ObjCioId(pObjReal) );
return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
}
if ( f == 0 ) // initialize!
@@ -287,7 +306,10 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
if ( p->pPars->fInit )
return 0;
assert( Gia_ObjCioId(pObjReal) >= Gia_ManPiNum(p->pAig) );
- pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
+ if ( !p->pPars->fSaveLastLit )
+ pObj = Gia_ManPi( pNew, Gia_ManPiNum(p->pAig) * p->pPars->nFrames + Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
+ else
+ pObj = Gia_ManPi( pNew, Gia_ObjCioId(pObjReal)-Gia_ManPiNum(p->pAig) );
return Gia_Var2Lit( Gia_ObjId(pNew, pObj), 0 );
}
pObj = Gia_ManObj( p->pOrder, Gia_Lit2Var(Gia_ObjRoToRi(p->pAig, pObjReal)->Value) );
@@ -306,6 +328,144 @@ static inline int Gia_ObjUnrReadCi( Gia_ManUnr_t * p, int Id, int f, Gia_Man_t *
SeeAlso []
***********************************************************************/
+void * Gia_ManUnrollStart( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
+{
+ Gia_ManUnr_t * p;
+ int f, i;
+ // start
+ p = Gia_ManUnrStart( pAig, pPars );
+ // start timeframes
+ assert( p->pNew == NULL );
+ p->pNew = Gia_ManStart( 10000 );
+ p->pNew->pName = Gia_UtilStrsav( p->pAig->pName );
+ Gia_ManHashAlloc( p->pNew );
+ // create combinational inputs
+ if ( !p->pPars->fSaveLastLit ) // only in the case when unrolling depth is known
+ for ( f = 0; f < p->pPars->nFrames; f++ )
+ for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+ Gia_ManAppendCi(p->pNew);
+ // create flop outputs
+ if ( !p->pPars->fInit ) // only in the case when initialization is not performed
+ for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
+ Gia_ManAppendCi(p->pNew);
+ return p;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes init/non-init unrolling without flops.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void * Gia_ManUnrollAdd( void * pMan, int fMax )
+{
+ Gia_ManUnr_t * p = (Gia_ManUnr_t *)pMan;
+ Gia_Obj_t * pObj;
+ int f, i, Lit, Beg, End;
+ // create PIs on demand
+ if ( p->pPars->fSaveLastLit )
+ for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
+ Gia_ManAppendCi(p->pNew);
+ // unroll another timeframe
+ for ( f = 0; f < fMax; f++ )
+ {
+ if ( Vec_IntSize(p->vLimit) <= fMax-f )
+ continue;
+ Beg = Vec_IntEntry( p->vLimit, fMax-f-1 );
+ End = Vec_IntEntry( p->vLimit, fMax-f );
+ for ( i = Beg; i < End; i++ )
+ {
+ pObj = Gia_ManObj( p->pOrder, i );
+ if ( Gia_ObjIsAnd(pObj) )
+ Lit = Gia_ManHashAnd( p->pNew, Gia_ObjUnrReadCopy0(p, pObj, i), Gia_ObjUnrReadCopy1(p, pObj, i) );
+ else if ( Gia_ObjIsCo(pObj) )
+ {
+ Lit = Gia_ObjUnrReadCopy0(p, pObj, i);
+ if ( f == fMax-1 )
+ {
+ if ( p->pPars->fSaveLastLit )
+ p->LastLit = Lit;
+ else
+ Gia_ManAppendCo( p->pNew, Lit );
+ }
+ }
+ else if ( Gia_ObjIsCi(pObj) )
+ Lit = Gia_ObjUnrReadCi( p, i, f, p->pNew );
+ else assert( 0 );
+ assert( Lit >= 0 );
+ Gia_ObjUnrWrite( p, i, Lit ); // should be exactly one call for each obj!
+ }
+ }
+ return p->pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Read the last literal.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Gia_ManUnrollLastLit( void * pMan )
+{
+ Gia_ManUnr_t * p = (Gia_ManUnr_t *)pMan;
+ return p->LastLit;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes init/non-init unrolling without flops.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManUnroll( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
+{
+ Gia_ManUnr_t * p;
+ Gia_Man_t * pNew, * pTemp;
+ int fMax;
+ p = (Gia_ManUnr_t *)Gia_ManUnrollStart( pAig, pPars );
+ for ( fMax = 1; fMax <= p->pPars->nFrames; fMax++ )
+ Gia_ManUnrollAdd( p, fMax );
+ assert( Gia_ManPoNum(p->pNew) == p->pPars->nFrames * Gia_ManPoNum(p->pAig) );
+ Gia_ManHashStop( p->pNew );
+ Gia_ManSetRegNum( p->pNew, 0 );
+// Gia_ManPrintStats( pNew, 0 );
+ // cleanup
+ p->pNew = Gia_ManCleanup( pTemp = p->pNew );
+ Gia_ManStop( pTemp );
+// Gia_ManPrintStats( pNew, 0 );
+ pNew = p->pNew; p->pNew = NULL;
+ Gia_ManUnrollStop( p );
+ return pNew;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Computes init/non-init unrolling without flops.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+/*
Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
{
Gia_Man_t * pNew, * pTemp;
@@ -359,6 +519,7 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
// Gia_ManPrintStats( pNew, 0 );
return pNew;
}
+*/
/**Function*************************************************************
@@ -373,19 +534,9 @@ Gia_Man_t * Gia_ManUnroll( Gia_ManUnr_t * p )
***********************************************************************/
Gia_Man_t * Gia_ManFrames2( Gia_Man_t * pAig, Gia_ParFra_t * pPars )
{
- Gia_ManUnr_t * p;
- Gia_Man_t * pNew = NULL;
+ Gia_Man_t * pNew;
int clk = clock();
- p = Gia_ManUnrStart( pAig, pPars );
- pNew = Gia_ManUnroll( p );
-
- if ( pPars->fVerbose )
- printf( "Convergence = %d. Dangling objects = %d. Average degree = %.3f ",
- Vec_IntSize(p->vLimit) - 1,
- Gia_ManObjNum(pAig) - Gia_ManObjNum(p->pOrder),
- 1.0*Vec_IntSize(p->vStore)/Gia_ManObjNum(p->pOrder) - 1.0 );
-
- Gia_ManUnrStop( p );
+ pNew = Gia_ManUnroll( pAig, pPars );
if ( pPars->fVerbose )
Abc_PrintTime( 1, "Time", clock() - clk );
return pNew;
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 21:14:17 +0000