summaryrefslogtreecommitdiffstats
path: root/src/base
diff options
context:
space:
mode:
Diffstat (limited to 'src/base')
-rw-r--r--src/base/abc/abc.h1
-rw-r--r--src/base/abc/abcNtk.c3
-rw-r--r--src/base/abci/abc.c290
-rw-r--r--src/base/abci/abcDar.c84
-rw-r--r--src/base/io/io.c45
5 files changed, 331 insertions, 92 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index f7739b91..11161698 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -197,6 +197,7 @@ struct Abc_Ntk_t_
Vec_Int_t * vLevelsR; // level in the reverse topological order (for AIGs)
Vec_Ptr_t * vSupps; // CO support information
int * pModel; // counter-example (for miters)
+ void * pSeqModel; // counter-example (for sequential miters)
Abc_Ntk_t * pExdc; // the EXDC network (if given)
void * pData; // misc
Abc_Ntk_t * pCopy;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index adaaf7be..d78a3a6a 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -979,7 +979,8 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
Vec_PtrFree( pNtk->vObjs );
Vec_PtrFree( pNtk->vBoxes );
if ( pNtk->vLevelsR ) Vec_IntFree( pNtk->vLevelsR );
- if ( pNtk->pModel ) free( pNtk->pModel );
+ FREE( pNtk->pModel );
+ FREE( pNtk->pSeqModel );
TotalMemory = 0;
TotalMemory += pNtk->pMmObj? Extra_MmFixedReadMemUsage(pNtk->pMmObj) : 0;
TotalMemory += pNtk->pMmStep? Extra_MmStepReadMemUsage(pNtk->pMmStep) : 0;
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7d9b8be2..3f9ffb40 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -123,11 +123,9 @@ static int Abc_CommandISat ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandIFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCSweep ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandIProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandHaig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMini ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandBmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandQbf ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -173,6 +171,7 @@ static int Abc_CommandLcorr ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSim ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -181,7 +180,9 @@ static int Abc_CommandDSec ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDSat ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv );
+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_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -294,10 +295,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "New AIG", "ifraig", Abc_CommandIFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "dfraig", Abc_CommandDFraig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "csweep", Abc_CommandCSweep, 1 );
- Cmd_CommandAdd( pAbc, "New AIG", "iprove", Abc_CommandIProve, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "haig", Abc_CommandHaig, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "mini", Abc_CommandMini, 1 );
- Cmd_CommandAdd( pAbc, "New AIG", "_bmc", Abc_CommandBmc, 0 );
Cmd_CommandAdd( pAbc, "New AIG", "qbf", Abc_CommandQbf, 0 );
Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 );
@@ -341,6 +340,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Sequential", "scleanup", Abc_CommandSeqCleanup, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "cycle", Abc_CommandCycle, 1 );
Cmd_CommandAdd( pAbc, "Sequential", "xsim", Abc_CommandXsim, 0 );
+ Cmd_CommandAdd( pAbc, "Sequential", "sim", Abc_CommandSim, 0 );
Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dcec", Abc_CommandDCec, 0 );
@@ -350,7 +350,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "dsat", Abc_CommandDSat, 0 );
Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 );
+ 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", "trace_start", Abc_CommandTraceStart, 0 );
// Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 );
@@ -6337,8 +6339,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// pNtkRes = Abc_NtkDar( pNtk );
// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 );
- pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
-// pNtkRes = NULL;
+// pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose );
+ pNtkRes = NULL;
if ( pNtkRes == NULL )
{
fprintf( pErr, "Command has failed.\n" );
@@ -8100,89 +8102,6 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
- FILE * pOut, * pErr;
- Abc_Ntk_t * pNtk;
- int c;
- int nFrames;
- int fInit;
- int fVerbose;
-
- extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose );
-
- pNtk = Abc_FrameReadNtk(pAbc);
- pOut = Abc_FrameReadOut(pAbc);
- pErr = Abc_FrameReadErr(pAbc);
-
- // set defaults
- nFrames = 5;
- fInit = 0;
- fVerbose = 1;
- Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Kivh" ) ) != EOF )
- {
- switch ( c )
- {
- case 'K':
- if ( globalUtilOptind >= argc )
- {
- fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" );
- goto usage;
- }
- nFrames = atoi(argv[globalUtilOptind]);
- globalUtilOptind++;
- if ( nFrames < 0 )
- goto usage;
- break;
- case 'i':
- fInit ^= 1;
- 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_NtkIsStrash(pNtk) )
- Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
- else
- {
- pNtk = Abc_NtkStrash( pNtk, 0, 1, 0 );
- Abc_NtkBmc( pNtk, nFrames, fInit, fVerbose );
- Abc_NtkDelete( pNtk );
- }
- return 0;
-
-usage:
- fprintf( pErr, "usage: _bmc [-K num] [-ivh]\n" );
- fprintf( pErr, "\t perform bounded model checking\n" );
- fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames );
- fprintf( pErr, "\t-i : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" );
- fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
- fprintf( pErr, "\t-h : print the command usage\n");
- return 1;
-}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
int Abc_CommandQbf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr;
@@ -11659,6 +11578,103 @@ usage:
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nFrames;
+ int nWords;
+ int fVerbose;
+ extern int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 32;
+ nWords = 8;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FWvh" ) ) != 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 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nWords = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nWords < 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_NtkIsStrash(pNtk) )
+ {
+ fprintf( pErr, "Only works for strashed networks.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkLatchNum(pNtk) )
+ {
+ fprintf( pErr, "Only works for sequential networks.\n" );
+ return 1;
+ }
+
+ FREE( pNtk->pSeqModel );
+ Abc_NtkDarSeqSim( pNtk, nFrames, nWords, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: sim [-F num] [-W num] [-vh]\n" );
+ fprintf( pErr, "\t performs random simulation of the sequentail miter\n" );
+ fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
+ 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*************************************************************
@@ -12787,6 +12803,102 @@ usage:
fprintf( pErr, "\t-h : print the command usage\n");
return 1;
}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int nFrames;
+ int nBTLimit;
+ int fRewrite;
+ int fVerbose;
+
+// extern void Abc_NtkBmc( Abc_Ntk_t * pNtk, int nFrames, int fInit, int fVerbose );
+ extern int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ nFrames = 5;
+ nBTLimit = 1000000;
+ fRewrite = 0;
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "FCrvh" ) ) != 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 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'r':
+ fRewrite ^= 1;
+ 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_NtkIsStrash(pNtk) )
+ {
+ fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
+ return 0;
+ }
+ Abc_NtkDarBmc( pNtk, nFrames, nBTLimit, fRewrite, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: bmc [-F num] [-C num] [-rvh]\n" );
+ fprintf( pErr, "\t perform bounded model checking\n" );
+ fprintf( pErr, "\t-F num : number of time frames [default = %d]\n", nFrames );
+ fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", nBTLimit );
+ fprintf( pErr, "\t-r : toggle initialization of the first frame [default = %s]\n", fRewrite? "yes": "no" );
+ fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
/**Function*************************************************************
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index abf79a82..ab8614fb 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1070,6 +1070,44 @@ Abc_Ntk_t * Abc_NtkDarLcorr( Abc_Ntk_t * pNtk, int nFramesP, int nConfMax, int f
SeeAlso []
***********************************************************************/
+int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nBTLimit, int fRewrite, int fVerbose )
+{
+ Aig_Man_t * pMan;
+ int clk = clock();
+ // derive the AIG manager
+ pMan = Abc_NtkToDar( pNtk, 1 );
+ if ( pMan == NULL )
+ {
+ printf( "Converting miter into AIG has failed.\n" );
+ return -1;
+ }
+ assert( pMan->nRegs > 0 );
+ // perform verification
+ Fra_BmcPerformSimple( pMan, nFrames, nBTLimit, fRewrite, fVerbose );
+ pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+ if ( pNtk->pSeqModel )
+ {
+ Fra_Cex_t * pCex = pNtk->pSeqModel;
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace). ", pCex->iPo, pCex->iFrame );
+ }
+ else
+ printf( "No output was asserted after BMC with %d frames. ", nFrames );
+PRT( "Time", clock() - clk );
+ Aig_ManStop( pMan );
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Gives the current ABC network to AIG manager for processing.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose )
{
Aig_Man_t * pMan;
@@ -1084,6 +1122,12 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fVerbo
assert( pMan->nRegs > 0 );
// perform verification
RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fVerbose, fVeryVerbose );
+ pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
+ if ( pNtk->pSeqModel )
+ {
+ Fra_Cex_t * pCex = pNtk->pSeqModel;
+ printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump the trace).\n", pCex->iPo, pCex->iFrame );
+ }
Aig_ManStop( pMan );
return RetValue;
}
@@ -1238,6 +1282,46 @@ Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose )
return pNtkAig;
}
+/**Function*************************************************************
+
+ Synopsis [Performs random simulation.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int fVerbose )
+{
+ Aig_Man_t * pMan;
+ Fra_Sml_t * pSml;
+ Fra_Cex_t * pCex;
+ int RetValue, clk = clock();
+ pMan = Abc_NtkToDar( pNtk, 1 );
+ pSml = Fra_SmlSimulateSeq( pMan, 0, nFrames, nWords );
+ if ( pSml->fNonConstOut )
+ {
+ pCex = Fra_SmlGetCounterExample( pSml );
+ if ( pCex )
+ printf( "Simulation of %d frames with %d words asserted output %d in frame %d. ",
+ nFrames, nWords, pCex->iPo, pCex->iFrame );
+ pNtk->pSeqModel = pCex;
+ RetValue = 1;
+ }
+ else
+ {
+ RetValue = 0;
+ printf( "Simulation of %d frames with %d words did not assert the outputs. ",
+ nFrames, nWords );
+ }
+ PRT( "Time", clock() - clk );
+ Fra_SmlStop( pSml );
+ Aig_ManStop( pMan );
+ return RetValue;
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 7a5e4a5d..941ef7a7 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -1569,6 +1569,8 @@ usage:
return 1;
}
+#include "fra.h"
+
/**Function*************************************************************
Synopsis []
@@ -1617,13 +1619,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
// get the input file name
pFileName = argv[globalUtilOptind];
- if ( pNtk->pModel == NULL )
+ if ( pNtk->pModel == NULL && pNtk->pSeqModel == NULL )
{
fprintf( pAbc->Out, "Counter-example is not available.\n" );
return 0;
}
// write the counter-example into the file
+ if ( pNtk->pModel )
{
Abc_Obj_t * pObj;
FILE * pFile = fopen( pFileName, "w" );
@@ -1646,12 +1649,50 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
fprintf( pFile, "\n" );
fclose( pFile );
}
+ else
+ {
+ Fra_Cex_t * pCex = pNtk->pSeqModel;
+ Abc_Obj_t * pObj;
+ FILE * pFile;
+ int i, f;
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ if ( !Abc_LatchIsInit0(pObj) )
+ {
+ fprintf( stdout, "IoCommandWriteCounter(): The init-state should be all-0 for counter-example to work.\n" );
+ fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
+ return 1;
+ }
+
+ pFile = fopen( pFileName, "w" );
+ if ( pFile == NULL )
+ {
+ fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
+ return 1;
+ }
+ if ( fNames )
+ {
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ fprintf( pFile, "%s@0=%c ", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+ for ( f = 0; f <= pCex->iFrame; f++ )
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+ }
+ else
+ {
+ Abc_NtkForEachLatch( pNtk, pObj, i )
+ fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
+ for ( i = pCex->nRegs; i < pCex->nBits; i++ )
+ fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) );
+ }
+ fprintf( pFile, "\n" );
+ fclose( pFile );
+ }
return 0;
usage:
fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
- fprintf( pAbc->Err, "\t writes the counter-example derived by \"prove\" or \"sat\"\n" );
+ fprintf( pAbc->Err, "\t saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
fprintf( pAbc->Err, "\t the file contains values for each PI in the natural order\n" );
fprintf( pAbc->Err, "\t-n : write input names into the file [default = %s]\n", fNames? "yes": "no" );
fprintf( pAbc->Err, "\t-h : print the help massage\n" );
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-05 06:02:32 +0000