Skip to content

A
abc
Unverified Commit f36724e3 by Miodrag Milanović Committed by GitHub
Options

read_cex (#12) 

Added read_cex command
parent b4790a64
Showing with 285 additions and 7 deletions
src/base/io/io.c
...@@ -44,6 +44,7 @@ static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv ); ...@@ -44,6 +44,7 @@ static int IoCommandReadBblif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBlifMv ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadBench ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadCex ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadDsd ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEdif ( Abc_Frame_t * pAbc, int argc, char **argv );
static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandReadEqn ( Abc_Frame_t * pAbc, int argc, char **argv );
...@@ -113,6 +114,7 @@ void Io_Init( Abc_Frame_t * pAbc ) ...@@ -113,6 +114,7 @@ void Io_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif", IoCommandReadBlif, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv", IoCommandReadBlifMv, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_bench", IoCommandReadBench, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_cex", IoCommandReadCex, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_dsd", IoCommandReadDsd, 1 );
Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 ); Cmd_CommandAdd( pAbc, "I/O", "read_formula", IoCommandReadDsd, 1 );
// Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 ); // Cmd_CommandAdd( pAbc, "I/O", "read_edif", IoCommandReadEdif, 1 );
...@@ -679,6 +681,271 @@ usage: ...@@ -679,6 +681,271 @@ usage:
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, int * pnFrames, int * fOldFormat )
{
FILE * pFile;
Abc_Cex_t * pCex;
Vec_Int_t * vNums;
int c, nRegs = -1, nFrames = -1, Status = 0;
pFile = fopen( pFileName, "r" );
if ( pFile == NULL )
{
printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
return -1;
}
vNums = Vec_IntAlloc( 100 );
int usedX = 0;
*fOldFormat = 0;
char Buffer[1000];
int state = 0;
int iPo = 0;
nFrames = -1;
int status = 0;
while ( fgets( Buffer, 1000, pFile ) != NULL )
{
if ( Buffer[0] == '#' )
continue;
Buffer[strlen(Buffer) - 1] = '\0';
if (state==0 && strlen(Buffer)>1) {
// old format detected
*fOldFormat = 1;
state = 2;
iPo = 0;
status = 1;
}
if (state==1 && Buffer[0]!='b' && Buffer[0]!='c') {
// old format detected, first line was actually register
*fOldFormat = 1;
state = 3;
Vec_IntPush( vNums, status );
status = 1;
}
if (Buffer[0] == '.' )
break;
switch(state) {
case 0 :
{
char c = Buffer[0];
if ( c == '0' || c == '1' || c == '2' ) {
status = c - '0' ;
state = 1;
} else if ( c == 'x' ) {
// old format with one x state latch
usedX = 1;
// set to 2 so we can Abc_LatchSetInitNone
// acts like 0 when setting bits
Vec_IntPush( vNums, 2 );
nRegs = Vec_IntSize(vNums);
state = 3;
} else {
printf( "ERROR: Bad aiger status line.\n" );
return -1;
}
}
break;
case 1 :
iPo = atoi(Buffer+1);
state = 2;
break;
case 2 :
for (int i=0; i<strlen(Buffer);i++) {
char c = Buffer[i];
if ( c == '0' || c == '1' )
Vec_IntPush( vNums, c - '0' );
else if ( c == 'x') {
usedX = 1;
// set to 2 so we can Abc_LatchSetInitNone
// acts like 0 when setting bits
Vec_IntPush( vNums, 2 );
}
}
nRegs = Vec_IntSize(vNums);
state = 3;
break;
default:
for (int i=0; i<strlen(Buffer);i++) {
char c = Buffer[i];
if ( c == '0' || c == '1' )
Vec_IntPush( vNums, c - '0' );
else if ( c == 'x') {
usedX = 1;
Vec_IntPush( vNums, 0 );
}
}
nFrames++;
break;
}
}
fclose( pFile );
if (usedX)
printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
int i;
Abc_Obj_t * pObj;
int iFrameCex = nFrames;
int nRegsNtk = 0;
int nPiNtk = 0;
int nPoNtk = 0;
Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
Abc_NtkForEachPi(pNtk, pObj, i ) nPiNtk++;
Abc_NtkForEachPo(pNtk, pObj, i ) nPoNtk++;
if ( nRegs < 0 )
{
printf( "ERROR: Cannot read register number.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( nRegs != nRegsNtk )
{
printf( "ERROR: Register number not coresponding to Ntk.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( Vec_IntSize(vNums)-nRegs == 0 )
{
printf( "ERROR: Cannot read counter example.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
{
printf( "ERROR: Incorrect number of bits.\n" );
Vec_IntFree( vNums );
return -1;
}
int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1);
if ( nPi != nPiNtk )
{
printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" );
Vec_IntFree( vNums );
return -1;
}
if ( iPo >= nPoNtk )
{
printf( "ERROR: PO that failed verification not coresponding to Ntk.\n" );
Vec_IntFree( vNums );
return -1;
}
Abc_NtkForEachLatch( pNtk, pObj, i ) {
if ( Vec_IntEntry(vNums, i) ==0)
Abc_LatchSetInit0(pObj);
else if ( Vec_IntEntry(vNums, i) ==2)
Abc_LatchSetInitNone(pObj);
else
Abc_LatchSetInit1(pObj);
}
pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 );
// the zero-based number of PO, for which verification failed
// fails in Bmc_CexVerify if not less than actual number of PO
pCex->iPo = iPo;
// the zero-based number of the time-frame, for which verificaiton failed
pCex->iFrame = iFrameCex;
assert( Vec_IntSize(vNums) == pCex->nBits );
for ( c = 0; c < pCex->nBits; c++ )
if ( Vec_IntEntry(vNums, c) == 1)
Abc_InfoSetBit( pCex->pData, c );
Vec_IntFree( vNums );
if ( ppCex )
*ppCex = pCex;
else
ABC_FREE( pCex );
if ( pnFrames )
*pnFrames = nFrames;
return Status;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
char * pFileName;
FILE * pFile;
int fCheck;
int c;
int fOldFormat = 0;
fCheck = 1;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF )
{
switch ( c )
{
case 'c':
fCheck ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
// get the input file name
pFileName = argv[globalUtilOptind];
if ( (pFile = fopen( pFileName, "r" )) == NULL )
{
fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
return 1;
}
fclose( pFile );
pNtk = pAbc->pNtkCur;
if ( pNtk == NULL )
{
fprintf( pAbc->Out, "Empty network.\n" );
return 0;
}
Abc_FrameClearVerifStatus( pAbc );
pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pAbc->pCex, &pAbc->nFrames, &fOldFormat );
if ( fCheck ) {
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Bmc_CexCareVerify( pAig, pAbc->pCex, pAbc->pCex, false );
Aig_ManStop( pAig );
} else if (fOldFormat) {
fprintf( pAbc->Err, "Using old aiger format with no checks enabled.\n" );
return -1;
}
return 0;
usage:
fprintf( pAbc->Err, "usage: read_cex [-ch] <file>\n" );
fprintf( pAbc->Err, "\t reads the witness cex\n" );
fprintf( pAbc->Err, "\t-c : toggle check after reading [default = %s]\n", fCheck? "yes":"no" );
fprintf( pAbc->Err, "\t-h : prints the command summary\n" );
fprintf( pAbc->Err, "\tfile : the name of a file to read\n" );
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv ) int IoCommandReadDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
{ {
Abc_Ntk_t * pNtk; Abc_Ntk_t * pNtk;
...@@ -2447,7 +2714,7 @@ extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Ce ...@@ -2447,7 +2714,7 @@ extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Ce
void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo, int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo,
int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose ) int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended )
{ {
Abc_Cex_t * pCare = NULL; Abc_Cex_t * pCare = NULL;
Abc_Obj_t * pObj; Abc_Obj_t * pObj;
...@@ -2558,13 +2825,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, ...@@ -2558,13 +2825,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
} }
else else
{ {
if (fExtended && fAiger && !fNames) {
fprintf( pFile, "1\n");
fprintf( pFile, "b%d\n", pCex->iPo);
}
// output flop values (unaffected by the minimization) // output flop values (unaffected by the minimization)
Abc_NtkForEachLatch( pNtk, pObj, i ) Abc_NtkForEachLatch( pNtk, pObj, i )
if ( fNames ) if ( fNames )
fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) ); fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
else else
fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) ); fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
if ( !fNames ) if ( !fNames && fAiger)
fprintf( pFile, "\n"); fprintf( pFile, "\n");
// output PI values (while skipping the minimized ones) // output PI values (while skipping the minimized ones)
for ( f = 0; f <= pCex->iFrame; f++ ) { for ( f = 0; f <= pCex->iFrame; f++ ) {
...@@ -2576,9 +2847,11 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, ...@@ -2576,9 +2847,11 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) ); fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
else if ( !fNames ) else if ( !fNames )
fprintf( pFile, "x"); fprintf( pFile, "x");
if ( !fNames ) if ( !fNames && fAiger)
fprintf( pFile, "\n"); fprintf( pFile, "\n");
} }
if (fExtended && fAiger && !fNames)
fprintf( pFile, ".\n");
} }
Abc_CexFreeP( &pCare ); Abc_CexFreeP( &pCare );
} }
...@@ -2611,9 +2884,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -2611,9 +2884,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
int fUseFfNames = 0; int fUseFfNames = 0;
int fVerbose = 0; int fVerbose = 0;
int fCexInfo = 0; int fCexInfo = 0;
int fExtended = 0;
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhx" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
...@@ -2653,6 +2927,9 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -2653,6 +2927,9 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
case 'x': case 'x':
fCexInfo ^= 1; fCexInfo ^= 1;
break; break;
case 't':
fExtended ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
...@@ -2702,7 +2979,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -2702,7 +2979,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
{ {
Abc_NtkDumpOneCex( pFile, pNtk, pCex, Abc_NtkDumpOneCex( pFile, pNtk, pCex,
fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
} }
else if ( pAbc->vCexVec ) else if ( pAbc->vCexVec )
{ {
...@@ -2710,10 +2987,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv ) ...@@ -2710,10 +2987,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
{ {
if ( pCex == NULL ) if ( pCex == NULL )
continue; continue;
fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i );
Abc_NtkDumpOneCex( pFile, pNtk, pCex, Abc_NtkDumpOneCex( pFile, pNtk, pCex,
fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo, fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose ); fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
} }
} }
fprintf( pFile, "# DONE\n" ); fprintf( pFile, "# DONE\n" );
...@@ -2760,6 +3037,7 @@ usage: ...@@ -2760,6 +3037,7 @@ usage:
fprintf( pAbc->Err, "\t-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" ); fprintf( pAbc->Err, "\t-x : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" );
fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" ); fprintf( pAbc->Err, "\t-c : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" ); fprintf( pAbc->Err, "\t-a : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-t : extended header info when cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" ); fprintf( pAbc->Err, "\t-f : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" );
fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" ); fprintf( pAbc->Err, "\t-z : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" );
fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pAbc->Err, "\t-v : enable verbose output [default = %s]\n", fVerbose? "yes": "no" );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment