diff options
| -rw-r--r-- | src/aig/gia/gia.h | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaFrames.c | 60 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc2.c | 122 | ||||
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 199 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 26 |
5 files changed, 229 insertions, 179 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index dc3a3b01..b3584f14 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -739,6 +739,7 @@ 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 ); +extern Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbose ); /*=== giaFront.c ==========================================================*/ extern Gia_Man_t * Gia_ManFront( Gia_Man_t * p ); extern void Gia_ManFrontTest( Gia_Man_t * p ); diff --git a/src/aig/gia/giaFrames.c b/src/aig/gia/giaFrames.c index a14122ae..48a0568e 100644 --- a/src/aig/gia/giaFrames.c +++ b/src/aig/gia/giaFrames.c @@ -915,6 +915,66 @@ Gia_Man_t * Gia_ManFrames( Gia_Man_t * pAig, Gia_ParFra_t * pPars ) return pFrames; } + +/**Function************************************************************* + + Synopsis [Perform init unrolling as long as PO(s) are constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFrames, int fVerbose ) +{ + Gia_Man_t * pFrames, * pTemp; + Gia_Obj_t * pObj; + int i, f; + assert( Gia_ManRegNum(pAig) > 0 ); + if ( nFrames > 0 ) + printf( "Computing specialized unrolling with %d frames...\n", nFrames ); + pFrames = Gia_ManStart( Gia_ManObjNum(pAig) ); + pFrames->pName = Abc_UtilStrsav( pAig->pName ); + Gia_ManHashAlloc( pFrames ); + Gia_ManConst0(pAig)->Value = 0; + for ( f = 0; nFrames == 0 || f < nFrames; f++ ) + { + if ( fVerbose && (f % 100 == 0) ) + { + printf( "%6d : ", f ); + Gia_ManPrintStats( pFrames, 0, 0 ); + } + Gia_ManForEachRo( pAig, pObj, i ) + pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0; + Gia_ManForEachPi( pAig, pObj, i ) + pObj->Value = Gia_ManAppendCi( pFrames ); + Gia_ManForEachAnd( pAig, pObj, i ) + pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( pAig, pObj, i ) + if ( Gia_ObjFanin0Copy(pObj) != 0 ) + break; + if ( i < Gia_ManPoNum(pAig) ) + break; + Gia_ManForEachRi( pAig, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + } + if ( fVerbose ) + printf( "Computed prefix of %d frames.\n", f ); + Gia_ManForEachRi( pAig, pObj, i ) + Gia_ManAppendCo( pFrames, pObj->Value ); + Gia_ManHashStop( pFrames ); + pFrames = Gia_ManCleanup( pTemp = pFrames ); + if ( fVerbose ) + printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", + Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) ); + Gia_ManStop( pTemp ); + return pFrames; +} + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index ca6049ef..d28320fc 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -25,12 +25,11 @@ ABC_NAMESPACE_IMPL_START - //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1) +//#define AIG_VISITED ((Aig_Obj_t *)(ABC_PTRUINT_T)1) typedef struct Saig_Bmc_t_ Saig_Bmc_t; struct Saig_Bmc_t_ @@ -44,11 +43,10 @@ struct Saig_Bmc_t_ // AIG managers Aig_Man_t * pAig; // the user's AIG manager Aig_Man_t * pFrm; // Frames manager - Vec_Ptr_t * vVisited; // nodes visited in Frames + Vec_Int_t * vVisited; // nodes visited in Frames // 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 @@ -63,15 +61,43 @@ struct Saig_Bmc_t_ int iOutputFail; // failed output }; -static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); } -static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); } - -static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); } -static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); } +static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) +{ +// return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id ); + Aig_Obj_t * pRes; + Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i ); + int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) ); + if ( iObjLit == -1 ) + return NULL; + pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) ); + if ( pRes == NULL ) + Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 ); + else + pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) ); + return pRes; +} +static inline void Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) +{ +// Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode ); + Vec_Int_t * vFrame; + int iObjLit; + if ( i == Vec_PtrSize(p->vAig2Frm) ) + Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) ); + assert( i < Vec_PtrSize(p->vAig2Frm) ); + vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i ); + if ( pNode == NULL ) + iObjLit = -1; + else + iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) ); + Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit ); +} static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj)); } static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj)); } +static inline int Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj ) { return Vec_IntGetEntry( p->vObj2Var, pObj->Id ); } +static inline void Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num ) { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -268,12 +294,11 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, p->pAig = pAig; p->nObjs = Aig_ManObjNumMax(pAig); // create node and variable mappings - p->vAig2Frm = Vec_PtrAlloc( 0 ); - Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL ); + p->vAig2Frm = Vec_PtrAlloc( 100 ); p->vObj2Var = Vec_IntAlloc( 0 ); - Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 ); + Vec_IntFill( p->vObj2Var, p->nObjs, 0 ); // start the AIG manager and map primary inputs - p->pFrm = Aig_ManStart( 5 * p->nObjs ); + p->pFrm = Aig_ManStart( p->nObjs ); Saig_ManForEachLo( pAig, pObj, i ) Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); // create SAT solver @@ -284,8 +309,8 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ ); // other data structures - p->vTargets = Vec_PtrAlloc( 0 ); - p->vVisited = Vec_PtrAlloc( 0 ); + p->vTargets = Vec_PtrAlloc( 1000 ); + p->vVisited = Vec_IntAlloc( 1000 ); p->iOutputFail = -1; p->iFrameFail = -1; return p; @@ -304,36 +329,12 @@ 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_VecFree( (Vec_Vec_t *)p->vAig2Frm ); Vec_IntFree( p->vObj2Var ); sat_solver_delete( p->pSat ); Vec_PtrFree( p->vTargets ); - Vec_PtrFree( p->vVisited ); + Vec_IntFree( p->vVisited ); ABC_FREE( p ); } @@ -348,6 +349,7 @@ void Saig_BmcManStop( Saig_Bmc_t * p ) SeeAlso [] ***********************************************************************/ +/* Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i ) { Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig); @@ -388,6 +390,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i Saig_BmcObjSetFrame( p, pObj, i, pRes ); return pRes; } +*/ /**Function************************************************************* @@ -400,7 +403,7 @@ Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Ptr_t * vVisited ) +Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited ) { Aig_Obj_t * pRes; pRes = Saig_BmcObjFrame( p, pObj, i ); @@ -428,8 +431,8 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int } assert( pRes != NULL ); Saig_BmcObjSetFrame( p, pObj, i, pRes ); - Vec_PtrPush( vVisited, pObj ); - Vec_PtrPush( vVisited, (void *)(ABC_PTRINT_T)i ); + Vec_IntPush( vVisited, Aig_ObjId(pObj) ); + Vec_IntPush( vVisited, i ); return pRes; } @@ -447,13 +450,12 @@ Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int void Saig_BmcInterval( Saig_Bmc_t * p ) { Aig_Obj_t * pTarget; - Aig_Obj_t * pObj, * pRes; - int i, iFrame, Counter; + int i, iObj, iFrame; int nNodes = Aig_ManObjNum( p->pFrm ); Vec_PtrClear( p->vTargets ); p->iFramePrev = p->iFrameLast; for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 ) - { + { if ( p->iOutputLast == 0 ) { Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) ); @@ -463,24 +465,14 @@ void Saig_BmcInterval( Saig_Bmc_t * p ) if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax ) return; // Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast ); - Vec_PtrClear( p->vVisited ); + Vec_IntClear( p->vVisited ); pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited ); Vec_PtrPush( p->vTargets, pTarget ); Aig_ObjCreateCo( p->pFrm, pTarget ); Aig_ManCleanup( p->pFrm ); // check if the node is gone - Counter = 0; - Vec_PtrForEachEntry( Aig_Obj_t *, 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 ); + Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i ) + Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame ); } } } @@ -500,7 +492,7 @@ Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj { if ( pObj->pData ) return (Aig_Obj_t *)pObj->pData; - Vec_PtrPush( p->vVisited, pObj ); + Vec_IntPush( p->vVisited, Aig_ObjId(pObj) ); if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) ) { p->nStitchVars += !Aig_ObjIsCi(pObj); @@ -533,15 +525,15 @@ Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p ) pNew = Aig_ManStart( p->nNodesMax ); Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew); - Vec_PtrClear( p->vVisited ); - Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) ); + Vec_IntClear( p->vVisited ); + Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) ); Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i ) { // assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) ); pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) ); assert( !Aig_IsComplement(pObjNew) ); Aig_ObjCreateCo( pNew, pObjNew ); - } + } return pNew; } @@ -560,7 +552,7 @@ void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf ) { Aig_Obj_t * pObj, * pObjNew; int i, Lits[2], VarNumOld, VarNumNew; - Vec_PtrForEachEntry( Aig_Obj_t *, p->vVisited, pObj, i ) + Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i ) { // get the new variable of this node pObjNew = (Aig_Obj_t *)pObj->pData; diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 17a85bad..0a283bb5 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -40,14 +40,13 @@ struct Gia_ManBmc_t_ Vec_Int_t * vMapping; // mapping Vec_Vec_t * vSects; // sections Vec_Int_t * vId2Num; // number of each node - Vec_Int_t * vVisited; // visited nodes - // SAT variables - Vec_Int_t * vPiVars; // SAT vars for the PIs + Vec_Ptr_t * vTerInfo; // ternary information Vec_Ptr_t * vId2Var; // SAT vars for each object // SAT solver sat_solver * pSat; // SAT solver int nSatVars; // SAT variables int nObjNums; // SAT objects + int nWordNum; // unsigned words for ternary simulation int nBufNum; // the number of simple nodes int nDupNum; // the number of simple nodes char * pSopSizes, ** pSops; // CNF representation @@ -684,14 +683,15 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig ) Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ ); Aig_ManForEachCo( pAig, pObj, i ) Vec_IntWriteEntry( p->vId2Num, Aig_ObjId(pObj), p->nObjNums++ ); - p->vPiVars = Vec_IntAlloc( 1000 ); p->vId2Var = Vec_PtrAlloc( 100 ); - p->vVisited = Vec_IntAlloc( 1000 ); + p->vTerInfo = Vec_PtrAlloc( 100 ); // create solver p->nSatVars = 1; p->pSat = sat_solver_new(); sat_solver_setnvars( p->pSat, 1000 ); Cnf_ReadMsops( &p->pSopSizes, &p->pSops ); + // terminary simulation + p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) ); return p; } @@ -708,7 +708,7 @@ Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig ) ***********************************************************************/ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) { - Aig_ManCleanMarkA( p->pAig ); +// Aig_ManCleanMarkA( p->pAig ); if ( p->vCexes ) { assert( p->pAig->vSeqModelVec == NULL ); @@ -719,9 +719,8 @@ void Saig_Bmc3ManStop( Gia_ManBmc_t * p ) Vec_IntFree( p->vMapping ); Vec_VecFree( p->vSects ); Vec_IntFree( p->vId2Num ); - Vec_IntFree( p->vPiVars ); - Vec_IntFree( p->vVisited ); Vec_VecFree( (Vec_Vec_t *)p->vId2Var ); + Vec_PtrFreeFree( p->vTerInfo ); sat_solver_delete( p->pSat ); free( p->pSopSizes ); free( p->pSops[1] ); @@ -790,13 +789,6 @@ static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int ObjNum = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) ); vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame ); Vec_IntWriteEntry( vFrame, ObjNum, iLit ); - if ( iLit == ABC_INFINITY || iLit == ABC_INFINITY+1 ) - { - Vec_IntPush( p->vVisited, Aig_ObjId(pObj) ); - Vec_IntPush( p->vVisited, iFrame ); - } - else if ( iLit != ~0 && Saig_ObjIsPi(p->pAig, pObj) ) // save PI SAT var num - Vec_IntWriteEntry( p->vPiVars, iFrame*Saig_ManPiNum(p->pAig)+Aig_ObjCioId(pObj), lit_var(iLit) ); return iLit; } @@ -1058,12 +1050,14 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in { iLit = ABC_INFINITY; } + assert( iLit != ABC_INFINITY ); return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit ); } + /**Function************************************************************* - Synopsis [Derives CNF for one node.] + Synopsis [Recursively performs terminary simulation.] Description [] @@ -1072,25 +1066,59 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in SeeAlso [] ***********************************************************************/ -int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) +int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) { - int i, iLit, Entry, iFrameOld, Value; - Vec_IntClear( p->vVisited ); - iLit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 0 ); - Vec_IntForEachEntry( p->vVisited, Entry, i ) + unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame ); + int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj ); + if ( Value != SAIG_TER_NON ) + return Value; + if ( Aig_ObjIsCo(pObj) ) { - iFrameOld = Vec_IntEntry( p->vVisited, ++i ); - Value = Saig_ManBmcLiteral( p, Aig_ManObj(p->pAig, Entry), iFrameOld ); -// assert( Value == 0 || Value == 1 || Value == ABC_INFINITY || Value == ABC_INFINITY+1 ); - assert( Value == ABC_INFINITY || Value == ABC_INFINITY+1 ); - if ( !(Value == ABC_INFINITY || Value == ABC_INFINITY+1) ) - printf( "Internal error!\n" ); -// if ( Value == 0 || Value == 1 ) -// continue; - Saig_ManBmcSetLiteral( p, Aig_ManObj(p->pAig, Entry), iFrameOld, ~0 ); + Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame ); + if ( Aig_ObjFaninC0(pObj) ) + Value = Saig_ManBmcSimInfoNot( Value ); } - if ( iLit < 2 ) - return iLit; + else if ( Saig_ObjIsLo(p->pAig, pObj) ) + { + assert( iFrame > 0 ); + Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 ); + } + else if ( Aig_ObjIsNode(pObj) ) + { + Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame ); + Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame ); + if ( Aig_ObjFaninC0(pObj) ) + Val0 = Saig_ManBmcSimInfoNot( Val0 ); + if ( Aig_ObjFaninC1(pObj) ) + Val1 = Saig_ManBmcSimInfoNot( Val1 ); + Value = Saig_ManBmcSimInfoAnd( Val0, Val1 ); + } + else assert( 0 ); + Saig_ManBmcSimInfoSet( pInfo, pObj, Value ); + // transfer to the unrolling + if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND ) + Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) ); + return Value; +} + +/**Function************************************************************* + + Synopsis [Derives CNF for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame ) +{ + // perform terminary simulation + int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame ); + if ( Value != SAIG_TER_UND ) + return (int)(Value == SAIG_TER_ONE); + // construct CNF if value is ternary return Saig_ManBmcCreateCnf_rec( p, pObj, iFrame, 1 ); } @@ -1124,44 +1152,6 @@ int Aig_NodeCompareRefsIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 ) /**Function************************************************************* - Synopsis [Mark PIs to be skipped based on nPisAbstract.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Saig_ManBmcMarkPis( Aig_Man_t * pAig, int nPisAbstract ) -{ - Vec_Ptr_t * vPis; - Aig_Obj_t * pObj; - int i; - if ( nPisAbstract < 1 ) - return; - // sort PIs by the number of their fanouts - vPis = Vec_PtrAlloc( 100 ); - Saig_ManForEachPi( pAig, pObj, i ) - Vec_PtrPush( vPis, pObj ); - Vec_PtrSort( vPis, (int (*)(void))Aig_NodeCompareRefsIncrease ); - Vec_PtrForEachEntry( Aig_Obj_t *, vPis, pObj, i ) - { - if ( i < nPisAbstract ) - { - pObj->fMarkA = 1; -// printf( "%d=%d ", Aig_ObjCioId(pObj), Aig_ObjRefs(pObj) ); - } - } -// printf( "\n" ); - // print primary inputs -// Saig_ManForEachPi( pAig, pObj, i ) -// printf( "%d=%d ", i, Aig_ObjRefs(pObj) ); -// printf( "\n" ); -} - -/**Function************************************************************* - Synopsis [This procedure sets default parameters.] Description [] @@ -1203,19 +1193,18 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) { Gia_ManBmc_t * p; Aig_Obj_t * pObj; + unsigned * pInfo; int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0; - int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); + int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) ); int i, f, Lit, status, clk, clk2, clkOther = 0, clkTotal = clock(); int nTimeToStop = time(NULL) + pPars->nTimeOut; - if ( pPars->fVerbose && Aig_ManConstrNum(pAig) > 0 ) - printf( "Performing BMC with constraints...\n" ); p = Saig_Bmc3ManStart( pAig ); p->pPars = pPars; if ( pPars->fVerbose ) { - printf( "Running \"bmc3\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d. Map = %6d. Sect =%3d.\n", + printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n", Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), - Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), (Vec_IntSize(p->vMapping)-Aig_ManObjNumMax(pAig))/5, Vec_VecSize(p->vSects) ); + Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) ); printf( "Params: Start = %d. FramesMax = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", pPars->nStart, pPars->nFramesMax, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll ); } @@ -1225,7 +1214,6 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); // perform frames Aig_ManRandom( 1 ); - Saig_ManBmcMarkPis( pAig, pPars->nPisAbstract ); for ( f = 0; f < pPars->nFramesMax; f++ ) { // stop BMC after exploring all reachable states @@ -1235,7 +1223,7 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) return pPars->nFailOuts ? 0 : 1; } // stop BMC if all targets are solved - if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) + if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) ) { Saig_Bmc3ManStop( p ); return 0; @@ -1243,11 +1231,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) // consider the next timeframe if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame ) pPars->iFrame = f-1; - // resize the array - Vec_IntFillExtra( p->vPiVars, (f+1)*Saig_ManPiNum(p->pAig), 0 ); // map nodes of this section Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) ); + Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) ); /* + // cannot remove mapping of frame values for any timeframes + // because with constant propagation they may be needed arbitrarily far if ( f > 2*Vec_VecSize(p->vSects) ) { int iFrameOld = f - 2*Vec_VecSize( p->vSects ); @@ -1257,28 +1246,15 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars ) */ // prepare some nodes Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 ); + Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE ); + Saig_ManForEachPi( pAig, pObj, i ) + Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND ); if ( f == 0 ) - Saig_ManForEachLo( p->pAig, pObj, i ) - Saig_ManBmcSetLiteral( p, pObj, 0, 0 ); - // set PIs to zero if they are marked - Saig_ManForEachPi( p->pAig, pObj, i ) - if ( pObj->fMarkA ) - Saig_ManBmcSetLiteral( p, pObj, f, Aig_ManRandom(0) & 1 ); - // add the constraints for this frame - Saig_ManForEachPo( pAig, pObj, i ) { - if ( i < Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) - continue; -clk2 = clock(); - Lit = Saig_ManBmcCreateCnf( p, pObj, f ); - Lit = lit_neg( Lit ); -clkOther += clock() - clk2; - status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); - if ( status == 0 ) + Saig_ManForEachLo( p->pAig, pObj, i ) { - printf( "SAT problem became UNSAT after adding constraints in frame %d.\n", f ); - Saig_Bmc3ManStop( p ); - return 1; + Saig_ManBmcSetLiteral( p, pObj, 0, 0 ); + Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER ); } } if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) ) @@ -1287,7 +1263,7 @@ clkOther += clock() - clk2; clk = clock(); Saig_ManForEachPo( pAig, pObj, i ) { - if ( i >= Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ) + if ( i >= Saig_ManPoNum(pAig) ) break; // skip solved outputs if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) ) @@ -1311,7 +1287,7 @@ clkOther += clock() - clk2; } pPars->nFailOuts++; printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", - nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); + nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); @@ -1332,13 +1308,19 @@ clkOther += clock() - clk2; } else if ( status == l_True ) { - int * pModel = Sat_SolverGetModel( p->pSat, Vec_IntArray(p->vPiVars), Vec_IntSize(p->vPiVars) ); - Abc_Cex_t * pCex = Abc_CexCreate( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), pModel, f, i, 1 ); - ABC_FREE( pModel ); + Aig_Obj_t * pObjPi; + Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i ); + int j, k, iBit = Saig_ManRegNum(pAig); + for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) ) + Saig_ManForEachPi( p->pAig, pObjPi, k ) + { + int iLit = Saig_ManBmcLiteral( p, pObjPi, j ); + if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) ) + Abc_InfoSetBit( pCex->pData, iBit + k ); + } fFirst = 0; if ( !pPars->fSolveAll ) { -//ABC_PRT( "CNF generation runtime", clkOther ); if ( pPars->fVerbose ) { printf( "%3d %s : ", f, fUnfinished ? "-" : "+" ); @@ -1347,8 +1329,9 @@ clkOther += clock() - clk2; printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); + printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) ); + printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); - printf( "%5.0f Mb", 1.0+sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); @@ -1364,7 +1347,7 @@ clkOther += clock() - clk2; } pPars->nFailOuts++; printf( "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", - nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) - Saig_ManConstrNum(pAig) ); + nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); if ( p->vCexes == NULL ) p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) ); Vec_PtrWriteEntry( p->vCexes, i, pCex ); @@ -1409,8 +1392,10 @@ clkOther += clock() - clk2; printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts ); printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations ); // ABC_PRT( "Time", clock() - clk ); +// printf( "%4.0f Mb", 4.0*Vec_IntSize(p->vVisited) /(1<<20) ); + printf( "%4.0f Mb", 4.0*(f+1)*p->nObjNums /(1<<20) ); + printf( "%4.0f Mb", 1.0*sat_solver_memory(p->pSat)/(1<<20) ); printf( "%9.2f sec ", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) ); - printf( "%5.0f Mb", 1.0+sat_solver_memory(p->pSat)/(1<<20) ); printf( "\n" ); // ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 ); // ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fa2aa375..9167c54c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -19927,6 +19927,11 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Does not work for combinational networks.\n" ); return 0; } + if ( Abc_NtkConstrNum(pNtk) > 0 ) + { + Abc_Print( -1, "Constraints have to be folded (use \"fold\").\n" ); + return 0; + } pAbc->Status = Abc_NtkDarBmc3( pNtk, pPars, fOrDecomp ); pAbc->nFrames = pPars->iFrame; Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel ); @@ -24162,10 +24167,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ParFra_t Pars, * pPars = &Pars; int c; int nCofFanLit = 0; - int nNewAlgo = 1; + int fNewAlgo = 1; + int fInitSpecial = 0; Gia_ManFraSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FLiavh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FLiasvh" ) ) != EOF ) { switch ( c ) { @@ -24195,7 +24201,10 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->fInit ^= 1; break; case 'a': - nNewAlgo ^= 1; + fNewAlgo ^= 1; + break; + case 's': + fInitSpecial ^= 1; break; case 'v': pPars->fVerbose ^= 1; @@ -24216,9 +24225,11 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The network is combinational.\n" ); return 0; } - if ( nCofFanLit ) + if ( fInitSpecial ) + pTemp = Gia_ManFramesInitSpecial( pAbc->pGia, pPars->nFrames, pPars->fVerbose ); + else if ( nCofFanLit ) pTemp = Gia_ManUnrollAndCofactor( pAbc->pGia, pPars->nFrames, nCofFanLit, pPars->fVerbose ); - else if ( nNewAlgo ) + else if ( fNewAlgo ) pTemp = Gia_ManFrames2( pAbc->pGia, pPars ); else pTemp = Gia_ManFrames( pAbc->pGia, pPars ); @@ -24226,12 +24237,13 @@ int Abc_CommandAbc9Frames( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &frames [-FL <num>] [-aivh]\n" ); + Abc_Print( -2, "usage: &frames [-FL <num>] [-iasvh]\n" ); Abc_Print( -2, "\t unrolls the design for several timeframes\n" ); Abc_Print( -2, "\t-F num : the number of frames to unroll [default = %d]\n", pPars->nFrames ); Abc_Print( -2, "\t-L num : the limit on fanout count of resets/enables to cofactor [default = %d]\n", nCofFanLit ); Abc_Print( -2, "\t-i : toggle initializing registers [default = %s]\n", pPars->fInit? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", nNewAlgo? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle computing special AIG for BMC [default = %s]\n", fInitSpecial? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; |