diff options
-rw-r--r-- | src/base/abci/abc.c | 132 | ||||
-rw-r--r-- | src/misc/util/utilCex.c | 2 |
2 files changed, 122 insertions, 12 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 425b64f5..6778e6ee 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -354,6 +354,7 @@ static int Abc_CommandAbc9Sat ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Fraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Srm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Reduce ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9EquivMark ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Cec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Force ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Embed ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -396,6 +397,42 @@ extern int Abc_CommandAbcLivenessToSafetyWithLTL( Abc_Frame_t * pAbc, int argc, SeeAlso [] ***********************************************************************/ +Abc_Cex_t * Abc_FrameReadCex( Abc_Frame_t * pAbc ) +{ + Abc_Cex_t * pCex; + pCex = pAbc->pCex; + pAbc->pCex = NULL; + return pCex; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_FrameSetCex( Abc_Frame_t * pAbc, Abc_Cex_t * pCex ) +{ + ABC_FREE( pAbc->pCex ); + pAbc->pCex = pCex; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Abc_FrameReplaceCex( Abc_Frame_t * pAbc, Abc_Cex_t ** ppCex ) { ABC_FREE( pAbc->pCex ); @@ -752,6 +789,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&fraig", Abc_CommandAbc9Fraig, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&srm", Abc_CommandAbc9Srm, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&reduce", Abc_CommandAbc9Reduce, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&equiv_mark", Abc_CommandAbc9EquivMark, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&cec", Abc_CommandAbc9Cec, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&force", Abc_CommandAbc9Force, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&embed", Abc_CommandAbc9Embed, 0 ); @@ -25936,14 +25974,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) { - char * pFileName = "gsrm.aig"; - char * pFileName2 = "gsyn.aig"; + char pFileName[10], pFileName2[10]; Gia_Man_t * pTemp, * pAux; int c, fVerbose = 0; + int fSpeculate = 1; int fSynthesis = 0; int fDualOut = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "dsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "dsrvh" ) ) != EOF ) { switch ( c ) { @@ -25951,6 +25989,9 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) fDualOut ^= 1; break; case 's': + fSpeculate ^= 1; + break; + case 'r': fSynthesis ^= 1; break; case 'v': @@ -25967,12 +26008,16 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Srm(): There is no AIG.\n" ); return 1; } - pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fVerbose ); + sprintf( pFileName, "gsrm%s.aig", fSpeculate? "" : "s" ); + sprintf( pFileName2, "gsyn%s.aig", fSpeculate? "" : "s" ); + pTemp = Gia_ManSpecReduce( pAbc->pGia, fDualOut, fSynthesis, fSpeculate, fVerbose ); if ( pTemp ) { - pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); - Gia_ManStop( pAux ); - + if ( fSpeculate ) + { + pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 ); + Gia_ManStop( pAux ); + } Gia_WriteAiger( pTemp, pFileName, 0, 0 ); Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", pFileName ); Gia_ManPrintStatsShort( pTemp ); @@ -25995,10 +26040,11 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &srm [-dsvh]\n" ); + Abc_Print( -2, "usage: &srm [-dsrvh]\n" ); Abc_Print( -2, "\t writes speculatively reduced model into file \"%s\"\n", pFileName ); Abc_Print( -2, "\t-d : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" ); - Abc_Print( -2, "\t-s : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle using speculation at the internal nodes [default = %s]\n", fSpeculate? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -26046,13 +26092,15 @@ int Abc_CommandAbc9Reduce( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Reduce(): There is no AIG.\n" ); return 1; } - pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, fVerbose ); - if ( pTemp != NULL ) + if ( fUseAll ) { + pTemp = Gia_ManEquivReduce( pAbc->pGia, fUseAll, fDualOut, fVerbose ); pTemp = Gia_ManSeqStructSweep( pTemp2 = pTemp, 1, 1, 0 ); Gia_ManStop( pTemp2 ); - Abc_CommandUpdate9( pAbc, pTemp ); } + else + pTemp = Gia_ManEquivReduceAndRemap( pAbc->pGia, 1, fDualOut ); + Abc_CommandUpdate9( pAbc, pTemp ); return 0; usage: @@ -26076,6 +26124,66 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandAbc9EquivMark( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_ManEquivMark( Gia_Man_t * p, char * pFileName, int fVerbose ); + char * pFileName; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Reduce(): There is no AIG.\n" ); + return 1; + } + if ( argc != globalUtilOptind + 1 ) + goto usage; + // get the input file name + pFileName = argv[globalUtilOptind]; + // mark equivalences + Gia_ManEquivMark( pAbc->pGia, pFileName, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &equiv_mark [-vh] <miter.aig>\n" ); + Abc_Print( -2, "\t marks equivalences using an external miter\n" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t<miter.aig> : file with the external miter to read\n"); + Abc_Print( -2, "\t \n" ); + Abc_Print( -2, "\t The external miter should be generated by &srm -m\n" ); + Abc_Print( -2, "\t and (partially) solved by any verification engine(s).\n" ); + Abc_Print( -2, "\t The external miter should have as many POs as\n" ); + Abc_Print( -2, "\t the number of POs in the current AIG plus\n" ); + Abc_Print( -2, "\t the number of equivalences in the current AIG.\n" ); + Abc_Print( -2, "\t If some POs are proved, the corresponding equivs\n" ); + Abc_Print( -2, "\t are marked as proved, to be reduced by &reduce.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) { Cec_ParCec_t ParsCec, * pPars = &ParsCec; diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c index 068e1768..a4cf5e33 100644 --- a/src/misc/util/utilCex.c +++ b/src/misc/util/utilCex.c @@ -139,6 +139,8 @@ Abc_Cex_t * Abc_CexDup( Abc_Cex_t * p, int nRegsNew ) { Abc_Cex_t * pCex; int i; + if ( nRegsNew == -1 ) + nRegsNew = p->nRegs; pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 ); pCex->iPo = p->iPo; pCex->iFrame = p->iFrame; |