From adcc398bc38c91fa4cc8849aca9eb69c6fb61d21 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 26 Jun 2022 19:45:03 -0700 Subject: Dumping equivalences after SAT sweeping. --- src/aig/miniaig/miniaig.h | 14 +++++ src/base/abci/abc.c | 20 +++++-- src/misc/vec/vecWrd.h | 8 +++ src/proof/acec/acecXor.c | 1 + src/proof/cec/cecSatG2.c | 135 +++++++++++++++++++++++++++++++++++++++++++++- 5 files changed, 172 insertions(+), 6 deletions(-) diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index c501d326..0365b946 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -368,6 +368,20 @@ static inline int Mini_AigTruth( Mini_Aig_t * p, int * pVarLits, int nVars, unsi Lit1 = Mini_AigTruth( p, pVarLits, Var, Mini_AigTt5Cofactor1(Truth, Var) ); return Mini_AigMuxProp( p, pVarLits[Var], Lit1, Lit0 ); } +static char * Mini_AigPhase( Mini_Aig_t * p ) +{ + char * pRes = MINI_AIG_CALLOC( char, Mini_AigNodeNum(p) ); + int i; + Mini_AigForEachAnd( p, i ) + { + int iFaninLit0 = Mini_AigNodeFanin0( p, i ); + int iFaninLit1 = Mini_AigNodeFanin1( p, i ); + int Phase0 = pRes[Mini_AigLit2Var(iFaninLit0)] ^ Mini_AigLitIsCompl(iFaninLit0); + int Phase1 = pRes[Mini_AigLit2Var(iFaninLit1)] ^ Mini_AigLitIsCompl(iFaninLit1); + pRes[i] = Phase0 & Phase1; + } + return pRes; +} // procedure to check the topological order during AIG construction static int Mini_AigCheck( Mini_Aig_t * p ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f1c8cc7f..33a8315c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37195,13 +37195,14 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Gia_Man_t * Cec2_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec3_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern void Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose ); extern Gia_Man_t * Cec5_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars, int fCbs, int approxLim, int subBatchSz, int adaRecycle ); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp; - int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0; + int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoX = 0, fUseAlgoY = 0, fUseSave = 0; int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxywvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxyswvh" ) ) != EOF ) { switch ( c ) { @@ -37331,6 +37332,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'y': fUseAlgoY ^= 1; break; + case 's': + fUseSave ^= 1; + break; case 'w': pPars->fVeryVerbose ^= 1; break; @@ -37346,7 +37350,12 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" ); return 1; } - if ( fUseAlgo ) + if ( fUseSave ) + { + Cec4_ManSimulateTest5( pAbc->pGia, pPars->nBTLimit, pPars->fVerbose ); + return 0; + } + else if ( fUseAlgo ) pTemp = Cec2_ManSimulateTest( pAbc->pGia, pPars ); else if ( fUseAlgoG ) pTemp = Cec3_ManSimulateTest( pAbc->pGia, pPars ); @@ -37354,7 +37363,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pTemp = Cec4_ManSimulateTest( pAbc->pGia, pPars ); else if ( fUseAlgoY ) pTemp = Cec5_ManSimulateTest( pAbc->pGia, pPars, fCbs, approxLim, subBatchSz, adaRecycle ); - else + else pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 ); if ( pAbc->pGia->pCexSeq != NULL ) { @@ -37366,7 +37375,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-JWRILDCNP ] [-rmdckngxywvh]\n" ); + Abc_Print( -2, "usage: &fraig [-JWRILDCNP ] [-rmdckngxyswvh]\n" ); Abc_Print( -2, "\t performs combinational SAT sweeping\n" ); Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType ); Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords ); @@ -37386,6 +37395,7 @@ usage: Abc_Print( -2, "\t-g : toggle using another new implementation [default = %s]\n", fUseAlgoG? "yes": "no" ); Abc_Print( -2, "\t-x : toggle using another new implementation [default = %s]\n", fUseAlgoX? "yes": "no" ); Abc_Print( -2, "\t-y : toggle using another new implementation [default = %s]\n", fUseAlgoY? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle dumping equivalences into a file [default = %s]\n", fUseSave? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "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"); diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index 8275702a..fdbb1866 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -195,6 +195,14 @@ static inline Vec_Wrd_t * Vec_WrdStartTruthTables( int nVars ) } return p; } +static inline int Vec_WrdShiftOne( Vec_Wrd_t * p, int nWords ) +{ + int i, nObjs = p->nSize/nWords; + assert( nObjs * nWords == p->nSize ); + for ( i = 0; i < nObjs; i++ ) + p->pArray[i*nWords] <<= 1; + return nObjs; +} /**Function************************************************************* diff --git a/src/proof/acec/acecXor.c b/src/proof/acec/acecXor.c index 963ea15b..49d0a58f 100644 --- a/src/proof/acec/acecXor.c +++ b/src/proof/acec/acecXor.c @@ -466,6 +466,7 @@ void Gia_ManTestXor( Gia_Man_t * p ) } Vec_WrdFree( vSimsPi ); Vec_WrdFree( vSims ); + nWords = 0; } //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index ce299c66..2bbc03d2 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1877,9 +1877,9 @@ void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) abctime clk = Abc_Clock(); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Cec4_ManSetParams( pPars ); - Cec4_ManPerformSweeping( p, pPars, NULL, 0 ); pPars->fVerbose = fVerbose; pPars->nBTLimit = nConfs; + Cec4_ManPerformSweeping( p, pPars, NULL, 0 ); if ( fVerbose ) Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk ); } @@ -1912,6 +1912,139 @@ int Cec4_ManSimulateOnlyTest( Gia_Man_t * p, int fVerbose ) return Cec4_ManPerformSweeping( p, pPars, NULL, 1 ); } +/**Function************************************************************* + + Synopsis [Internal simulation APIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec4_ManSimulateTest5Int( Gia_Man_t * p, int nConfs, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + pPars->fVerbose = fVerbose; + pPars->nBTLimit = nConfs; + Cec4_ManPerformSweeping( p, pPars, NULL, 0 ); + if ( fVerbose ) + Abc_PrintTime( 1, "Equivalence detection time", Abc_Clock() - clk ); +} +Gia_Man_t * Gia_ManLocalRehash( Gia_Man_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManForEachObj1( p, pObj, i ) + { + int iLitNew = Gia_ManObj(pTemp, Abc_Lit2Var(pObj->Value))->Value; + if ( iLitNew == ~0 ) + pObj->Value = iLitNew; + else + pObj->Value = Abc_LitNotCond(iLitNew, Abc_LitIsCompl(pObj->Value)); + } + Gia_ManStop( pTemp ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} +Vec_Int_t * Cec4_ManComputeMapping( Gia_Man_t * p, Gia_Man_t * pAig, int fVerbose ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vReprs = Vec_IntStartFull( Gia_ManObjNum(p) ); + int * pAig2Abc = ABC_FALLOC( int, Gia_ManObjNum(pAig) ); + int i, nConsts = 0, nReprs = 0; + pAig2Abc[0] = 0; + Gia_ManForEachCand( p, pObj, i ) + { + int iLitGia = pObj->Value, iReprGia; + if ( iLitGia == -1 ) + continue; + iReprGia = Gia_ObjReprSelf( pAig, Abc_Lit2Var(iLitGia) ); + if ( pAig2Abc[iReprGia] == -1 ) + pAig2Abc[iReprGia] = i; + else + { + int iLitGia2 = Gia_ManObj(p, pAig2Abc[iReprGia] )->Value; + assert( Gia_ObjReprSelf(pAig, Abc_Lit2Var(iLitGia)) == Gia_ObjReprSelf(pAig, Abc_Lit2Var(iLitGia2)) ); + assert( i > pAig2Abc[iReprGia] ); + Vec_IntWriteEntry( vReprs, i, pAig2Abc[iReprGia] ); + if ( pAig2Abc[iReprGia] == 0 ) + nConsts++; + else + nReprs++; + } + } + ABC_FREE( pAig2Abc ); + if ( fVerbose ) + printf( "Found %d const reprs and %d other reprs.\n", nConsts, nReprs ); + return vReprs; +} +void Cec4_ManVerifyEquivs( Gia_Man_t * p, Vec_Int_t * vRes, int fVerbose ) +{ + int i, iRepr, nWords = 4; word * pSim0, * pSim1; + Vec_Wrd_t * vSimsCi = Vec_WrdStartRandom( Gia_ManCiNum(p) * nWords ); + int nObjs = Vec_WrdShiftOne( vSimsCi, nWords ), nFails = 0; + Vec_Wrd_t * vSims = Gia_ManSimPatSimOut( p, vSimsCi, 0 ); + assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) ); + assert( nObjs == Gia_ManCiNum(p) ); + Vec_IntForEachEntry( vRes, iRepr, i ) + { + if ( iRepr == -1 ) + continue; + assert( i > iRepr ); + pSim0 = Vec_WrdEntryP( vSims, nWords*i ); + pSim1 = Vec_WrdEntryP( vSims, nWords*iRepr ); + if ( (pSim0[0] ^ pSim1[0]) & 1 ) + nFails += !Abc_TtOpposite(pSim0, pSim1, nWords); + else + nFails += !Abc_TtEqual(pSim0, pSim1, nWords); + } + Vec_WrdFree( vSimsCi ); + Vec_WrdFree( vSims ); + if ( nFails ) + printf( "Verification failed at %d nodes.\n", nFails ); + else if ( fVerbose ) + printf( "Verification succeeded for all (%d) nodes.\n", Gia_ManCandNum(p) ); +} +void Cec4_ManConvertToLits( Gia_Man_t * p, Vec_Int_t * vRes ) +{ + Gia_Obj_t * pObj; int i, iRepr; + Gia_ManSetPhase( p ); + Gia_ManForEachObj( p, pObj, i ) + if ( (iRepr = Vec_IntEntry(vRes, i)) >= 0 ) + Vec_IntWriteEntry( vRes, i, Abc_Var2Lit(iRepr, Gia_ManObj(p, iRepr)->fPhase ^ pObj->fPhase) ); +} +void Cec4_ManSimulateTest5( Gia_Man_t * p, int nConfs, int fVerbose ) +{ + Vec_Int_t * vRes = NULL; + Gia_Man_t * pAig = Gia_ManLocalRehash( p ); + Cec4_ManSimulateTest5Int( pAig, nConfs, fVerbose ); + vRes = Cec4_ManComputeMapping( p, pAig, fVerbose ); + Cec4_ManVerifyEquivs( p, vRes, fVerbose ); + Cec4_ManConvertToLits( p, vRes ); + Vec_IntDumpBin( "_temp_.equiv", vRes, fVerbose ); + Vec_IntFree( vRes ); + Gia_ManStop( pAig ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3