From fd62957d39c18bd755e7fa46cf7dc7e278c6778c Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 5 Jan 2012 18:48:11 +0700 Subject: Backward reachability using circuit cofactoring. --- src/aig/gia/gia.h | 5 + src/aig/gia/giaCCof.c | 281 ++++++++++++++---------------------------------- src/aig/gia/giaFrames.c | 181 ++++++++++++++++++++++++++++--- 3 files changed, 250 insertions(+), 217 deletions(-) (limited to 'src/aig') 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; -- cgit v1.2.3