From d0efef2fe958ca093b06ad4be739ffdcb44c4d28 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 30 Dec 2020 11:24:35 -0800 Subject: Experiments with simulation. --- src/proof/cec/cecSim.c | 363 ++++++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 360 insertions(+), 3 deletions(-) (limited to 'src/proof/cec/cecSim.c') diff --git a/src/proof/cec/cecSim.c b/src/proof/cec/cecSim.c index 92f8fc2e..88e3b4c7 100644 --- a/src/proof/cec/cecSim.c +++ b/src/proof/cec/cecSim.c @@ -6,7 +6,7 @@ PackageName [Combinational equivalence checking.] - Synopsis [Simulation manager.] + Synopsis [Simulation.] Author [Alan Mishchenko] @@ -19,14 +19,40 @@ ***********************************************************************/ #include "cecInt.h" +#include "aig/gia/giaAig.h" +#include "misc/util/utilTruth.h" -ABC_NAMESPACE_IMPL_START +ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define SIM_RANDS 113 + +typedef struct Cec_ManS_t_ Cec_ManS_t; +struct Cec_ManS_t_ +{ + int nWords; + int nLevelMax; + int nLevelMin; + int iRand; + Gia_Man_t * pAig; + Vec_Int_t * vInputs; + Vec_Wec_t * vLevels; + Vec_Wrd_t * vSims; + word * pTemp[4]; + word Rands[SIM_RANDS]; + int nSkipped; + int nVisited; + int nCexes; + abctime clkSat; + abctime clkUnsat; +}; + +static inline word * Cec_ManSSim( Cec_ManS_t * p, int iNode, int Value ) { return Vec_WrdEntryP(p->vSims, p->nWords*(iNode+iNode+Value)); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -36,12 +62,343 @@ ABC_NAMESPACE_IMPL_START Synopsis [] Description [] - + SideEffects [] SeeAlso [] ***********************************************************************/ +Cec_ManS_t * Cec_ManSStart( Gia_Man_t * pAig, int nWords ) +{ + Cec_ManS_t * p; int i; + p = ABC_ALLOC( Cec_ManS_t, 1 ); + memset( p, 0, sizeof(Cec_ManS_t) ); + p->nWords = nWords; + p->pAig = pAig; + p->vInputs = Vec_IntAlloc( 100 ); + p->vLevels = Vec_WecStart( Gia_ManLevelNum(pAig) + 1 ); + p->vSims = Vec_WrdStart( Gia_ManObjNum(pAig) * nWords * 2 ); + p->pTemp[0] = ABC_ALLOC( word, 4*nWords ); + for ( i = 1; i < 4; i++ ) + p->pTemp[i] = p->pTemp[i-1] + nWords; + for ( i = 0; i < SIM_RANDS; i++ ) + p->Rands[i] = Gia_ManRandomW(0); + return p; +} +void Cec_ManSStop( Cec_ManS_t * p ) +{ + Vec_IntFree( p->vInputs ); + Vec_WecFree( p->vLevels ); + Vec_WrdFree( p->vSims ); + ABC_FREE( p->pTemp[0] ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Verify counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Cec_ManSVerify_rec( Gia_Man_t * p, int iObj ) +{ + int Value0, Value1; + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( iObj == 0 ) return 0; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return pObj->fMark1; + Gia_ObjSetTravIdCurrentId(p, iObj); + if ( Gia_ObjIsCi(pObj) ) + return pObj->fMark1; + assert( Gia_ObjIsAnd(pObj) ); + Value0 = Cec_ManSVerify_rec( p, Gia_ObjFaninId0(pObj, iObj) ) ^ Gia_ObjFaninC0(pObj); + Value1 = Cec_ManSVerify_rec( p, Gia_ObjFaninId1(pObj, iObj) ) ^ Gia_ObjFaninC1(pObj); + return pObj->fMark1 = Gia_ObjIsXor(pObj) ? Value0 ^ Value1 : Value0 & Value1; +} +void Cec_ManSVerifyTwo( Gia_Man_t * p, int iObj0, int iObj1 ) +{ + int Value0, Value1; + Gia_ManIncrementTravId( p ); + Value0 = Cec_ManSVerify_rec( p, iObj0 ); + Value1 = Cec_ManSVerify_rec( p, iObj1 ); + if ( (Value0 ^ Value1) == Gia_ObjPhaseDiff(p, iObj0, iObj1) ) + printf( "CEX verification FAILED for obj %d and obj %d.\n", iObj0, iObj1 ); +// else +// printf( "CEX verification succeeded for obj %d and obj %d.\n", iObj0, iObj1 );; +} +void Cec_ManSVerify( Cec_ManS_t * p, int iObj0, int iObj1 ) +{ + int fDoVerify = 0; + int w, i, iObj, nCares; + word * pCare = Vec_WrdArray(p->vSims); + if ( Vec_IntSize(p->vInputs) == 0 ) + { + printf( "No primary inputs.\n" ); + return; + } + Vec_IntForEachEntry( p->vInputs, iObj, i ) + { + word * pSim_0 = Cec_ManSSim( p, iObj, 0 ); + word * pSim_1 = Cec_ManSSim( p, iObj, 1 ); + if ( p->nWords == 1 ) + pCare[0] |= pSim_0[0] & pSim_1[0]; + else + Abc_TtOrAnd( pCare, pSim_0, pSim_1, p->nWords ); + } + nCares = Abc_TtCountOnesVec( pCare, p->nWords ); + if ( nCares == 64*p->nWords ) + { + printf( "No CEXes.\n" ); + return; + } + assert( Vec_IntSize(p->vInputs) > 0 ); + for ( w = 0; w < 64*p->nWords; w++ ) + { + if ( Abc_TtGetBit(pCare, w) ) + continue; + if ( !fDoVerify ) + continue; + Vec_IntForEachEntry( p->vInputs, iObj, i ) + Gia_ManObj(p->pAig, iObj)->fMark1 = Abc_TtGetBit( Cec_ManSSim(p, iObj, 1), w ); + Cec_ManSVerifyTwo( p->pAig, iObj0, iObj1 ); + } + printf( "Considered %d CEXes of nodes %d and %d.\n", 64*p->nWords - nCares, iObj0, iObj1 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec_ManSRunImply( Cec_ManS_t * p, int iNode ) +{ + Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode ); + if ( Gia_ObjIsAnd(pNode) ) + { + int iFan0 = Gia_ObjFaninId0( pNode, iNode ); + int iFan1 = Gia_ObjFaninId1( pNode, iNode ); + word * pSim__ = Cec_ManSSim( p, 0, 0 ); + word * pSim_0 = Cec_ManSSim( p, iNode, 0 ); + word * pSim_1 = Cec_ManSSim( p, iNode, 1 ); + word * pSim00 = Cec_ManSSim( p, iFan0, Gia_ObjFaninC0(pNode) ); + word * pSim01 = Cec_ManSSim( p, iFan0, !Gia_ObjFaninC0(pNode) ); + word * pSim10 = Cec_ManSSim( p, iFan1, Gia_ObjFaninC1(pNode) ); + word * pSim11 = Cec_ManSSim( p, iFan1, !Gia_ObjFaninC1(pNode) ); + if ( p->nWords == 1 ) + { + pSim_0[0] |= pSim00[0] | pSim10[0]; + pSim_1[0] |= pSim01[0] & pSim11[0]; + pSim__[0] |= pSim_0[0] & pSim_1[0]; + pSim_0[0] &= ~pSim__[0]; + pSim_1[0] &= ~pSim__[0]; + } + else + { + Abc_TtOr( pSim_0, pSim_0, pSim00, p->nWords ); + Abc_TtOr( pSim_0, pSim_0, pSim10, p->nWords ); + Abc_TtOrAnd( pSim_1, pSim01, pSim11, p->nWords ); + Abc_TtOrAnd( pSim__, pSim_0, pSim_1, p->nWords ); + Abc_TtAndSharp( pSim_0, pSim_0, pSim__, p->nWords, 1 ); + Abc_TtAndSharp( pSim_1, pSim_1, pSim__, p->nWords, 1 ); + } + } +} +int Cec_ManSRunPropagate( Cec_ManS_t * p, int iNode ) +{ + Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode ); + int iFan0 = Gia_ObjFaninId0( pNode, iNode ); + int iFan1 = Gia_ObjFaninId1( pNode, iNode ); + word * pSim_0 = Cec_ManSSim( p, iNode, 0 ); + word * pSim_1 = Cec_ManSSim( p, iNode, 1 ); + if ( Abc_TtIsConst0(pSim_0, p->nWords) && Abc_TtIsConst0(pSim_1, p->nWords) ) + { + p->nSkipped++; + return 0; + } + p->nVisited++; + Cec_ManSRunImply( p, iFan0 ); + Cec_ManSRunImply( p, iFan1 ); + { + word * pSim__ = Cec_ManSSim( p, 0, 0 ); + word * pSim00 = Cec_ManSSim( p, iFan0, Gia_ObjFaninC0(pNode) ); + word * pSim01 = Cec_ManSSim( p, iFan0, !Gia_ObjFaninC0(pNode) ); + word * pSim10 = Cec_ManSSim( p, iFan1, Gia_ObjFaninC1(pNode) ); + word * pSim11 = Cec_ManSSim( p, iFan1, !Gia_ObjFaninC1(pNode) ); + p->iRand = p->iRand == SIM_RANDS-1 ? 0 : p->iRand + 1; + if ( p->nWords == 1 ) + { + pSim__[0] |= pSim_0[0] & pSim01[0] & pSim11[0]; + pSim__[0] |= pSim_1[0] & (pSim00[0] | pSim10[0]); + + pSim00[0] |= pSim_0[0] & ~pSim__[0] & (pSim01[0] | ~p->Rands[p->iRand]); + pSim10[0] |= pSim_0[0] & ~pSim__[0] & (pSim11[0] | p->Rands[p->iRand]); + + pSim01[0] |= pSim_1[0] & ~pSim__[0]; + pSim11[0] |= pSim_1[0] & ~pSim__[0]; + + pSim__[0] |= pSim00[0] & pSim01[0]; + pSim__[0] |= pSim10[0] & pSim11[0]; + } + else + { + int w; + + Abc_TtAnd( p->pTemp[0], pSim01, pSim11, p->nWords, 0 ); + Abc_TtOrAnd( pSim__, pSim_0, p->pTemp[0], p->nWords ); + + Abc_TtOr( p->pTemp[0], pSim00, pSim10, p->nWords ); + Abc_TtOrAnd( pSim__, pSim_1, p->pTemp[0], p->nWords ); + + //Abc_TtVec( p->pTemp[0], p->nWords, p->Rands[p->iRand] ); + for ( w = 0; w < p->nWords; w++ ) + p->pTemp[0][w] = p->Rands[(p->iRand + w) % SIM_RANDS]; + + Abc_TtAndCompl( p->pTemp[1], pSim01, 1, p->pTemp[0], 0, p->nWords ); + Abc_TtAndCompl( p->pTemp[2], pSim__, 1, p->pTemp[1], 1, p->nWords ); + Abc_TtOrAnd( pSim00, pSim_0, p->pTemp[2], p->nWords ); + + Abc_TtAndCompl( p->pTemp[1], pSim11, 1, p->pTemp[0], 1, p->nWords ); + Abc_TtAndCompl( p->pTemp[2], pSim__, 1, p->pTemp[1], 1, p->nWords ); + Abc_TtOrAnd( pSim10, pSim_0, p->pTemp[2], p->nWords ); + + Abc_TtAndSharp( p->pTemp[0], pSim_1, pSim__, p->nWords, 1 ); + Abc_TtOr( pSim01, pSim01, p->pTemp[0], p->nWords ); + Abc_TtOr( pSim11, pSim11, p->pTemp[0], p->nWords ); + + Abc_TtOrAnd( pSim__, pSim00, pSim01, p->nWords ); + Abc_TtOrAnd( pSim__, pSim10, pSim11, p->nWords ); + } + } + return 1; +} +void Cec_ManSInsert( Cec_ManS_t * p, int iNode ) +{ + Gia_Obj_t * pNode; int Level; + assert( iNode > 0 ); + if ( Gia_ObjIsTravIdCurrentId(p->pAig, iNode) ) + return; + Gia_ObjSetTravIdCurrentId(p->pAig, iNode); + pNode = Gia_ManObj( p->pAig, iNode ); + if ( Gia_ObjIsCi(pNode) ) + { + Vec_IntPush( p->vInputs, iNode ); + return; + } + assert( Gia_ObjIsAnd(pNode) ); + Level = Gia_ObjLevelId( p->pAig, iNode ); + assert( Level > 0 ); + Vec_WecPush( p->vLevels, Level, iNode ); + p->nLevelMax = Abc_MaxInt( p->nLevelMax, Level ); + p->nLevelMin = Abc_MinInt( p->nLevelMin, Level ); + assert( p->nLevelMin <= p->nLevelMax ); +} +int Cec_ManSRunSimInt( Cec_ManS_t * p ) +{ + Vec_Int_t * vLevel; + int i, k, iNode, fSolved = 0; + Vec_WecForEachLevelReverseStartStop( p->vLevels, vLevel, i, p->nLevelMax+1, p->nLevelMin ) + { + Vec_IntForEachEntry( vLevel, iNode, k ) + { + Gia_Obj_t * pNode = Gia_ManObj( p->pAig, iNode ); + if ( !fSolved && Cec_ManSRunPropagate( p, iNode ) ) + { + Cec_ManSInsert( p, Gia_ObjFaninId0(pNode, iNode) ); + Cec_ManSInsert( p, Gia_ObjFaninId1(pNode, iNode) ); + if ( Abc_TtIsConst1(Vec_WrdArray(p->vSims), p->nWords) ) + fSolved = 1; + } + Abc_TtClear( Cec_ManSSim(p, iNode, 0), 2*p->nWords ); + } + Vec_IntClear( vLevel ); + } + //Vec_WecForEachLevel( p->vLevels, vLevel, i ) + // assert( Vec_IntSize(vLevel) == 0 ); + return fSolved; +} +int Cec_ManSRunSim( Cec_ManS_t * p, int iNode0, int iNode1 ) +{ + abctime clk = Abc_Clock(); + //Vec_Int_t * vLevel; + int pNodes[2] = { iNode0, iNode1 }; + int i, iNode, Status, fDiff = Gia_ObjPhaseDiff( p->pAig, iNode0, iNode1 ); + word * pSim00 = Cec_ManSSim( p, iNode0, 0 ); + word * pSim01 = Cec_ManSSim( p, iNode0, 1 ); + word * pSim10 = Cec_ManSSim( p, iNode1, fDiff ); + word * pSim11 = Cec_ManSSim( p, iNode1, !fDiff ); + Abc_TtClear( Vec_WrdArray(p->vSims), p->nWords ); + //for ( i = 0; i < Vec_WrdSize(p->vSims); i++ ) + // assert( p->vSims->pArray[i] == 0 ); + assert( Vec_IntSize(p->vInputs) == 0 ); + if ( iNode0 == 0 ) + Abc_TtFill( pSim11, p->nWords ); + else + { + if ( p->nWords == 1 ) + { + pSim00[0] = (word)0xFFFFFFFF; + pSim11[0] = (word)0xFFFFFFFF; + pSim01[0] = pSim00[0] << 32; + pSim10[0] = pSim11[0] << 32; + } + else + { + assert( p->nWords % 2 == 0 ); + Abc_TtFill( pSim00, p->nWords/2 ); + Abc_TtFill( pSim11, p->nWords/2 ); + Abc_TtFill( pSim01 + p->nWords/2, p->nWords/2 ); + Abc_TtFill( pSim10 + p->nWords/2, p->nWords/2 ); + } + } + p->nLevelMin = ABC_INFINITY; + p->nLevelMax = 0; + Gia_ManIncrementTravId( p->pAig ); + if ( iNode0 ) + Cec_ManSInsert( p, iNode0 ); + Cec_ManSInsert( p, iNode1 ); + p->nSkipped = p->nVisited = 0; + Status = Cec_ManSRunSimInt( p ); + if ( Status == 0 ) + p->clkSat += Abc_Clock() - clk; + else + p->clkUnsat += Abc_Clock() - clk; +// if ( Status == 0 ) +// printf( "Solving %6d and %6d. Skipped = %6d. Visited = %6d. Cone = %6d. Min = %3d. Max = %3d.\n", +// iNode0, iNode1, p->nSkipped, p->nVisited, Gia_ManConeSize(p->pAig, pNodes, 2), p->nLevelMin, p->nLevelMax ); + if ( Status == 0 ) + Cec_ManSVerify( p, iNode0, iNode1 ), p->nCexes++; + Vec_IntForEachEntry( p->vInputs, iNode, i ) + Abc_TtClear( Cec_ManSSim(p, iNode, 0), 2*p->nWords ); + Vec_IntClear( p->vInputs ); + return Status; +} +void Cec_ManSRunTest( Gia_Man_t * pAig ) +{ + abctime clk = Abc_Clock(); + Cec_ManS_t * p; + int i, k, nWords = 1; + Gia_ManRandomW( 1 ); + p = Cec_ManSStart( pAig, nWords ); + Gia_ManForEachClass0( p->pAig, i ) + Gia_ClassForEachObj1( p->pAig, i, k ) + Cec_ManSRunSim( p, i, k ); + printf( "Detected %d CEXes. ", p->nCexes ); + Abc_PrintTime( 1, "Time ", Abc_Clock() - clk ); + Abc_PrintTime( 1, "Sat ", p->clkSat ); + Abc_PrintTime( 1, "Unsat", p->clkUnsat ); + Cec_ManSStop( p ); +} //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3