From 126637ddd3c237d9c83f3a7f2b1f3f2722337411 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 16 Dec 2007 08:01:00 -0800 Subject: Version abc71216 --- src/base/abci/abc.c | 244 +++++++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 234 insertions(+), 10 deletions(-) (limited to 'src/base/abci/abc.c') diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 3b238779..98dcde81 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -184,6 +184,8 @@ static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandIndcut ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandEnlarge ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -355,6 +357,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "iprove", Abc_CommandIProve, 1 ); Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); Cmd_CommandAdd( pAbc, "Verification", "bmc", Abc_CommandBmc, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "indcut", Abc_CommandIndcut, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "enlarge", Abc_CommandEnlarge, 1 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); @@ -6210,12 +6214,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk ); - extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nStepsMax, int fBmc, int fVerbose, int fVeryVerbose ); + extern void Abc_NtkDarTestBlif( char * pFileName ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); +// printf( "This command is temporarily disabled.\n" ); +// return 0; + // set defaults fVeryVerbose = 0; fVerbose = 1; @@ -6351,13 +6358,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } */ - +/* if ( !Abc_NtkIsStrash(pNtk) ) { fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); return 0; } - +*/ /* if ( Abc_NtkIsStrash(pNtk) ) { @@ -6378,7 +6385,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); */ // Abc_NtkDarHaigRecord( pNtk ); - Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose ); +// Abc_NtkDarClau( pNtk, nFrames, nLevels, fBmc, fVerbose, fVeryVerbose ); + + if ( globalUtilOptind != 1 ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + Abc_NtkDarTestBlif( argv[globalUtilOptind] ); return 0; usage: fprintf( pErr, "usage: test [-vwh]\n" ); @@ -11302,7 +11316,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Abc_NtkIsComb(pNtk) ) { fprintf( pErr, "The network is combinational (run \"fraig\" or \"fraig_sweep\").\n" ); - return 1; + return 0; } if ( !Abc_NtkIsStrash(pNtk) ) @@ -11523,7 +11537,6 @@ usage: fprintf( pErr, "\t - removes nodes/latches that do not feed into POs\n" ); fprintf( pErr, "\t - removes stuck-at and identical latches (latch sweep)\n" ); // fprintf( pErr, "\t - replaces autonomous logic by free PI variables\n" ); - fprintf( pErr, "\t (the latter may change sequential behaviour)\n" ); fprintf( pErr, "\t-l : toggle sweeping latches [default = %s]\n", fLatchSweep? "yes": "no" ); // fprintf( pErr, "\t-a : toggle removing autonomous logic [default = %s]\n", fAutoSweep? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); @@ -12390,11 +12403,11 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF ) { switch ( c ) { - case 'K': + case 'F': if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); @@ -12435,9 +12448,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" ); + fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); - fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames ); + fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); @@ -13031,6 +13044,217 @@ usage: fprintf( pErr, "\t-h : print the command usage\n"); return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandIndcut( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int nFrames; + int nPref; + int nClauses; + int fBmc; + int fRegs; + int fVerbose; + int fVeryVerbose; + int c; + extern int Abc_NtkDarClau( Abc_Ntk_t * pNtk, int nFrames, int nPref, int nClauses, int fBmc, int fRegs, int fVerbose, int fVeryVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 1; + nPref = 0; + nClauses = 5000; + fBmc = 1; + fRegs = 1; + fVerbose = 0; + fVeryVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FPCbrvwh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nPref = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPref < 0 ) + goto usage; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nClauses = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nClauses < 0 ) + goto usage; + break; + case 'b': + fBmc ^= 1; + break; + case 'r': + fRegs ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'w': + fVeryVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "Only works for sequential networks.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + Abc_NtkDarClau( pNtk, nFrames, nPref, nClauses, fBmc, fRegs, fVerbose, fVeryVerbose ); + return 0; +usage: + fprintf( pErr, "usage: indcut [-F num] [-P num] [-C num] [-bvh]\n" ); + fprintf( pErr, "\t K-step induction strengthened with cut properties\n" ); + fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFrames ); + fprintf( pErr, "\t-P num : number of time frames in the prefix (0=no prefix) [default = %d]\n", nPref ); + fprintf( pErr, "\t-C num : the max number of clauses to use for strengthening [default = %d]\n", nClauses ); + fprintf( pErr, "\t-b : toggle enabling BMC check [default = %s]\n", fBmc? "yes": "no" ); + fprintf( pErr, "\t-r : toggle enabling register clauses [default = %s]\n", fRegs? "yes": "no" ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); +// fprintf( pErr, "\t-w : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandEnlarge( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int nFrames; + int fVerbose; + int c; + extern Abc_Ntk_t * Abc_NtkDarEnlarge( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 5; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( Abc_NtkIsComb(pNtk) ) + { + fprintf( pErr, "Only works for sequential networks.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( stdout, "Currently only works for structurally hashed circuits.\n" ); + return 0; + } + + // modify the current network + pNtkRes = Abc_NtkDarEnlarge( pNtk, nFrames, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Target enlargement has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; +usage: + fprintf( pErr, "usage: enlarge [-F num] [-vh]\n" ); + fprintf( pErr, "\t performs structural K-step target enlargement\n" ); + fprintf( pErr, "\t-F num : the number of timeframes for enlargement [default = %d]\n", nFrames ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} /**Function************************************************************* -- cgit v1.2.3