diff options
Diffstat (limited to 'src/base/wlc/wlcCom.c')
| -rw-r--r-- | src/base/wlc/wlcCom.c | 949 |
1 files changed, 865 insertions, 84 deletions
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index f3eb6dd7..df736e70 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -28,22 +28,31 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandPsInv ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandGetInv ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static int Abc_CommandInvPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandInvMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; } static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); } static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; } static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; } -static inline Vec_Int_t * Wlc_AbcGetCnf( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcCnf; } -static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcStr; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -62,14 +71,25 @@ static inline Vec_Str_t * Wlc_AbcGetStr( Abc_Frame_t * pAbc ) ******************************************************************************/ void Wlc_Init( Abc_Frame_t * pAbc ) { - Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%psinv", Abc_CommandPsInv, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%getinv", Abc_CommandGetInv, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%show", Abc_CommandShow, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); + + Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_get", Abc_CommandInvGet, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_put", Abc_CommandInvPut, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "inv_min", Abc_CommandInvMin, 0 ); } /**Function******************************************************************** @@ -275,15 +295,20 @@ usage: int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int fShowCones = 0; int fShowMulti = 0; int fShowAdder = 0; int fDistrib = 0; + int fTwoSides = 0; int c, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "madvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "cmadtvh" ) ) != EOF ) { switch ( c ) { + case 'c': + fShowCones ^= 1; + break; case 'm': fShowMulti ^= 1; break; @@ -293,6 +318,9 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDistrib ^= 1; break; + case 't': + fTwoSides ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -307,18 +335,110 @@ int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( 1, "Abc_CommandPs(): There is no current design.\n" ); return 0; } - Wlc_NtkPrintStats( pNtk, fDistrib, fVerbose ); + Wlc_NtkPrintStats( pNtk, fDistrib, fTwoSides, fVerbose ); + if ( fShowCones ) + Wlc_NtkProfileCones( pNtk ); if ( fShowMulti ) Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_MULTI ); if ( fShowAdder ) Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD ); return 0; usage: - Abc_Print( -2, "usage: %%ps [-madvh]\n" ); + Abc_Print( -2, "usage: %%ps [-cmadtvh]\n" ); Abc_Print( -2, "\t prints statistics\n" ); - Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" ); - Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" ); - Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle printing cones [default = %s]\n", fShowCones? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" ); + Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" ); + Abc_Print( -2, "\t-t : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides? "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; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, iOutput = -1, Range = 1, fAllPis = 0, fSeq = 0, fVerbose = 0; + char * pName; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ORisvh" ) ) != EOF ) + { + switch ( c ) + { + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + iOutput = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( iOutput < 0 ) + goto usage; + break; + case 'R': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" ); + goto usage; + } + Range = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( Range < 0 ) + goto usage; + break; + case 'i': + fAllPis ^= 1; + break; + case 's': + fSeq ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + if ( iOutput < 0 || iOutput >= Wlc_NtkCoNum(pNtk) ) + { + Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkCoNum(pNtk) ); + return 0; + } + printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" ); + pName = Wlc_NtkNewName( pNtk, iOutput, fSeq ); + Wlc_NtkMarkCone( pNtk, iOutput, Range, fSeq, fAllPis ); + pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq ); + ABC_FREE( pNtk->pName ); + pNtk->pName = Abc_UtilStrsav( pName ); + Wlc_AbcUpdateNtk( pAbc, pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%cone [-OR num] [-isvh]\n" ); + Abc_Print( -2, "\t extracts logic cone of one or more word-level outputs\n" ); + Abc_Print( -2, "\t-O num : zero-based index of the first word-level output to extract [default = %d]\n", iOutput ); + Abc_Print( -2, "\t-R num : total number of word-level outputs to extract [default = %d]\n", Range ); + Abc_Print( -2, "\t-i : toggle using support composed of all primary inputs [default = %s]\n", fAllPis? "yes": "no" ); + Abc_Print( -2, "\t-s : toggle performing extracting sequential cones [default = %s]\n", fSeq? "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; @@ -335,6 +455,357 @@ usage: SeeAlso [] ******************************************************************************/ +int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIcpxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'c': + pPars->fCheckClauses ^= 1; + break; + case 'p': + pPars->fPushClauses ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkPdrAbs( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-cpxvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkAbsCore( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%abs [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandAbs2( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Wlc_Par_t Pars, * pPars = &Pars; + int c; + Wlc_ManSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsAdd < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMul = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMul < 0 ) + goto usage; + break; + case 'X': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsMux = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsMux < 0 ) + goto usage; + break; + case 'F': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBitsFlop = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBitsFlop < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nIterMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nIterMax < 0 ) + goto usage; + break; + case 'x': + pPars->fXorOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'w': + pPars->fPdrVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" ); + return 0; + } + Wlc_NtkAbsCore2( pNtk, pPars ); + return 0; +usage: + Abc_Print( -2, "usage: %%abs2 [-AMXFI num] [-xvwh]\n" ); + Abc_Print( -2, "\t abstraction for word-level networks\n" ); + Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd ); + Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul ); + Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux ); + Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop ); + Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax ); + Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" ); + Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) { Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); @@ -440,10 +911,200 @@ usage: SeeAlso [] ******************************************************************************/ -int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + 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 ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" ); + return 0; + } + Wlc_WinProfileArith( pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%profile [-vh]\n" ); + Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\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"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + 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 ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" ); + return 0; + } + Wlc_NtkShortNames( pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%short_names [-vh]\n" ); + Abc_Print( -2, "\t derives short names for all objects of the network\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"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold ); + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + int c, fVerbose = 0; + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + Wlc_NtkShow( pNtk, NULL ); + return 0; + +usage: + Abc_Print( -2, "usage: %%show [-h]\n" ); + Abc_Print( -2, " visualizes the network structure using DOT and GSVIEW\n" ); +#ifdef WIN32 + Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" ); + Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" ); +#endif + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p ); + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + 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 ( pNtk == NULL ) + { + Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" ); + return 0; + } + // transform + //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); + //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); + //Wlc_AbcUpdateNtk( pAbc, pNtk ); + //Wlc_GenerateSmtStdout( pAbc ); + //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc ); + pNtk = Wlc_NtkDupSingleNodes( pNtk ); + Wlc_AbcUpdateNtk( pAbc, pNtk ); + return 0; +usage: + Abc_Print( -2, "usage: %%test [-vh]\n" ); + Abc_Print( -2, "\t experiments with word-level networks\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"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv ); extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose ); Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + Vec_Int_t * vCounts; int c, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) @@ -461,24 +1122,66 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( pNtk == NULL ) { - Abc_Print( 1, "Abc_CommandPsInv(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" ); return 0; } - if ( Wlc_AbcGetNtk(pAbc) == NULL ) + if ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandPsInv(): There is no saved invariant.\n" ); + Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" ); return 0; } + vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) ); + Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose ); + Vec_IntFree( vCounts ); + return 0; +usage: + Abc_Print( -2, "usage: inv_ps [-vh]\n" ); + Abc_Print( -2, "\t prints statistics for inductive invariant\n" ); + Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\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"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose ); + 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 ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandPsInv(): Invariant is not available.\n" ); + Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" ); return 0; } - Wlc_NtkPrintInvStats( pNtk, Wlc_AbcGetInv(pAbc), fVerbose ); + Pdr_InvPrint( Wlc_AbcGetInv(pAbc), fVerbose ); return 0; - usage: - Abc_Print( -2, "usage: %%psinv [-vh]\n" ); - Abc_Print( -2, "\t prints statistics for inductive invariant\n" ); +usage: + Abc_Print( -2, "usage: inv_print [-vh]\n" ); + Abc_Print( -2, "\t prints the current inductive invariant\n" ); Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\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"); @@ -496,12 +1199,11 @@ int Abc_CommandPsInv( Abc_Frame_t * pAbc, int argc, char ** argv ) SeeAlso [] ******************************************************************************/ -int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, Vec_Str_t * vSop, int fVerbose ); - Abc_Ntk_t * pMainNtk; - Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - int c, fVerbose = 0; + abctime clk = Abc_Clock(); + extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + int c, nFailed, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { @@ -516,28 +1218,81 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pNtk == NULL ) + if ( pAbc->pGia == NULL ) { - Abc_Print( 1, "Abc_CommandGetInv(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" ); return 0; } - if ( Wlc_AbcGetNtk(pAbc) == NULL ) + if ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandGetInv(): There is no saved invariant.\n" ); + Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" ); return 0; } + if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) ) + { + Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); + return 0; + } + nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose ); + if ( nFailed ) + printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) ); + else + printf( "Invariant verification succeeded. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return 0; +usage: + Abc_Print( -2, "usage: inv_check [-vh]\n" ); + Abc_Print( -2, "\t checks that the invariant is indeed an inductive invariant\n" ); + Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\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"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv ); + Abc_Ntk_t * pMainNtk; + Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + 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 ( Wlc_AbcGetInv(pAbc) == NULL ) { - Abc_Print( 1, "Abc_CommandGetInv(): Invariant is not available.\n" ); + Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" ); return 0; } // derive the network - pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc), Wlc_AbcGetStr(pAbc), fVerbose ); + pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) ); // replace the current network - Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk ); + if ( pMainNtk ) + Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk ); return 0; - usage: - Abc_Print( -2, "usage: %%getinv [-vh]\n" ); +usage: + Abc_Print( -2, "usage: inv_get [-vh]\n" ); Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" ); Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); @@ -556,34 +1311,45 @@ int Abc_CommandGetInv( Abc_Frame_t * pAbc, int argc, char ** argv ) SeeAlso [] ******************************************************************************/ -int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); + extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia ); + Vec_Int_t * vInv = NULL; + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); 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; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; } } if ( pNtk == NULL ) { - Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" ); return 0; } - Wlc_WinProfileArith( pNtk ); + if ( pAbc->pGia == NULL ) + { + Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" ); + return 0; + } + // derive the network + vInv = Wlc_NtkGetPut( pNtk, pAbc->pGia ); + if ( vInv ) + Abc_FrameSetInv( vInv ); return 0; usage: - Abc_Print( -2, "usage: %%profile [-vh]\n" ); - Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" ); + Abc_Print( -2, "usage: inv_put [-vh]\n" ); + Abc_Print( -2, "\t inputs the current network in the main-space as an invariant\n" ); + Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\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"); return 1; @@ -600,42 +1366,57 @@ usage: SeeAlso [] ******************************************************************************/ -int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) +int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p ); - Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); - int c, fVerbose = 0; + extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose ); + Vec_Int_t * vInv, * vInv2; + 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 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; + case 'l': + fLits ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; } } - if ( pNtk == NULL ) + if ( pAbc->pGia == NULL ) { - Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" ); + Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" ); return 0; } - // transform - //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL ); - //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL ); - //Wlc_AbcUpdateNtk( pAbc, pNtk ); - //Wlc_GenerateSmtStdout( pAbc ); - //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc ); - pNtk = Wlc_NtkDupSingleNodes( pNtk ); - Wlc_AbcUpdateNtk( pAbc, pNtk ); + if ( Wlc_AbcGetInv(pAbc) == NULL ) + { + Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" ); + return 0; + } + vInv = Wlc_AbcGetInv(pAbc); + if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) ) + { + Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" ); + return 0; + } + if ( fLits ) + vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv, fVerbose ); + else + vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv, fVerbose ); + if ( vInv2 ) + Abc_FrameSetInv( vInv2 ); return 0; usage: - Abc_Print( -2, "usage: %%test [-vh]\n" ); - Abc_Print( -2, "\t experiments with word-level networks\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; |