diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-24 20:44:25 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-01-24 20:44:25 -0800 |
commit | 849f18076411a54c21e593e3bd9e72bf6d56883e (patch) | |
tree | 63d8af87e0660715774c7136ce18d3f274e1de44 /src/base/wlc/wlcCom.c | |
parent | 876eb5a52e67911ccc19d5f732aa9e1c9279fd26 (diff) | |
download | abc-849f18076411a54c21e593e3bd9e72bf6d56883e.tar.gz abc-849f18076411a54c21e593e3bd9e72bf6d56883e.tar.bz2 abc-849f18076411a54c21e593e3bd9e72bf6d56883e.zip |
Adding features for invariant minimization.
Diffstat (limited to 'src/base/wlc/wlcCom.c')
-rw-r--r-- | src/base/wlc/wlcCom.c | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 93614938..85b3b35d 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -646,8 +646,8 @@ usage: ******************************************************************************/ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Vec_Int_t * Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ); - int c, fVerbose = 0; + extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv ); + int c, nFailed, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { @@ -677,7 +677,11 @@ int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); return 0; } - Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) ); + nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc) ); + if ( nFailed ) + printf( "Invariant verification failed for %d clauses (out of %d).\n", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); + else + printf( "Invariant verification passes.\n" ); return 0; usage: Abc_Print( -2, "usage: inv_check [-vh]\n" ); @@ -808,13 +812,17 @@ usage: int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv ); + extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv ); Vec_Int_t * vInv, * vInv2; - int c, fVerbose = 0; + int c, fLits = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "lvh" ) ) != EOF ) { switch ( c ) { + case 'l': + fLits ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -840,14 +848,18 @@ int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); return 0; } - vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv ); + if ( fLits ) + vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv ); + else + vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv ); if ( vInv2 ) Abc_FrameSetInv( vInv2 ); return 0; usage: - Abc_Print( -2, "usage: inv_min [-vh]\n" ); - Abc_Print( -2, "\t minimizes the number of clauses in the current invariant\n" ); + Abc_Print( -2, "usage: inv_min [-lvh]\n" ); + Abc_Print( -2, "\t performs minimization of the current invariant\n" ); Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" ); + Abc_Print( -2, "\t-l : toggle minimizing literals rather than clauses [default = %s]\n", fLits? "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; |