From 89e8e50069b62afa021bfd16b340d56cd5b4c113 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 6 Feb 2017 00:21:28 -0800 Subject: Improving new X-valued simulation in 'pdr'. --- src/proof/pdr/pdrInv.c | 8 +-- src/proof/pdr/pdrMan.c | 4 +- src/proof/pdr/pdrTsim2.c | 177 ++++++++++++++++++++++++++++++++++++++++++++--- src/sat/bmc/bmcCexCare.c | 31 +++++++-- 4 files changed, 203 insertions(+), 17 deletions(-) diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c index 16d98a36..8130d0a3 100644 --- a/src/proof/pdr/pdrInv.c +++ b/src/proof/pdr/pdrInv.c @@ -467,10 +467,10 @@ void Pdr_ManReportInvariant( Pdr_Man_t * p ) Vec_Ptr_t * vCubes; int kStart = Pdr_ManFindInvariantStart( p ); vCubes = Pdr_ManCollectCubes( p, kStart ); -// Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n", -// kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns ); - Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", - kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) ); + Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d) (%.2f)\n", + kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig), 1.0*p->nXsimLits/p->nXsimRuns ); +// Abc_Print( 1, "Invariant F[%d] : %d clauses with %d flops (out of %d)\n", +// kStart, Vec_PtrSize(vCubes), Pdr_ManCountVariables(p, kStart), Aig_ManRegNum(p->pAig) ); Vec_PtrFree( vCubes ); } diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 13e0b23c..f9a14a07 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -271,7 +271,9 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio p->vPrio = vPrioInit; else if ( pPars->fFlopPrio ) p->vPrio = Pdr_ManDeriveFlopPriorities(pAig, 1); - else + else if ( p->pPars->fNewXSim ) + p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) ); + else p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) ); p->vLits = Vec_IntAlloc( 100 ); // array of literals p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves diff --git a/src/proof/pdr/pdrTsim2.c b/src/proof/pdr/pdrTsim2.c index 82e9a56c..8a86eecc 100644 --- a/src/proof/pdr/pdrTsim2.c +++ b/src/proof/pdr/pdrTsim2.c @@ -36,6 +36,7 @@ struct Txs_Man_t_ Vec_Int_t * vCiVals; // cone leaf values (0/1 CI values) Vec_Int_t * vCoVals; // cone root values (0/1 CO values) Vec_Int_t * vNodes; // cone nodes (node obj IDs) + Vec_Int_t * vTemp; // cone nodes (node obj IDs) Vec_Int_t * vPiLits; // resulting array of PI literals Vec_Int_t * vFfLits; // resulting array of flop literals Pdr_Man_t * pMan; // calling manager @@ -72,6 +73,7 @@ Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values (0/1 CI values) p->vCoVals = Vec_IntAlloc( 100 ); // cone root values (0/1 CO values) p->vNodes = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs) + p->vTemp = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs) p->vPiLits = Vec_IntAlloc( 100 ); // resulting array of PI literals p->vFfLits = Vec_IntAlloc( 100 ); // resulting array of flop literals p->pMan = pMan; // calling manager @@ -85,6 +87,7 @@ void Txs_ManStop( Txs_Man_t * p ) Vec_IntFree( p->vCiVals ); Vec_IntFree( p->vCoVals ); Vec_IntFree( p->vNodes ); + Vec_IntFree( p->vTemp ); Vec_IntFree( p->vPiLits ); Vec_IntFree( p->vFfLits ); ABC_FREE( p ); @@ -143,7 +146,8 @@ void Txs_ManForwardPass( Gia_Man_t * p, Vec_Int_t * vPrio, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals ) { - Gia_Obj_t * pObj, * pFan0, * pFan1; int i; + Gia_Obj_t * pObj, * pFan0, * pFan1; + int i, value0, value1; pObj = Gia_ManConst0(p); pObj->fMark0 = 0; pObj->fMark1 = 0; @@ -158,15 +162,17 @@ void Txs_ManForwardPass( Gia_Man_t * p, { pFan0 = Gia_ObjFanin0(pObj); pFan1 = Gia_ObjFanin1(pObj); - pObj->fMark0 = (pFan0->fMark0 ^ Gia_ObjFaninC0(pObj)) & (pFan1->fMark0 ^ Gia_ObjFaninC1(pObj)); + value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj); + value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj); + pObj->fMark0 = value0 && value1; pObj->fMark1 = 0; if ( pObj->fMark0 ) pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value ); - else if ( pFan0->fMark0 ) + else if ( value0 ) pObj->Value = pFan1->Value; - else if ( pFan1->fMark0 ) + else if ( value1 ) pObj->Value = pFan0->Value; - else // if ( pFan0->fMark0 == 0 && pFan1->fMark0 == 0 ) + else // if ( value0 == 0 && value1 == 0 ) pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value ); assert( ~pObj->Value ); } @@ -202,9 +208,9 @@ static inline int Txs_ObjIsJust( Gia_Man_t * p, Gia_Obj_t * pObj ) assert( !pObj->fMark0 ); assert( !value0 || !value1 ); if ( value0 ) - return pFan1->fMark1; + return pFan1->fMark1 || Gia_ObjIsPi(p, pFan1); if ( value1 ) - return pFan0->fMark1; + return pFan0->fMark1 || Gia_ObjIsPi(p, pFan0); assert( !value0 && !value1 ); return pFan0->fMark1 || pFan1->fMark1 || Gia_ObjIsPi(p, pFan0) || Gia_ObjIsPi(p, pFan1); } @@ -215,6 +221,7 @@ void Txs_ManBackwardPass( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes { if ( !pObj->fMark1 ) continue; + pObj->fMark1 = 0; pFan0 = Gia_ObjFanin0(pObj); pFan1 = Gia_ObjFanin1(pObj); if ( pObj->fMark0 ) @@ -265,6 +272,156 @@ void Txs_ManBackwardPass( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes assert( Vec_IntSize(vFfLits) > 0 ); } +/**Function************************************************************* + + Synopsis [Collects justification path.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Txs_ManSelectJustPath( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vRes ) +{ + Gia_Obj_t * pObj, * pFan0, * pFan1; + int i, value0, value1; + // mark CO drivers + Gia_ManForEachObjVec( vCoObjs, p, pObj, i ) + Gia_ObjFanin0(pObj)->fMark1 = 1; + // collect just paths + Vec_IntClear( vRes ); + Gia_ManForEachObjVecReverse( vNodes, p, pObj, i ) + { + if ( !pObj->fMark1 ) + continue; + pObj->fMark1 = 0; + Vec_IntPush( vRes, Gia_ObjId(p, pObj) ); + pFan0 = Gia_ObjFanin0(pObj); + pFan1 = Gia_ObjFanin1(pObj); + if ( pObj->fMark0 ) + { + pFan0->fMark1 = 1; + pFan1->fMark1 = 1; + continue; + } + value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj); + value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj); + assert( !value0 || !value1 ); + if ( value0 ) + pFan1->fMark1 = 1; + else if ( value1 ) + pFan0->fMark1 = 1; + else // if ( !value0 && !value1 ) + { + pFan0->fMark1 = 1; + pFan1->fMark1 = 1; + } + } + Vec_IntReverseOrder( vRes ); +} +void Txs_ManCollectJustPis( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vPiLits ) +{ + Gia_Obj_t * pObj; int i; + Vec_IntClear( vPiLits ); + Gia_ManForEachObjVec( vCiObjs, p, pObj, i ) + if ( pObj->fMark1 && Gia_ObjIsPi(p, pObj) ) + Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj), !pObj->fMark0) ); +} +void Txs_ManInitPrio( Gia_Man_t * p, Vec_Int_t * vCiObjs ) +{ + Gia_Obj_t * pObj; int i; + Gia_ManConst0(p)->Value = 0x7FFFFFFF; + Gia_ManForEachObjVec( vCiObjs, p, pObj, i ) + pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Gia_ObjCioId(pObj) - Gia_ManPiNum(p); +} +void Txs_ManPropagatePrio( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Int_t * vPrio ) +{ + Gia_Obj_t * pObj, * pFan0, * pFan1; + int i, value0, value1; + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + { + pFan0 = Gia_ObjFanin0(pObj); + pFan1 = Gia_ObjFanin1(pObj); + if ( pObj->fMark0 ) + { +// pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value ); + if ( pFan0->Value == 0x7FFFFFFF ) + pObj->Value = pFan1->Value; + else if ( pFan1->Value == 0x7FFFFFFF ) + pObj->Value = pFan0->Value; + else if ( Vec_IntEntry(vPrio, pFan0->Value) < Vec_IntEntry(vPrio, pFan1->Value) ) + pObj->Value = pFan0->Value; + else + pObj->Value = pFan1->Value; + continue; + } + value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj); + value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj); + assert( !value0 || !value1 ); + if ( value0 ) + pObj->Value = pFan1->Value; + else if ( value1 ) + pObj->Value = pFan0->Value; + else // if ( value0 == 0 && value1 == 0 ) + { +// pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value ); + if ( pFan0->Value == 0x7FFFFFFF || pFan1->Value == 0x7FFFFFFF ) + pObj->Value = 0x7FFFFFFF; + else if ( Vec_IntEntry(vPrio, pFan0->Value) >= Vec_IntEntry(vPrio, pFan1->Value) ) + pObj->Value = pFan0->Value; + else + pObj->Value = pFan1->Value; + } + assert( ~pObj->Value ); + } +} +int Txs_ManFindMinId( Gia_Man_t * p, Vec_Int_t * vCoObjs, Vec_Int_t * vPrio ) +{ + Gia_Obj_t * pObj; int i, iMinId = -1; + Gia_ManForEachObjVec( vCoObjs, p, pObj, i ) + if ( Gia_ObjFanin0(pObj)->Value != 0x7FFFFFFF ) + { + if ( iMinId == -1 || Vec_IntEntry(vPrio, iMinId) > Vec_IntEntry(vPrio, Gia_ObjFanin0(pObj)->Value) ) + iMinId = Gia_ObjFanin0(pObj)->Value; + } + return iMinId; +} +void Txs_ManFindCiReduction( Gia_Man_t * p, + Vec_Int_t * vPrio, Vec_Int_t * vCiObjs, + Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, + Vec_Int_t * vPiLits, Vec_Int_t * vFfLits, Vec_Int_t * vTemp ) +{ + Gia_Obj_t * pObj; + int iPrioCi; + // propagate PI influence + Txs_ManSelectJustPath( p, vNodes, vCoObjs, vTemp ); + Txs_ManCollectJustPis( p, vCiObjs, vPiLits ); +// printf( "%d -> %d ", Vec_IntSize(vNodes), Vec_IntSize(vTemp) ); + // iteratively detect and remove smallest IDs + Vec_IntClear( vFfLits ); + Txs_ManInitPrio( p, vCiObjs ); + while ( 1 ) + { + Txs_ManPropagatePrio( p, vTemp, vPrio ); + iPrioCi = Txs_ManFindMinId( p, vCoObjs, vPrio ); + if ( iPrioCi == -1 ) + break; + pObj = Gia_ManCi( p, Gia_ManPiNum(p)+iPrioCi ); + Vec_IntPush( vFfLits, Abc_Var2Lit(iPrioCi, !pObj->fMark0) ); + pObj->Value = 0x7FFFFFFF; + } +} +void Txs_ManPrintFlopLits( Vec_Int_t * vFfLits, Vec_Int_t * vPrio ) +{ + int i, Entry; + printf( "%3d : ", Vec_IntSize(vFfLits) ); + Vec_IntForEachEntry( vFfLits, Entry, i ) + printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "+":"-", Abc_Lit2Var(Entry), Vec_IntEntry(vPrio, Abc_Lit2Var(Entry)) ); + printf( "\n" ); +} + /**Function************************************************************* Synopsis [Verify the result.] @@ -332,6 +489,7 @@ void Txs_ManVerify( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_ ***********************************************************************/ Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube ) { + int fTryNew = 1; Pdr_Set_t * pRes; Gia_Obj_t * pObj; // collect CO objects @@ -370,7 +528,10 @@ Abc_Print( 1, " in frame %d.\n", k ); // perform two passes Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals ); - Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits ); + if ( fTryNew ) + Txs_ManFindCiReduction( p->pGia, p->vPrio, p->vCiObjs, p->vNodes, p->vCoObjs, p->vPiLits, p->vFfLits, p->vTemp ); + else + Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits ); Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals ); // derive the final set diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index 21fea429..a6613891 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/src/sat/bmc/bmcCexCare.c @@ -158,7 +158,7 @@ void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, int fGrow, Vec_In SeeAlso [] ***********************************************************************/ -void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin ) +void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, int fGrow, Abc_Cex_t * pCexMin ) { Gia_Obj_t * pObj; int i, Phase0, Phase1; @@ -184,10 +184,33 @@ void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex Gia_ObjFanin0(pObj)->fPhase = 1; else // if ( !Phase0 && !Phase1 ) { - if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) <= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) ) + if ( Gia_ObjFanin0(pObj)->fPhase || Gia_ObjFanin1(pObj)->fPhase ) + continue; + if ( Gia_ObjIsPi(p, Gia_ObjFanin0(pObj)) ) Gia_ObjFanin0(pObj)->fPhase = 1; - else + else if ( Gia_ObjIsPi(p, Gia_ObjFanin1(pObj)) ) Gia_ObjFanin1(pObj)->fPhase = 1; +// else if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && Txs_ObjIsJust(p, Gia_ObjFanin0(pObj)) ) +// Gia_ObjFanin0(pObj)->fPhase = 1; +// else if ( Gia_ObjIsAnd(Gia_ObjFanin1(pObj)) && Txs_ObjIsJust(p, Gia_ObjFanin1(pObj)) ) +// Gia_ObjFanin1(pObj)->fPhase = 1; + else + { + if ( fGrow & 1 ) + { + if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) >= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) ) + Gia_ObjFanin0(pObj)->fPhase = 1; + else + Gia_ObjFanin1(pObj)->fPhase = 1; + } + else + { + if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) <= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) ) + Gia_ObjFanin0(pObj)->fPhase = 1; + else + Gia_ObjFanin1(pObj)->fPhase = 1; + } + } } } Gia_ManForEachPi( p, pObj, i ) @@ -210,7 +233,7 @@ Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t Gia_ManForEachRo( p, pObj, i ) pObj->Value = Vec_IntEntry( vPrios, f * pCex->nRegs + i ); Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow ); - Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin ); + Bmc_CexCarePropagateBwdOne( p, pCex, f, fGrow, pCexMin ); Gia_ManForEachRiRo( p, pObjRi, pObjRo, i ) pObjRi->fPhase = pObjRo->fPhase; } -- cgit v1.2.3