From 53e7d1f9ef0b13e63f2b316c6f1de253fec6f42e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 22 Mar 2018 10:10:09 -0700 Subject: Adding switch 'scorr -f' to dump inductive invariant as an AIG. --- src/aig/saig/saig.h | 2 +- src/aig/saig/saigDup.c | 4 +++- src/base/abci/abc.c | 19 ++++++++++++++----- src/proof/ssw/ssw.h | 1 + src/proof/ssw/sswCore.c | 1 + src/proof/ssw/sswSweep.c | 25 ++++++++++++++++--------- 6 files changed, 36 insertions(+), 16 deletions(-) (limited to 'src') diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 380af64b..16e7fb44 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -126,7 +126,7 @@ extern Aig_Man_t * Saig_ManDupDual( Aig_Man_t * pAig, Vec_Int_t * vDcFlops extern void Saig_ManBlockPo( Aig_Man_t * pAig, int nCycles ); /*=== saigDup.c ==========================================================*/ extern Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * p ); -extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ); +extern Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs, int fAddOuts ); extern Aig_Man_t * Saig_ManDupAbstraction( Aig_Man_t * pAig, Vec_Int_t * vFlops ); extern int Saig_ManVerifyCex( Aig_Man_t * pAig, Abc_Cex_t * p ); extern Abc_Cex_t * Saig_ManExtendCex( Aig_Man_t * pAig, Abc_Cex_t * p ); diff --git a/src/aig/saig/saigDup.c b/src/aig/saig/saigDup.c index b16e3c3b..17dfcc40 100644 --- a/src/aig/saig/saigDup.c +++ b/src/aig/saig/saigDup.c @@ -88,7 +88,7 @@ Aig_Man_t * Saig_ManDupOrpos( Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ) +Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs, int fAddOuts ) { Aig_Man_t * pAigNew; Aig_Obj_t * pObj, * pObj2, * pMiter; @@ -120,9 +120,11 @@ Aig_Man_t * Saig_ManCreateEquivMiter( Aig_Man_t * pAig, Vec_Int_t * vPairs ) Aig_ObjCreateCo( pAigNew, pMiter ); } // transfer to register outputs + if ( fAddOuts ) Saig_ManForEachLi( pAig, pObj, i ) Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) ); Aig_ManCleanup( pAigNew ); + if ( fAddOuts ) Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) ); return pAigNew; } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 4d0ddfea..016c0a59 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -20581,7 +20581,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Ssw_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplkofdseqvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplkodsefqvwh" ) ) != EOF ) { switch ( c ) { @@ -20713,9 +20713,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fOutputCorr ^= 1; break; - case 'f': - pPars->fSemiFormal ^= 1; - break; +// case 'f': +// pPars->fSemiFormal ^= 1; +// break; case 'd': pPars->fDynamic ^= 1; break; @@ -20725,6 +20725,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'e': pPars->fEquivDump ^= 1; break; + case 'f': + pPars->fEquivDump2 ^= 1; + break; case 'q': pPars->fStopWhenGone ^= 1; break; @@ -20787,6 +20790,11 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) else Abc_Print( 0, "Performing constraint-based scorr without constraints.\n" ); } + if ( pPars->fEquivDump && pPars->fEquivDump2 ) + { + Abc_Print( 0, "Command line switches \'-e\' and \'-f\' cannot be used at the same time.\n" ); + return 0; + } // get the new network pNtkRes = Abc_NtkDarSeqSweep2( pNtk, pPars ); @@ -20800,7 +20808,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: scorr [-PQFCLSIVMN ] [-cmplkodseqvwh]\n" ); + Abc_Print( -2, "usage: scorr [-PQFCLSIVMN ] [-cmplkodsefqvwh]\n" ); Abc_Print( -2, "\t performs sequential sweep using K-step induction\n" ); Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize ); Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize ); @@ -20823,6 +20831,7 @@ usage: Abc_Print( -2, "\t-d : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" ); Abc_Print( -2, "\t-s : toggle local simulation in the cone of influence [default = %s]\n", pPars->fLocalSim? "yes": "no" ); Abc_Print( -2, "\t-e : toggle dumping disproved internal equivalences [default = %s]\n", pPars->fEquivDump? "yes": "no" ); + Abc_Print( -2, "\t-f : toggle dumping proved internal equivalences [default = %s]\n", pPars->fEquivDump2? "yes": "no" ); Abc_Print( -2, "\t-q : toggle quitting when PO is not a constant candidate [default = %s]\n", pPars->fStopWhenGone? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printout of flop equivalences [default = %s]\n", pPars->fFlopVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" ); diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h index cd65fc67..9bd83964 100644 --- a/src/proof/ssw/ssw.h +++ b/src/proof/ssw/ssw.h @@ -70,6 +70,7 @@ struct Ssw_Pars_t_ int fVerbose; // verbose stats int fFlopVerbose; // verbose printout of redundant flops int fEquivDump; // enables dumping equivalences + int fEquivDump2; // enables dumping equivalences int fStopWhenGone; // stop when PO output is not a candidate constant // optimized latch correspondence int fLatchCorrOpt; // perform register correspondence (optimized) diff --git a/src/proof/ssw/sswCore.c b/src/proof/ssw/sswCore.c index 5ef6e71e..58c01b21 100644 --- a/src/proof/ssw/sswCore.c +++ b/src/proof/ssw/sswCore.c @@ -66,6 +66,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p ) p->fLocalSim = 0; // local simulation p->fVerbose = 0; // verbose stats p->fEquivDump = 0; // enables dumping equivalences + p->fEquivDump2 = 0; // enables dumping equivalences // latch correspondence p->fLatchCorrOpt = 0; // performs optimized register correspondence diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c index 77cb24de..2687e9c1 100644 --- a/src/proof/ssw/sswSweep.c +++ b/src/proof/ssw/sswSweep.c @@ -220,9 +220,14 @@ p->timeMarkCones += Abc_Clock() - clk; { pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase ); Ssw_ObjSetFrame( p, pObj, f, pObjFraig2 ); + if ( p->pPars->fEquivDump2 && vPairs ) + { + Vec_IntPush( vPairs, pObjRepr->Id ); + Vec_IntPush( vPairs, pObj->Id ); + } return 0; } - if ( vPairs ) + if ( p->pPars->fEquivDump && vPairs ) { Vec_IntPush( vPairs, pObjRepr->Id ); Vec_IntPush( vPairs, pObj->Id ); @@ -334,7 +339,7 @@ p->timeBmc += Abc_Clock() - clk; SeeAlso [] ***********************************************************************/ -void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num ) +void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num, int fAddOuts ) { FILE * pFile; char pBuffer[16]; @@ -347,7 +352,7 @@ void Ssw_ManDumpEquivMiter( Aig_Man_t * p, Vec_Int_t * vPairs, int Num ) return; } fclose( pFile ); - pNew = Saig_ManCreateEquivMiter( p, vPairs ); + pNew = Saig_ManCreateEquivMiter( p, vPairs, fAddOuts ); Ioa_WriteAiger( pNew, pBuffer, 0, 0 ); Aig_ManStop( pNew ); Abc_Print( 1, "AIG with %4d disproved equivs is dumped into file \"%s\".\n", Vec_IntSize(vPairs)/2, pBuffer ); @@ -372,7 +377,7 @@ int Ssw_ManSweep( Ssw_Man_t * p ) Aig_Obj_t * pObj, * pObj2, * pObjNew; int nConstrPairs, i, f; abctime clk; - Vec_Int_t * vDisproved; + Vec_Int_t * vObjPairs; // perform speculative reduction clk = Abc_Clock(); @@ -407,18 +412,18 @@ p->timeReduce += Abc_Clock() - clk; Ssw_ClassesClearRefined( p->ppClasses ); if ( p->pPars->fVerbose ) pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pAig) ); - vDisproved = p->pPars->fEquivDump? Vec_IntAlloc(1000) : NULL; + vObjPairs = (p->pPars->fEquivDump || p->pPars->fEquivDump2)? Vec_IntAlloc(1000) : NULL; Aig_ManForEachObj( p->pAig, pObj, i ) { if ( p->pPars->fVerbose ) Bar_ProgressUpdate( pProgress, i, NULL ); if ( Saig_ObjIsLo(p->pAig, pObj) ) - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vObjPairs ); else if ( Aig_ObjIsNode(pObj) ) { pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) ); Ssw_ObjSetFrame( p, pObj, f, pObjNew ); - p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vDisproved ); + p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 0, vObjPairs ); } } if ( p->pPars->fVerbose ) @@ -427,8 +432,10 @@ p->timeReduce += Abc_Clock() - clk; // cleanup // Ssw_ClassesCheck( p->ppClasses ); if ( p->pPars->fEquivDump ) - Ssw_ManDumpEquivMiter( p->pAig, vDisproved, Counter++ ); - Vec_IntFreeP( &vDisproved ); + Ssw_ManDumpEquivMiter( p->pAig, vObjPairs, Counter++, 1 ); + if ( p->pPars->fEquivDump2 && !p->fRefined ) + Ssw_ManDumpEquivMiter( p->pAig, vObjPairs, 0, 0 ); + Vec_IntFreeP( &vObjPairs ); return p->fRefined; } -- cgit v1.2.3