diff options
Diffstat (limited to 'src/aig/saig')
-rw-r--r-- | src/aig/saig/saig.h | 3 | ||||
-rw-r--r-- | src/aig/saig/saigAbs.c | 122 | ||||
-rw-r--r-- | src/aig/saig/saigBmc.c | 251 | ||||
-rw-r--r-- | src/aig/saig/saigDup.c | 121 | ||||
-rw-r--r-- | src/aig/saig/saigSimExt.c | 10 |
5 files changed, 407 insertions, 100 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index b77a4292..f72a3074 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -26,6 +26,7 @@ //////////////////////////////////////////////////////////////////////// #include "aig.h" +#include "giaAbs.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -90,7 +91,7 @@ static inline Aig_Obj_t * Saig_ObjLiToLo( Aig_Man_t * p, Aig_Obj_t * pObj ) { //////////////////////////////////////////////////////////////////////// /*=== sswAbs.c ==========================================================*/ -extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ); +extern Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ); /*=== saigBmc.c ==========================================================*/ extern int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit ); extern void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite ); diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c index 844d6f24..2fac60f5 100644 --- a/src/aig/saig/saigAbs.c +++ b/src/aig/saig/saigAbs.c @@ -686,6 +686,30 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex /**Function************************************************************* + Synopsis [Find the first PI corresponding to the flop.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManFirstFlopPi( Aig_Man_t * p, Aig_Man_t * pAbs ) +{ + Aig_Obj_t * pObj; + int i; + assert( pAbs->vCiNumsOrig != NULL ); + Aig_ManForEachPi( p, pObj, i ) + { + if ( Vec_IntEntry(pAbs->vCiNumsOrig, i) >= Saig_ManPiNum(p) ) + return i; + } + return -1; +} + +/**Function************************************************************* + Synopsis [Performs proof-based abstraction using BMC of the given depth.] Description [] @@ -701,9 +725,9 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex, int fVerbose ); extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent ); - Vec_Int_t * vFlopsNew, * vPiToReg; - Aig_Obj_t * pObj; - int i, Entry, iFlop; + Vec_Int_t * vFlopsNew;//, * vPiToReg; +// Aig_Obj_t * pObj; + int i, Entry;//, iFlop; if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 ) { Fra_Sec_t SecPar, * pSecPar = &SecPar; @@ -727,8 +751,8 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF return NULL; if ( pnUseStart ) *pnUseStart = ((Fra_Cex_t *)pAbs->pSeqModel)->iFrame; -// Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel ); - vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); +// vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManPiNum(p), pAbs->pSeqModel, fVerbose ); + vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose ); if ( Vec_IntSize(vFlopsNew) == 0 ) { printf( "Discovered a true counter-example!\n" ); @@ -739,7 +763,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF if ( fVerbose ) printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) ); // vFlopsNew contains PI number that should be kept in pAbs - +/* // for each additional PI, collect the number of a register it stands for Vec_IntForEachEntry( vFlops, Entry, i ) { @@ -773,6 +797,20 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF Vec_IntSort( vFlops, 0 ); Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) assert( Vec_IntEntry(vFlops, i-1) != Entry ); +*/ + // add to the abstraction + Vec_IntForEachEntry( vFlopsNew, Entry, i ) + { + Entry = Vec_IntEntry(pAbs->vCiNumsOrig, Entry); + assert( Entry >= Saig_ManPiNum(p) ); + assert( Entry < Aig_ManPiNum(p) ); + Vec_IntPush( vFlops, Entry-Saig_ManPiNum(p) ); + } + Vec_IntFree( vFlopsNew ); + + Vec_IntSort( vFlops, 0 ); + Vec_IntForEachEntryStart( vFlops, Entry, i, 1 ) + assert( Vec_IntEntry(vFlops, i-1) != Entry ); return Saig_ManAbstraction( p, vFlops ); } @@ -788,7 +826,7 @@ Aig_Man_t * Saig_ManProofRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vF SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, int fDynamic, int fExtend, int fSkipProof, int nFramesBmc, int nConfMaxBmc, int nRatio, int fUseBdds, int fUseDprove, int fUseStart, int fVerbose ) +Vec_Int_t * Saig_ManProofAbstraction_int( Aig_Man_t * p, Gia_ParAbs_t * pPars ) { Aig_Man_t * pResult, * pTemp; Cnf_Dat_t * pCnf; @@ -800,10 +838,10 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, assert( Aig_ManRegNum(p) > 0 ); Aig_ManSetPioNumbers( p ); - if ( fSkipProof ) + if ( pPars->fSkipProof ) { // assert( 0 ); - if ( fVerbose ) + if ( pPars->fVerbose ) printf( "Performing counter-example-based refinement.\n" ); // vFlops = Vec_IntStartNatural( 100 ); // Vec_IntPush( vFlops, 0 ); @@ -811,12 +849,12 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, } else { - if ( fVerbose ) - printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", nFrames, nConfMax ); - if ( fDynamic ) + if ( pPars->fVerbose ) + printf( "Performing proof-based abstraction with %d frames and %d max conflicts.\n", pPars->nFramesMax, pPars->nConfMax ); + if ( pPars->fDynamic ) { // create CNF for the frames - vFrames = Saig_AbsCreateFrames( p, nFrames, fVerbose ); + vFrames = Saig_AbsCreateFrames( p, pPars->nFramesMax, pPars->fVerbose ); // create dynamic solver pSat = Saig_AbsCreateSolverDyn( p, vFrames ); } @@ -825,15 +863,15 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, // create CNF for the AIG pCnf = Cnf_DeriveSimple( p, Aig_ManPoNum(p) ); // create SAT solver for the unrolled AIG - pSat = Saig_AbsCreateSolver( pCnf, nFrames ); + pSat = Saig_AbsCreateSolver( pCnf, pPars->nFramesMax ); } - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "SAT solver: Vars = %7d. Clauses = %7d. ", pSat->size, pSat->stats.clauses ); ABC_PRT( "Time", clock() - clk2 ); } // compute UNSAT core - vCore = Saig_AbsSolverUnsatCore( pSat, nConfMax, fVerbose ); + vCore = Saig_AbsSolverUnsatCore( pSat, pPars->nConfMax, pPars->fVerbose ); sat_solver_delete( pSat ); if ( vCore == NULL ) { @@ -841,18 +879,18 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, return NULL; } // collect registers - if ( fDynamic ) + if ( pPars->fDynamic ) { vFlops = Saig_AbsCollectRegistersDyn( p, vFrames, vCore ); Saig_AbsFreeCnfs( vFrames ); } else { - vFlops = Saig_AbsCollectRegisters( pCnf, nFrames, vCore ); + vFlops = Saig_AbsCollectRegisters( pCnf, pPars->nFramesMax, vCore ); Cnf_DataFree( pCnf ); } Vec_IntFree( vCore ); - if ( fVerbose ) + if ( pPars->fVerbose ) { printf( "The number of relevant registers is %d (out of %d). ", Vec_IntSize(vFlops), Aig_ManRegNum(p) ); ABC_PRT( "Time", clock() - clk ); @@ -872,10 +910,10 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, // create the resulting AIG pResult = Saig_ManAbstraction( p, vFlops ); - if ( fExtend ) + if ( pPars->fExtend ) { int nUseStart = 0; - if ( !fVerbose ) + if ( !pPars->fVerbose ) { printf( "Init : " ); Aig_ManPrintStats( pResult ); @@ -883,13 +921,13 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, printf( "Refining abstraction...\n" ); for ( Iter = 0; ; Iter++ ) { - pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fUseBdds, fUseDprove, fUseStart?&nUseStart:NULL, fVerbose ); + pTemp = Saig_ManProofRefine( p, pResult, vFlops, pPars->nFramesBmc, pPars->nConfMaxBmc, pPars->fUseBdds, pPars->fUseDprove, pPars->fUseStart?&nUseStart:NULL, pPars->fVerbose ); if ( pTemp == NULL ) break; Aig_ManStop( pResult ); pResult = pTemp; printf( "ITER %4d : ", Iter ); - if ( !fVerbose ) + if ( !pPars->fVerbose ) Aig_ManPrintStats( pResult ); // else // printf( " -----------------------------------------------------\n" ); @@ -897,26 +935,52 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax, Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); // printf( "Intermediate abstracted model was written into file \"%s\".\n", "gabs.aig" ); // check if the ratio is reached - if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio ) + if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*pPars->nRatio ) { - printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio ); + printf( "Refinements is stopped because flop reduction is less than %d%%\n", pPars->nRatio ); Aig_ManStop( pResult ); pResult = NULL; break; } } } - Vec_IntFree( vFlops ); // write the final result if ( pResult ) + Aig_ManStop( pResult ); + else { - Ioa_WriteAiger( pResult, "gabs.aig", 0, 0 ); - printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); + Vec_IntFree( vFlops ); + vFlops = NULL; } - return pResult; + return vFlops; } +/**Function************************************************************* + Synopsis [Performs proof-based abstraction using BMC of the given depth.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, Gia_ParAbs_t * pPars ) +{ + Vec_Int_t * vFlops; + Aig_Man_t * pAbs = NULL; + vFlops = Saig_ManProofAbstraction_int( p, pPars ); + // write the final result + if ( vFlops ) + { + pAbs = Saig_ManAbstraction( p, vFlops ); + Ioa_WriteAiger( pAbs, "gabs.aig", 0, 0 ); + printf( "Final abstracted model was written into file \"%s\".\n", "gabs.aig" ); + Vec_IntFree( vFlops ); + } + return pAbs; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c index a37be3ad..ac1cbe5b 100644 --- a/src/aig/saig/saigBmc.c +++ b/src/aig/saig/saigBmc.c @@ -45,6 +45,7 @@ struct Saig_Bmc_t_ // node mapping int nObjs; // the largest number of an AIG object Vec_Ptr_t * vAig2Frm; // mapping of AIG nodees into Frames nodes +// Vec_Str_t * vAig2Frm2; // mapping of AIG nodees into Frames nodes // SAT solver sat_solver * pSat; // SAT solver int nSatVars; // the number of used SAT variables @@ -71,6 +72,170 @@ static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, i /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +#define ABS_ZER 1 +#define ABS_ONE 2 +#define ABS_UND 3 + +static inline int Abs_ManSimInfoNot( int Value ) +{ + if ( Value == ABS_ZER ) + return ABS_ONE; + if ( Value == ABS_ONE ) + return ABS_ZER; + return ABS_UND; +} + +static inline int Abs_ManSimInfoAnd( int Value0, int Value1 ) +{ + if ( Value0 == ABS_ZER || Value1 == ABS_ZER ) + return ABS_ZER; + if ( Value0 == ABS_ONE && Value1 == ABS_ONE ) + return ABS_ONE; + return ABS_UND; +} + +static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame ) +{ + unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame ); + return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1)); +} + +static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value ) +{ + unsigned * pInfo = Vec_PtrEntry( vSimInfo, iFrame ); + assert( Value >= ABS_ZER && Value <= ABS_UND ); + Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame ); + pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1)); +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + int Value0, Value1, Value; + Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame ); + if ( Value ) + return Value; + if ( Aig_ObjIsPi(pObj) ) + { + assert( Saig_ObjIsLo(p, pObj) ); + Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 ); + Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); + return Value; + } + Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame ); + if ( Aig_ObjFaninC0(pObj) ) + Value0 = Abs_ManSimInfoNot( Value0 ); + if ( Aig_ObjIsPo(pObj) ) + { + Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 ); + return Value0; + } + assert( Aig_ObjIsNode(pObj) ); + if ( Value0 == ABS_ZER ) + Value = ABS_ZER; + else + { + Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame ); + if ( Aig_ObjFaninC1(pObj) ) + Value1 = Abs_ManSimInfoNot( Value1 ); + Value = Abs_ManSimInfoAnd( Value0, Value1 ); + } + Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value ); + assert( Value ); + return Value; +} + +/**Function************************************************************* + + Synopsis [Performs ternary simulation for one design.] + + Description [The returned array contains the result of ternary + simulation for all the frames where the output could be proved 0.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose ) +{ + Vec_Ptr_t * vSimInfo; + Aig_Obj_t * pObj; + int i, f, nFramesLimit, nFrameWords; + int clk = clock(); + assert( Aig_ManRegNum(p) > 0 ); + // the maximum number of frames will be determined to use at most 200Mb of RAM + nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p); + nFramesLimit = ABC_MIN( nFramesLimit, nFramesMax ); + nFrameWords = Aig_BitWordNum( 2 * Aig_ManObjNum(p) ); + // allocate simulation info + vSimInfo = Vec_PtrAlloc( nFramesLimit ); + for ( f = 0; f < nFramesLimit; f++ ) + { + Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) ); + if ( f == 0 ) + { + Saig_ManForEachLo( p, pObj, i ) + Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER ); + } + Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE ); + Saig_ManForEachPi( p, pObj, i ) + Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND ); + Saig_ManForEachPo( p, pObj, i ) + Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f ); + // check if simulation has derived at least one fail or unknown + Saig_ManForEachPo( p, pObj, i ) + if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER ) + { + if ( fVerbose ) + { + printf( "Ternary sim found non-zero output in frame %d. Used %5.2f Mb. ", + f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) ); + ABC_PRT( "Time", clock() - clk ); + } + return vSimInfo; + } + } + if ( fVerbose ) + { + printf( "Ternary sim proved all outputs in the first %d frames. Used %5.2f Mb. ", + nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) ); + ABC_PRT( "Time", clock() - clk ); + } + return vSimInfo; +} + +/**Function************************************************************* + + Synopsis [Free the array of simulation info.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abs_ManFreeAray( Vec_Ptr_t * p ) +{ + void * pTemp; + int i; + Vec_PtrForEachEntry( p, pTemp, i ) + ABC_FREE( pTemp ); + Vec_PtrFree( p ); +} + + /**Function************************************************************* Synopsis [Create manager.] @@ -135,8 +300,32 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, ***********************************************************************/ void Saig_BmcManStop( Saig_Bmc_t * p ) { +// Aig_Obj_t * pObj; +// int i, f, Counter = 0; +// int i, Counter = 0; +// for ( i = 0; i < p->vAig2Frm2->nSize; i++ ) +// Counter += (p->vAig2Frm2->pArray[i] != 0); +// for ( i = 0; i < p->vAig2Frm->nSize; i++ ) +// Counter += (p->vAig2Frm->pArray[i] != NULL); +// printf( "Objs = %d. Nodes = %d. Frames = %d. Used = %d. Non-empty = %d.\n", +// p->nObjs, Aig_ManNodeNum(p->pAig), p->iFrameLast, p->vAig2Frm->nSize, Counter ); + +/* + Aig_ManForEachObj( p->pAig, pObj, i ) + { + int Last = -1; + for ( f = 0; f <= p->iFrameLast; f++ ) + if ( Saig_BmcObjFrame( p, pObj, f ) ) + Last = f; + if ( i % 50 == 0 ) + printf( "%d ", Last ); + } + printf( "\n" ); +*/ + Aig_ManStop( p->pFrm ); Vec_PtrFree( p->vAig2Frm ); +// Vec_StrFree( p->vAig2Frm2 ); Vec_IntFree( p->vObj2Var ); sat_solver_delete( p->pSat ); Vec_PtrFree( p->vTargets ); @@ -207,44 +396,6 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Saig_BmcIntervalConstruct_rec_OLD( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) -{ - Aig_Obj_t * pRes; - pRes = Saig_BmcObjFrame( p, pObj, i ); - assert( pRes != NULL ); - if ( pRes != AIG_VISITED ) - return pRes; - if ( Saig_ObjIsPi( p->pAig, pObj ) ) - pRes = Aig_ObjCreatePi(p->pFrm); - else if ( Saig_ObjIsLo( p->pAig, pObj ) ) - pRes = Saig_BmcIntervalConstruct_rec_OLD( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 ); - else if ( Aig_ObjIsPo( pObj ) ) - { - Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i ); - pRes = Saig_BmcObjChild0( p, pObj, i ); - } - else - { - Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin0(pObj), i ); - Saig_BmcIntervalConstruct_rec_OLD( p, Aig_ObjFanin1(pObj), i ); - pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); - } - assert( pRes != AIG_VISITED ); - Saig_BmcObjSetFrame( p, pObj, i, pRes ); - return pRes; -} - -/**Function************************************************************* - - Synopsis [Performs the actual construction of the output.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Ptr_t * vVisited ) { Aig_Obj_t * pRes; @@ -263,8 +414,13 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int else { Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited ); - Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited ); - pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); + if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) ) + pRes = Aig_ManConst0(p->pFrm); + else + { + Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited ); + pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) ); + } } assert( pRes != NULL ); Saig_BmcObjSetFrame( p, pObj, i, pRes ); @@ -288,7 +444,7 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) { Aig_Obj_t * pTarget; Aig_Obj_t * pObj, * pRes; - int i, iFrame; + int i, iFrame, Counter; int nNodes = Aig_ManObjNum( p->pFrm ); Vec_PtrClear( p->vTargets ); p->iFramePrev = p->iFrameLast; @@ -309,13 +465,18 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) Aig_ObjCreatePo( p->pFrm, pTarget ); Aig_ManCleanup( p->pFrm ); // check if the node is gone + Counter = 0; Vec_PtrForEachEntry( p->vVisited, pObj, i ) { iFrame = (int)(ABC_PTRINT_T)Vec_PtrEntry( p->vVisited, 1+i++ ); pRes = Saig_BmcObjFrame( p, pObj, iFrame ); if ( Aig_ObjIsNone( Aig_Regular(pRes) ) ) + { Saig_BmcObjSetFrame( p, pObj, iFrame, NULL ); + Counter++; + } } +// printf( "%d ", Counter ); } } } @@ -564,7 +725,7 @@ void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p ) Aig_ManPrintStats( p->pFrm ); Aig_ManCleanup( p->pFrm ); Aig_ManPrintStats( p->pFrm ); -} +} /**Function************************************************************* @@ -584,6 +745,11 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMa Cnf_Dat_t * pCnf; int nOutsSolved = 0; int Iter, RetValue, clk = clock(), clk2; +/* + Vec_Ptr_t * vSimInfo; + vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose ); + Abs_ManFreeAray( vSimInfo ); +*/ p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); if ( fVerbose ) { @@ -593,6 +759,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMa printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll ); } + for ( Iter = 0; ; Iter++ ) { clk2 = clock(); diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index e6534a1f..e261fca1 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -70,7 +70,7 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) /**Function************************************************************* - Synopsis [Numbers of flops included in the abstraction.] + Synopsis [Duplicates the AIG manager recursively.] Description [] @@ -79,55 +79,130 @@ Aig_Man_t * Said_ManDupOrpos( Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ) +Aig_Obj_t * Saig_ManAbstractionDfs_rec( Aig_Man_t * pNew, Aig_Obj_t * pObj ) { - Aig_Man_t * pAigNew;//, * pTemp; + if ( pObj->pData ) + return pObj->pData; + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Trims the model by removing PIs without fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManTrimPis( Aig_Man_t * p ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj; + int i, fAllPisHaveNoRefs; + // check the refs of PIs + fAllPisHaveNoRefs = 1; + Saig_ManForEachPi( p, pObj, i ) + if ( pObj->nRefs ) + fAllPisHaveNoRefs = 0; + // start the new manager + pNew = Aig_ManStart( Aig_ManObjNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); + // start mapping of the CI numbers + pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); + // map const and primary inputs + Aig_ManCleanData( p ); + Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManForEachPi( p, pObj, i ) + if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) ) + { + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) ); + } + Aig_ManForEachNode( p, pObj, i ) + pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + Aig_ManForEachPo( p, pObj, i ) + pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Performs abstraction of the AIG to preserve the included flops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Saig_ManAbstraction( Aig_Man_t * p, Vec_Int_t * vFlops ) +{ + Aig_Man_t * pNew, * pTemp; Aig_Obj_t * pObj, * pObjLi, * pObjLo; int i, Entry; + Aig_ManCleanData( p ); // start the new manager - pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) ); - pAigNew->pName = Aig_UtilStrsav( pAig->pName ); + pNew = Aig_ManStart( Aig_ManNodeNum(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); // map the constant node - Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew ); + Aig_ManConst1(p)->pData = Aig_ManConst1( pNew ); // label included flops Vec_IntForEachEntry( vFlops, Entry, i ) { - pObjLi = Saig_ManLi( pAig, Entry ); + pObjLi = Saig_ManLi( p, Entry ); assert( pObjLi->fMarkA == 0 ); pObjLi->fMarkA = 1; - pObjLo = Saig_ManLo( pAig, Entry ); + pObjLo = Saig_ManLo( p, Entry ); assert( pObjLo->fMarkA == 0 ); pObjLo->fMarkA = 1; } // create variables for PIs - Aig_ManForEachPi( pAig, pObj, i ) + assert( p->vCiNumsOrig == NULL ); + pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManPiNum(p) ); + Aig_ManForEachPi( p, pObj, i ) if ( !pObj->fMarkA ) - pObj->pData = Aig_ObjCreatePi( pAigNew ); + { + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_IntPush( pNew->vCiNumsOrig, i ); + } // create variables for LOs - Aig_ManForEachPi( pAig, pObj, i ) + Aig_ManForEachPi( p, pObj, i ) if ( pObj->fMarkA ) { pObj->fMarkA = 0; - pObj->pData = Aig_ObjCreatePi( pAigNew ); + pObj->pData = Aig_ObjCreatePi( pNew ); + Vec_IntPush( pNew->vCiNumsOrig, i ); } // add internal nodes - Aig_ManForEachNode( pAig, pObj, i ) - pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); +// Aig_ManForEachNode( p, pObj, i ) +// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); // create POs - Saig_ManForEachPo( pAig, pObj, i ) - Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManForEachPo( p, pObj, i ) + { + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } // create LIs - Aig_ManForEachPo( pAig, pObj, i ) + Aig_ManForEachPo( p, pObj, i ) if ( pObj->fMarkA ) { pObj->fMarkA = 0; - Aig_ObjCreatePo( pAigNew, Aig_ObjChild0Copy(pObj) ); + Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) ); + Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); } - Aig_ManSetRegNum( pAigNew, Vec_IntSize(vFlops) ); - Aig_ManSeqCleanup( pAigNew ); -// pAigNew = Aig_ManDupSimpleDfs( pTemp = pAigNew ); -// Aig_ManStop( pTemp ); - return pAigNew; + Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) ); + Aig_ManSeqCleanup( pNew ); + // remove PIs without fanout + pNew = Saig_ManTrimPis( pTemp = pNew ); + Aig_ManStop( pTemp ); + return pNew; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c index 97b91b1d..22d5d6b8 100644 --- a/src/aig/saig/saigSimExt.c +++ b/src/aig/saig/saigSimExt.c @@ -247,7 +247,7 @@ void Saig_ManExtendUndo( Aig_Man_t * p, Vec_Ptr_t * vSimInfo, Vec_Int_t * vUndo SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose ) { Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2; int i, f, Value; @@ -262,7 +262,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t vVis = Vec_IntAlloc( 1000 ); vVis2 = Vec_IntAlloc( 1000 ); vUndo = Vec_IntAlloc( 1000 ); - for ( i = iFirstPi; i < Saig_ManPiNum(p); i++ ) + for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ ) { Vec_IntClear( vUndo ); for ( f = pCex->iFrame; f >= 0; f-- ) @@ -297,7 +297,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t SeeAlso [] ***********************************************************************/ -Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t * pCex, int fVerbose ) +Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstFlopPi, Ssw_Cex_t * pCex, int fVerbose ) { Vec_Int_t * vRes; Vec_Ptr_t * vSimInfo; @@ -305,10 +305,10 @@ Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Ssw_C Aig_ManFanoutStart( p ); vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) ); clk = clock(); - vRes = Saig_ManExtendCounterExample( p, iFirstPi, pCex, vSimInfo, fVerbose ); + vRes = Saig_ManExtendCounterExample( p, iFirstFlopPi, pCex, vSimInfo, fVerbose ); if ( fVerbose ) { - printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstPi, Vec_IntSize(vRes) ); + printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) ); ABC_PRT( "Time", clock() - clk ); } Vec_PtrFree( vSimInfo ); |