From bf96f0b31d255f56a355a92cb0fc2867eff68e9a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 1 Jan 2021 00:44:02 -0800 Subject: Experiments with simulation. --- src/proof/cec/cecSim.c | 51 ++++++++++++++++++++++++-------------------------- 1 file changed, 24 insertions(+), 27 deletions(-) (limited to 'src/proof/cec/cecSim.c') diff --git a/src/proof/cec/cecSim.c b/src/proof/cec/cecSim.c index 88e3b4c7..33bc11f5 100644 --- a/src/proof/cec/cecSim.c +++ b/src/proof/cec/cecSim.c @@ -227,8 +227,8 @@ int Cec_ManSRunPropagate( Cec_ManS_t * p, int iNode ) return 0; } p->nVisited++; - Cec_ManSRunImply( p, iFan0 ); - Cec_ManSRunImply( p, iFan1 ); + //Cec_ManSRunImply( p, iFan0 ); + //Cec_ManSRunImply( p, iFan1 ); { word * pSim__ = Cec_ManSSim( p, 0, 0 ); word * pSim00 = Cec_ManSSim( p, iFan0, Gia_ObjFaninC0(pNode) ); @@ -238,46 +238,43 @@ int Cec_ManSRunPropagate( Cec_ManS_t * p, int iNode ) 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]); + pSim01[0] |= pSim_1[0]; + pSim11[0] |= pSim_1[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]; + pSim00[0] |= pSim_0[0] & (pSim11[0] | ~p->Rands[p->iRand]); + pSim10[0] |= pSim_0[0] & (pSim01[0] | p->Rands[p->iRand]); pSim__[0] |= pSim00[0] & pSim01[0]; pSim__[0] |= pSim10[0] & pSim11[0]; + + pSim00[0] &= ~pSim__[0]; + pSim01[0] &= ~pSim__[0]; + pSim10[0] &= ~pSim__[0]; + pSim11[0] &= ~pSim__[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]; + 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_TtOr( pSim01, pSim01, pSim_1, p->nWords ); + Abc_TtOr( pSim11, pSim11, pSim_1, 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_TtOr( p->pTemp[1], pSim11, p->pTemp[0], p->nWords ); + Abc_TtOrAnd( pSim00, pSim_0, p->pTemp[1], 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_TtNot( p->pTemp[0], p->nWords ); + Abc_TtOr( p->pTemp[1], pSim01, p->pTemp[0], p->nWords ); + Abc_TtOrAnd( pSim10, pSim_0, p->pTemp[1], p->nWords ); Abc_TtOrAnd( pSim__, pSim00, pSim01, p->nWords ); Abc_TtOrAnd( pSim__, pSim10, pSim11, p->nWords ); + + Abc_TtAndSharp( pSim00, pSim00, pSim__, p->nWords, 1 ); + Abc_TtAndSharp( pSim01, pSim01, pSim__, p->nWords, 1 ); + Abc_TtAndSharp( pSim10, pSim10, pSim__, p->nWords, 1 ); + Abc_TtAndSharp( pSim11, pSim11, pSim__, p->nWords, 1 ); } } return 1; -- cgit v1.2.3