From 0e256dc2c234d12455df121d3cb831ba726c4cfc Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 10 Sep 2013 22:12:42 -0700 Subject: Updates for the new BMC engine. --- src/sat/bmc/bmcBmcAnd.c | 425 +++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 416 insertions(+), 9 deletions(-) (limited to 'src/sat/bmc/bmcBmcAnd.c') diff --git a/src/sat/bmc/bmcBmcAnd.c b/src/sat/bmc/bmcBmcAnd.c index 8dadd619..39b4cb46 100644 --- a/src/sat/bmc/bmcBmcAnd.c +++ b/src/sat/bmc/bmcBmcAnd.c @@ -43,10 +43,331 @@ struct Bmc_Mna_t_ abctime clkStart; // starting time }; +static inline int Gia_ManTerSimInfoGet( unsigned * pInfo, int i ) +{ + return 3 & (pInfo[i >> 4] >> ((i & 15) << 1)); +} +static inline void Gia_ManTerSimInfoSet( unsigned * pInfo, int i, int Value ) +{ + assert( Value >= GIA_ZER && Value <= GIA_UND ); + Value ^= Gia_ManTerSimInfoGet( pInfo, i ); + pInfo[i >> 4] ^= (Value << ((i & 15) << 1)); +} + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Performs ternary simulation of the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Bmc_MnaTernary( Gia_Man_t * p, int nFrames, int nFramesAdd, int fVerbose, int * iFirst ) +{ + Vec_Ptr_t * vStates; + unsigned * pState; + int nStateWords = Abc_BitWordNum( 2*Gia_ManCoNum(p) ); + Gia_Obj_t * pObj, * pObjRo; + int f, i, Count[4]; + abctime clk = Abc_Clock(); + Gia_ManConst0(p)->Value = GIA_ZER; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = GIA_UND; + Gia_ManForEachRi( p, pObj, i ) + pObj->Value = GIA_ZER; + *iFirst = -1; + vStates = Vec_PtrAlloc( 100 ); + for ( f = 0; ; f++ ) + { + // if frames are given, break at frames + if ( nFrames && f == nFrames ) + break; + // if frames are not given, break after nFramesAdd from the first x-valued + if ( !nFrames && *iFirst >= 0 && f == *iFirst + nFramesAdd ) + break; + // aassign CI values + Gia_ManForEachRiRo( p, pObj, pObjRo, i ) + pObjRo->Value = pObj->Value; + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); + // compute and save CO values + pState = ABC_ALLOC( unsigned, nStateWords ); + Gia_ManForEachCo( p, pObj, i ) + { + pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + Gia_ManTerSimInfoSet( pState, i, pObj->Value ); + if ( *iFirst == -1 && i < Gia_ManPoNum(p) && pObj->Value == GIA_UND ) + *iFirst = f; + } + Vec_PtrPush( vStates, pState ); + // print statistics + if ( !fVerbose ) + continue; + Count[0] = Count[1] = Count[2] = Count[3] = 0; + Gia_ManForEachRi( p, pObj, i ) + Count[pObj->Value]++; + printf( "%5d : 0 =%7d 1 =%7d x =%7d all =%7d out = %s\n", + f, Count[GIA_ZER], Count[GIA_ONE], Count[GIA_UND], Gia_ManRegNum(p), + Gia_ManPo(p, 0)->Value == GIA_UND ? "x" : "0" ); + } +// assert( Vec_PtrSize(vStates) == nFrames ); + if ( fVerbose ) + printf( "Finished %d frames. First x-valued PO is in frame %d. ", nFrames, *iFirst ); + if ( fVerbose ) + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return vStates; +} + + +/**Function************************************************************* + + Synopsis [Collect AIG nodes for the group of POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_MnaCollect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes, unsigned * pState ) +{ + if ( pObj->fPhase ) + return; + pObj->fPhase = 1; + if ( Gia_ObjIsAnd(pObj) ) + { + Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState ); + Bmc_MnaCollect_rec( p, Gia_ObjFanin1(pObj), vNodes, pState ); + pObj->Value = Gia_XsimAndCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj), Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj) ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + pObj->Value = pState ? Gia_ManTerSimInfoGet( pState, Gia_ObjCioId(Gia_ObjRoToRi(p, pObj)) ) : GIA_ZER; + else if ( Gia_ObjIsPi(p, pObj) ) + pObj->Value = GIA_UND; + else assert( 0 ); + Vec_IntPush( vNodes, Gia_ObjId(p, pObj) ); +} +void Bmc_MnaCollect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, unsigned * pState ) +{ + Gia_Obj_t * pObj; + int i; + Vec_IntClear( vNodes ); + Gia_ManConst0(p)->fPhase = 1; + Gia_ManConst0(p)->Value = GIA_ZER; + Gia_ManForEachObjVec( vCos, p, pObj, i ) + { + assert( Gia_ObjIsCo(pObj) ); + Bmc_MnaCollect_rec( p, Gia_ObjFanin0(pObj), vNodes, pState ); + pObj->Value = Gia_XsimNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) ); + assert( pObj->Value == GIA_UND ); + } +} + +/**Function************************************************************* + + Synopsis [Select related logic cones for the COs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_MnaSelect_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vLeaves ) +{ + if ( !pObj->fPhase ) + return; + pObj->fPhase = 0; + assert( pObj->Value == GIA_UND ); + if ( Gia_ObjIsAnd(pObj) ) + { + if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) + Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves ); + else assert( Gia_ObjFanin0(pObj)->Value + Gia_ObjFaninC0(pObj) == GIA_ONE ); + if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) + Bmc_MnaSelect_rec( p, Gia_ObjFanin1(pObj), vLeaves ); + else assert( Gia_ObjFanin1(pObj)->Value + Gia_ObjFaninC1(pObj) == GIA_ONE ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + Vec_IntPush( vLeaves, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)) ); +} +void Bmc_MnaSelect( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Vec_Int_t * vLeaves ) +{ + Gia_Obj_t * pObj; + int i; + Vec_IntClear( vLeaves ); + Gia_ManForEachObjVec( vCos, p, pObj, i ) + Bmc_MnaSelect_rec( p, Gia_ObjFanin0(pObj), vLeaves ); + Gia_ManConst0(p)->fPhase = 0; + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->fPhase = 0; +} + +/**Function************************************************************* + + Synopsis [Build AIG for the selected cones.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bmc_MnaBuild_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Man_t * pNew, Vec_Int_t * vMap ) +{ + if ( !pObj->fPhase ) + return; + pObj->fPhase = 0; + assert( pObj->Value == GIA_UND ); + if ( Gia_ObjIsAnd(pObj) ) + { + int iLit0 = 1, iLit1 = 1; + if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) + Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap ); + if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) + Bmc_MnaBuild_rec( p, Gia_ObjFanin1(pObj), pNew, vMap ); + if ( Gia_ObjFanin0(pObj)->Value == GIA_UND ) + iLit0 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) ); + if ( Gia_ObjFanin1(pObj)->Value == GIA_UND ) + iLit1 = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId1p(p, pObj)), Gia_ObjFaninC1(pObj) ); + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManHashAnd(pNew, iLit0, iLit1) ); + } + else if ( Gia_ObjIsRo(p, pObj) ) + assert( Vec_IntEntry(vMap, Gia_ObjId(p, pObj)) != -1 ); + else if ( Gia_ObjIsPi(p, pObj) ) + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), Gia_ManAppendCi(pNew) ); + else assert( 0 ); +} +void Bmc_MnaBuild( Gia_Man_t * p, Vec_Int_t * vCos, Vec_Int_t * vNodes, Gia_Man_t * pNew, Vec_Int_t * vMap ) +{ + Gia_Obj_t * pObj; + int i, iLit; + Gia_ManForEachObjVec( vCos, p, pObj, i ) + { + assert( Gia_ObjIsCo(pObj) ); + Bmc_MnaBuild_rec( p, Gia_ObjFanin0(pObj), pNew, vMap ); + iLit = Abc_LitNotCond( Vec_IntEntry(vMap, Gia_ObjFaninId0p(p, pObj)), Gia_ObjFaninC0(pObj) ); + Vec_IntWriteEntry( vMap, Gia_ObjId(p, pObj), iLit ); + } + Gia_ManConst0(p)->fPhase = 0; + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->fPhase = 0; +} + + +/**Function************************************************************* + + Synopsis [Compute the first non-trivial timeframe.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManBmcUnroll( Gia_Man_t * pGia, int nFramesMax, int nFramesAdd, int fVerbose ) +{ + Gia_Obj_t * pObj; + Gia_Man_t * pNew, * pTemp; + Vec_Ptr_t * vStates, * vBegins; + Vec_Int_t * vRoots, * vCone, * vLeaves, * vMap; + unsigned * pStateF, * pStateP; + int f, i, iFirst; + Gia_ManCleanPhase( pGia ); + vCone = Vec_IntAlloc( 1000 ); + vLeaves = Vec_IntAlloc( 1000 ); + // perform ternary simulation + vStates = Bmc_MnaTernary( pGia, nFramesMax, nFramesAdd, fVerbose, &iFirst ); + // go backward + vBegins = Vec_PtrStart( Vec_PtrSize(vStates) ); + for ( f = Vec_PtrSize(vStates) - 1; f >= 0; f-- ) + { + // get ternary states + pStateF = (unsigned *)Vec_PtrEntry(vStates, f); + pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0; + // collect roots of this frame + vRoots = Vec_IntAlloc( 100 ); + Gia_ManForEachPo( pGia, pObj, i ) + if ( Gia_ManTerSimInfoGet( pStateF, Gia_ObjCioId(pObj) ) == GIA_UND ) + Vec_IntPush( vRoots, Gia_ObjId(pGia, pObj) ); + // add leaves from the previous frame + Vec_IntAppend( vRoots, vLeaves ); + Vec_PtrWriteEntry( vBegins, f, vRoots ); + // find the cone + Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone + Bmc_MnaSelect( pGia, vRoots, vCone, vLeaves ); // computes vLeaves + if ( fVerbose ) + printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n", + f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) ); + if ( Vec_IntSize(vLeaves) == 0 ) + break; + // it is possible that some of the POs are still ternary... + } + assert( f >= 0 ); + // go forward + vMap = Vec_IntStartFull( Gia_ManObjNum(pGia) ); + pNew = Gia_ManStart( 10000 ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + Gia_ManHashStart( pNew ); + for ( f = 0; f < Vec_PtrSize(vStates); f++ ) + { + vRoots = (Vec_Int_t *)Vec_PtrEntry( vBegins, f ); + if ( vRoots == NULL ) + { + Gia_ManForEachPo( pGia, pObj, i ) + Gia_ManAppendCo( pNew, 0 ); + continue; + } + // get ternary states + pStateF = (unsigned *)Vec_PtrEntry(vStates, f); + pStateP = f ? (unsigned *)Vec_PtrEntry(vStates, f-1) : 0; + // clean POs + Gia_ManForEachPo( pGia, pObj, i ) + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pObj), 0 ); + // find the cone + Bmc_MnaCollect( pGia, vRoots, vCone, pStateP ); // computes vCone + Bmc_MnaBuild( pGia, vRoots, vCone, pNew, vMap ); // computes pNew + if ( fVerbose ) + printf( "Frame %4d : Roots = %6d Leaves = %6d Cone = %6d\n", + f, Vec_IntSize(vRoots), Vec_IntSize(vLeaves), Vec_IntSize(vCone) ); + // create POs + Gia_ManForEachPo( pGia, pObj, i ) + Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) ); + // set a new map + Gia_ManForEachObjVec( vRoots, pGia, pObj, i ) + if ( Gia_ObjIsRi(pGia, pObj) ) + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, Gia_ObjRiToRo(pGia, pObj)), Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) ); +// else if ( Gia_ObjIsPo(pGia, pObj) ) +// Gia_ManAppendCo( pNew, Vec_IntEntry(vMap, Gia_ObjId(pGia, pObj)) ); +// else assert( 0 ); + } + Gia_ManHashStop( pNew ); + Vec_VecFree( (Vec_Vec_t *)vBegins ); + Vec_PtrFreeFree( vStates ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vCone ); + Vec_IntFree( vMap ); + // cleanup +// Gia_ManPrintStats( pNew, NULL ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); +// Gia_ManPrintStats( pNew, NULL ); + return pNew; +} + + + /**Function************************************************************* Synopsis [BMC manager manipulation.] @@ -255,7 +576,7 @@ void Gia_ManBmcAddCone_rec( Bmc_Mna_t * p, Gia_Obj_t * pObj ) else Vec_IntPush( p->vInputs, iObj ); } -void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart ) +void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart, int iStop ) { Gia_Obj_t * pObj; int i; @@ -263,7 +584,7 @@ void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart ) Vec_IntClear( p->vInputs ); Vec_IntClear( p->vOutputs ); Vec_IntFillExtra( p->vId2Var, Gia_ManObjNum(p->pFrames), 0 ); - for ( i = iStart; i < Gia_ManPoNum(p->pFrames); i++ ) + for ( i = iStart; i < iStop; i++ ) { pObj = Gia_ManPo(p->pFrames, i); if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) @@ -289,10 +610,10 @@ void Gia_ManBmcAddCone( Bmc_Mna_t * p, int iStart ) SeeAlso [] ***********************************************************************/ -int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart ) +int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart, int iStop ) { int i; - for ( i = iStart; i < Gia_ManPoNum(pFrames); i++ ) + for ( i = iStart; i < iStop; i++ ) if ( Gia_ObjChild0(Gia_ManPo(pFrames, i)) != Gia_ManConst0(pFrames) ) return 0; return 1; @@ -309,24 +630,25 @@ int Gia_ManBmcCheckOutputs( Gia_Man_t * pFrames, int iStart ) SeeAlso [] ***********************************************************************/ -int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) +int Gia_ManBmcPerform_Unr( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) { Unr_Man_t * pUnroll; - Bmc_Mna_t * p = Bmc_MnaAlloc(); + Bmc_Mna_t * p; int nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY; int f, i=0, Lit, status, RetValue = -2; + p = Bmc_MnaAlloc(); pUnroll = Unr_ManUnrollStart( pGia, pPars->fVeryVerbose ); for ( f = 0; f < nFramesMax; f++ ) { p->pFrames = Unr_ManUnrollFrame( pUnroll, f ); - if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia) ) ) + if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) ) { // create another slice - Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia) ); + Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ); // create CNF in the SAT solver Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs ); // try solving the outputs - for ( i = f * Gia_ManPoNum(pGia); i < Gia_ManPoNum(p->pFrames); i++ ) + for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) { Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i); if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) @@ -380,6 +702,91 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) return RetValue; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) +{ + Bmc_Mna_t * p; + int nFramesMax, f, i=0, Lit, status, RetValue = -2; + p = Bmc_MnaAlloc(); + p->pFrames = Gia_ManBmcUnroll( pGia, pPars->nFramesMax, pPars->nFramesAdd, pPars->fVeryVerbose ); + nFramesMax = Gia_ManPoNum(p->pFrames) / Gia_ManPoNum(pGia); + if ( pPars->fVerbose ) + printf( "Performed unfolding for %d frames.\n", nFramesMax ); + if ( pPars->fVerbose ) + Gia_ManPrintStats( p->pFrames, NULL ); + for ( f = 0; f < nFramesMax; f++ ) + { + if ( !Gia_ManBmcCheckOutputs( p->pFrames, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ) ) + { + // create another slice + Gia_ManBmcAddCone( p, f * Gia_ManPoNum(pGia), (f+1) * Gia_ManPoNum(pGia) ); + // create CNF in the SAT solver + Gia_ManBmcAddCnf( p, p->pFrames, p->vInputs, p->vNodes, p->vOutputs ); + // try solving the outputs + for ( i = f * Gia_ManPoNum(pGia); i < (f+1) * Gia_ManPoNum(pGia); i++ ) + { + Gia_Obj_t * pObj = Gia_ManPo(p->pFrames, i); + if ( Gia_ObjChild0(pObj) == Gia_ManConst0(p->pFrames) ) + continue; + Lit = Abc_Var2Lit( Vec_IntEntry(p->vId2Var, Gia_ObjId(p->pFrames, pObj)), 0 ); + status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 ); + if ( status == l_False ) // unsat + continue; + if ( status == l_True ) // sat + RetValue = 0; + if ( status == l_Undef ) // undecided + RetValue = -1; + break; + } + // report statistics + if ( pPars->fVerbose ) + { + printf( "%4d : PI =%9d. AIG =%9d. Var =%8d. In =%6d. And =%9d. Cla =%9d. Conf =%9d. Mem =%7.1f MB ", + f, Gia_ManPiNum(p->pFrames), Gia_ManAndNum(p->pFrames), + p->nSatVars-1, Vec_IntSize(p->vInputs), Vec_IntSize(p->vNodes), + sat_solver_nclauses(p->pSat), sat_solver_nconflicts(p->pSat), Gia_ManMemory(p->pFrames)/(1<<20) ); + Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); + } + } + if ( RetValue != -2 ) + { + if ( RetValue == -1 ) + printf( "SAT solver reached conflict/runtime limit in frame %d.\n", f ); + else + { + printf( "Output %d of miter \"%s\" was asserted in frame %d. ", + i - f * Gia_ManPoNum(pGia), Gia_ManName(pGia), f ); + Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); + } + break; + } + } + if ( RetValue == -2 ) + RetValue = -1; + // dump unfolded frames + if ( pPars->fDumpFrames ) + { + p->pFrames = Gia_ManCleanup( p->pFrames ); + Gia_AigerWrite( p->pFrames, "frames.aig", 0, 0 ); + printf( "Dumped unfolded frames into file \"frames.aig\".\n" ); + Gia_ManStop( p->pFrames ); + } + // cleanup + Gia_ManStop( p->pFrames ); + Bmc_MnaFree( p ); + return RetValue; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3