diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-19 19:22:27 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-19 19:22:27 -0800 |
commit | 48f71adacd7727280498f414ad992257c23d76d7 (patch) | |
tree | 0ea6fdbc44c8a917b1a8f5b0e7df9b6b998bf82f | |
parent | c3699a2043e94107dd963d5c49789807c135927c (diff) | |
download | abc-48f71adacd7727280498f414ad992257c23d76d7.tar.gz abc-48f71adacd7727280498f414ad992257c23d76d7.tar.bz2 abc-48f71adacd7727280498f414ad992257c23d76d7.zip |
Integration with several commands.
-rw-r--r-- | src/aig/gia/giaDup.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaEquiv.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 59 | ||||
-rw-r--r-- | src/opt/dar/darScript.c | 7 | ||||
-rw-r--r-- | src/proof/cec/cecChoice.c | 23 | ||||
-rw-r--r-- | src/proof/cec/cecSatG2.c | 44 | ||||
-rw-r--r-- | src/proof/dch/dch.h | 1 | ||||
-rw-r--r-- | src/proof/dch/dchCore.c | 4 |
8 files changed, 119 insertions, 23 deletions
diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4f448c40..ed4b7109 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1327,7 +1327,7 @@ Gia_Man_t * Gia_ManDupMarked( Gia_Man_t * p ) { Gia_Obj_t * pRepr; pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(pNew) ); - for ( i = 0; i < Gia_ManObjNum(p); i++ ) + for ( i = 0; i < Gia_ManObjNum(pNew); i++ ) Gia_ObjSetRepr( pNew, i, GIA_VOID ); Gia_ManForEachObj1( p, pObj, i ) { diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index f7f873cd..c987453f 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -1988,7 +1988,7 @@ Gia_Man_t * Gia_ManEquivToChoices( Gia_Man_t * p, int nSnapshots ) pNew->pReprs = ABC_CALLOC( Gia_Rpr_t, Gia_ManObjNum(p) ); pNew->pNexts = ABC_CALLOC( int, Gia_ManObjNum(p) ); for ( i = 0; i < Gia_ManObjNum(p); i++ ) - Gia_ObjSetRepr( pNew, i, GIA_VOID ); + pNew->pReprs[i].iRepr = GIA_VOID; Gia_ManFillValue( p ); Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7bf97aa6..2819195f 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36284,21 +36284,13 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern void Cec4_ManSetParams( Cec_ParFra_t * pPars ); 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 ); Cec_ParFra_t ParsFra, * pPars = &ParsFra; Gia_Man_t * pTemp; int c, fUseAlgo = 0, fUseAlgoG = 0, fUseAlgoG2 = 0; - Cec_ManFraSetDefaultParams( pPars ); - pPars->jType = 2; // solver type - pPars->fSatSweeping = 1; // conflict limit at a node - pPars->nWords = 4; // simulation words - pPars->nRounds = 10; // simulation rounds - pPars->nItersMax = 2000; // this is a miter - pPars->nBTLimit = 1000000; // use logic cones - pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver - pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver - pPars->nGenIters = 100; // pattern generation iterations + Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPrmdckngxwvh" ) ) != EOF ) { @@ -37034,10 +37026,10 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pFile; Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; char ** pArgvNew; - int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; + int c, nArgcNew, fUseNew = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; Cec_ManCecSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdasxvwh" ) ) != EOF ) { switch ( c ) { @@ -37078,6 +37070,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': pPars->fSilent ^= 1; break; + case 'x': + fUseNew ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -37216,7 +37211,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } // compute the miter - pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, 1, 0, 0, pPars->fVerbose ); + pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, !fUseNew, 0, 0, pPars->fVerbose ); if ( pMiter ) { if ( fDumpMiter ) @@ -37229,8 +37224,23 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) pMiter->vSimsPi = Vec_WrdDup(pGias[0]->vSimsPi); pMiter->nSimWords = pGias[0]->nSimWords; } - pAbc->Status = Cec_ManVerify( pMiter, pPars ); - Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb ); + if ( fUseNew ) + { + abctime clk = Abc_Clock(); + extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose ); + Gia_Man_t * pNew = Cec4_ManSimulateTest3( pMiter, pPars->fVerbose ); + if ( Gia_ManAndNum(pNew) == 0 ) + Abc_Print( 1, "Networks are equivalent. " ); + else + Abc_Print( 1, "Networks are NOT EQUIVALENT. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + Gia_ManStop( pNew ); + } + else + { + pAbc->Status = Cec_ManVerify( pMiter, pPars ); + Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb ); + } Gia_ManStop( pMiter ); } if ( pGias[0] != pAbc->pGia ) @@ -37239,7 +37249,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &cec [-CT num] [-nmdasvwh]\n" ); + Abc_Print( -2, "usage: &cec [-CT num] [-nmdasxvwh]\n" ); Abc_Print( -2, "\t new combinational equivalence checker\n" ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); @@ -37248,6 +37258,7 @@ usage: Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); Abc_Print( -2, "\t-a : toggle writing dual-output miter [default = %s]\n", fDumpMiter? "yes":"no"); Abc_Print( -2, "\t-s : toggle silent operation [default = %s]\n", pPars->fSilent ? "yes":"no"); + Abc_Print( -2, "\t-x : toggle using new solver [default = %s]\n", fUseNew? "yes":"no"); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no"); Abc_Print( -2, "\t-w : toggle printing SAT solver statistics [default = %s]\n", pPars->fVeryVerbose? "yes":"no"); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -40970,7 +40981,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Dch_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfremgcxvh" ) ) != EOF ) { switch ( c ) { @@ -41028,6 +41039,15 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'm': fMinLevel ^= 1; break; + case 'g': + pPars->fUseGia ^= 1; + break; + case 'c': + pPars->fUseCSat ^= 1; + break; + case 'x': + pPars->fUseNew ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -41067,7 +41087,7 @@ int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremvh]\n" ); + Abc_Print( -2, "usage: &dch [-WCS num] [-sptfremgcxvh]\n" ); Abc_Print( -2, "\t computes structural choices using a new approach\n" ); Abc_Print( -2, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords ); Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); @@ -41079,6 +41099,9 @@ usage: Abc_Print( -2, "\t-r : toggle skipping choices with redundant support [default = %s]\n", pPars->fSkipRedSupp? "yes": "no" ); Abc_Print( -2, "\t-e : toggle computing and merging equivalences [default = %s]\n", fEquiv? "yes": "no" ); Abc_Print( -2, "\t-m : toggle minimizing logic level after merging equivalences [default = %s]\n", fMinLevel? "yes": "no" ); + Abc_Print( -2, "\t-g : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle using new choice computation [default = %s]\n", pPars->fUseNew? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c index f8fa3788..684e85e6 100644 --- a/src/opt/dar/darScript.c +++ b/src/opt/dar/darScript.c @@ -848,6 +848,7 @@ pPars->timeSynth = Abc_Clock() - clk; ***********************************************************************/ Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { + extern Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose ); extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ); // extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs ); extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ); @@ -870,15 +871,17 @@ clk = Abc_Clock(); pPars->timeSynth = Abc_Clock() - clk; // perform choice computation - if ( pPars->fUseGia ) + if ( pPars->fUseNew ) + pMan = Cec_ComputeChoicesNew( pGia, pPars->fVerbose ); + else if ( pPars->fUseGia ) pMan = Cec_ComputeChoices( pGia, pPars ); else { pMan = Gia_ManToAigSkip( pGia, 3 ); - Gia_ManStop( pGia ); pMan = Dch_ComputeChoices( pTemp = pMan, pPars ); Aig_ManStop( pTemp ); } + Gia_ManStop( pGia ); // create guidence vPios = Aig_ManOrderPios( pMan, pAig ); diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 49025630..47d6a478 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -401,6 +401,29 @@ Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars ) return pAig; } +/**Function************************************************************* + + Synopsis [Performs computation of AIGs with choices.] + + Description [Takes several AIGs and performs choicing.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Cec_ComputeChoicesNew( Gia_Man_t * pGia, int fVerbose ) +{ + extern void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ); + Aig_Man_t * pAig; + Cec4_ManSimulateTest2( pGia, fVerbose ); + pGia = Gia_ManEquivToChoices( pGia, 3 ); + Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) ); + pAig = Gia_ManToAig( pGia, 1 ); + Gia_ManStop( pGia ); + return pAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 51654cba..122f33d0 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -145,6 +145,30 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +/**Function************************************************************* + + Synopsis [Default parameter settings.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Cec4_ManSetParams( Cec_ParFra_t * pPars ) +{ + memset( pPars, 0, sizeof(Cec_ParFra_t) ); + pPars->jType = 2; // solver type + pPars->fSatSweeping = 1; // conflict limit at a node + pPars->nWords = 4; // simulation words + pPars->nRounds = 10; // simulation rounds + pPars->nItersMax = 2000; // this is a miter + pPars->nBTLimit = 1000000; // use logic cones + pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver + pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver + pPars->nGenIters = 100; // pattern generation iterations +} /**Function************************************************************* @@ -1768,6 +1792,26 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Cec4_ManPerformSweeping( p, pPars, &pNew ); return pNew; } +void Cec4_ManSimulateTest2( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + Cec4_ManPerformSweeping( p, pPars, NULL ); + pPars->fVerbose = fVerbose; + //if ( fVerbose ) + Abc_PrintTime( 1, "New choice computation time", Abc_Clock() - clk ); +} +Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Man_t * pNew = NULL; + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec4_ManSetParams( pPars ); + pPars->fVerbose = fVerbose; + Cec4_ManPerformSweeping( p, pPars, &pNew ); + return pNew; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/proof/dch/dch.h b/src/proof/dch/dch.h index 5d644643..07f6a1d2 100644 --- a/src/proof/dch/dch.h +++ b/src/proof/dch/dch.h @@ -52,6 +52,7 @@ struct Dch_Pars_t_ int fPower; // uses power-aware rewriting int fUseGia; // uses GIA package int fUseCSat; // uses circuit-based solver + int fUseNew; // uses new implementation int fLightSynth; // uses lighter version of synthesis int fSkipRedSupp; // skip choices with redundant support vars int fVerbose; // verbose stats diff --git a/src/proof/dch/dchCore.c b/src/proof/dch/dchCore.c index 0da65bee..eef53e73 100644 --- a/src/proof/dch/dchCore.c +++ b/src/proof/dch/dchCore.c @@ -90,7 +90,7 @@ Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars ) { Dch_Man_t * p; Aig_Man_t * pResult; - abctime clk, clkTotal = Abc_Clock(); + abctime clk, clk2 = Abc_Clock(), clkTotal = Abc_Clock(); // reset random numbers Aig_ManRandom(1); // start the choicing manager @@ -106,6 +106,8 @@ p->timeSimInit = Abc_Clock() - clk; // free memory ahead of time p->timeTotal = Abc_Clock() - clkTotal; Dch_ManStop( p ); + //if ( pPars->fVerbose ) + Abc_PrintTime( 1, "Old choice computation time", Abc_Clock() - clk2 ); // create choices ABC_FREE( pAig->pTable ); pResult = Dch_DeriveChoiceAig( pAig, pPars->fSkipRedSupp ); |