luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Added command "testcex".

This commit is contained in:
Alan Mishchenko 2010-11-28 19:32:19 -08:00
parent 093774c1b8
commit 98257daa82
1 changed files with 310 additions and 52 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

310
src/base/abci/abc.c
View File

@ -129,6 +129,7 @@ static int Abc_CommandDemiter ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOrPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAndPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandZeroPo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandZeroPo ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSwapPos ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAppend ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFrames ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandDFrames ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDFrames ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -164,6 +165,8 @@ static int Abc_CommandQuaVar ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQuaRel ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandQuaReach ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSenseInput ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSenseInput ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNpnLoad ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandNpnSave ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandICut ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -269,6 +272,7 @@ static int Abc_CommandConstr ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandUnfold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFold ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandBm ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTestCex ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTraceStart ( 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 ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -524,6 +528,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "orpos", Abc_CommandOrPos, 1 ); Cmd_CommandAdd( pAbc, "Various", "orpos", Abc_CommandOrPos, 1 );
Cmd_CommandAdd( pAbc, "Various", "andpos", Abc_CommandAndPos, 1 ); Cmd_CommandAdd( pAbc, "Various", "andpos", Abc_CommandAndPos, 1 );
Cmd_CommandAdd( pAbc, "Various", "zeropo", Abc_CommandZeroPo, 1 ); Cmd_CommandAdd( pAbc, "Various", "zeropo", Abc_CommandZeroPo, 1 );
Cmd_CommandAdd( pAbc, "Various", "swappos", Abc_CommandSwapPos, 1 );
Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 ); Cmd_CommandAdd( pAbc, "Various", "append", Abc_CommandAppend, 1 );
Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "frames", Abc_CommandFrames, 1 );
Cmd_CommandAdd( pAbc, "Various", "dframes", Abc_CommandDFrames, 1 ); Cmd_CommandAdd( pAbc, "Various", "dframes", Abc_CommandDFrames, 1 );
@ -560,6 +565,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "qrel", Abc_CommandQuaRel, 1 ); Cmd_CommandAdd( pAbc, "Various", "qrel", Abc_CommandQuaRel, 1 );
Cmd_CommandAdd( pAbc, "Various", "qreach", Abc_CommandQuaReach, 1 ); Cmd_CommandAdd( pAbc, "Various", "qreach", Abc_CommandQuaReach, 1 );
Cmd_CommandAdd( pAbc, "Various", "senseinput", Abc_CommandSenseInput, 1 ); Cmd_CommandAdd( pAbc, "Various", "senseinput", Abc_CommandSenseInput, 1 );
Cmd_CommandAdd( pAbc, "Various", "npnload", Abc_CommandNpnLoad, 0 );
Cmd_CommandAdd( pAbc, "Various", "npnsave", Abc_CommandNpnSave, 0 );
Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 );
Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 ); Cmd_CommandAdd( pAbc, "New AIG", "icut", Abc_CommandICut, 0 );
@ -663,6 +670,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "unfold", Abc_CommandUnfold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 ); Cmd_CommandAdd( pAbc, "Verification", "fold", Abc_CommandFold, 1 );
Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 ); Cmd_CommandAdd( pAbc, "Verification", "bm", Abc_CommandBm, 1 );
Cmd_CommandAdd( pAbc, "Verification", "testcex", Abc_CommandTestCex, 0 );
Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 ); Cmd_CommandAdd( pAbc, "ABC8", "*r", Abc_CommandAbc8Read, 0 );
@ -858,6 +866,10 @@ void Abc_End( Abc_Frame_t * pAbc )
extern void Aig_RManQuit(); extern void Aig_RManQuit();
Aig_RManQuit(); Aig_RManQuit();
} }
{
extern void Npn_ManClean();
Npn_ManClean();
}
Abc_NtkFraigStoreClean(); Abc_NtkFraigStoreClean();
if ( Abc_FrameGetGlobalFrame()->pGia ) if ( Abc_FrameGetGlobalFrame()->pGia )
Gia_ManStop( Abc_FrameGetGlobalFrame()->pGia ); Gia_ManStop( Abc_FrameGetGlobalFrame()->pGia );
@ -5715,7 +5727,76 @@ int Abc_CommandZeroPo( Abc_Frame_t * pAbc, int argc, char ** argv )
usage: usage:
Abc_Print( -2, "usage: zeropo [-N num] [-h]\n" ); Abc_Print( -2, "usage: zeropo [-N num] [-h]\n" );
Abc_Print( -2, "\t replaces the PO driver by constant 0\n" ); Abc_Print( -2, "\t replaces the PO driver by constant 0\n" );
Abc_Print( -2, "\t-F num : the zero-based index of the PO to replace [default = %d]\n", iOutput ); Abc_Print( -2, "\t-N num : the zero-based index of the PO to replace [default = %d]\n", iOutput );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandSwapPos( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes;
int c, iOutput = -1;
extern void Abc_NtkSwapOneOutput( Abc_Ntk_t * pNtk, int iOutput );
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF )
{
switch ( c )
{
case 'N':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" );
goto usage;
}
iOutput = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( iOutput < 0 )
goto usage;
break;
default:
goto usage;
}
}
if ( !Abc_NtkIsStrash(pNtk) )
{
Abc_Print( -1, "The network is not strashed.\n" );
return 1;
}
if ( iOutput < 0 )
{
Abc_Print( -1, "The output index is not specified.\n" );
return 1;
}
if ( iOutput >= Abc_NtkPoNum(pNtk) )
{
Abc_Print( -1, "The output index is larger than the allowed POs.\n" );
return 1;
}
// get the new network
pNtkRes = Abc_NtkDup( pNtk );
Abc_NtkSwapOneOutput( pNtkRes, iOutput );
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
return 0;
usage:
Abc_Print( -2, "usage: swappos [-N num] [-h]\n" );
Abc_Print( -2, "\t swap the 0-th PO with the <num>-th PO\n" );
Abc_Print( -2, "\t-N num : the zero-based index of the PO to swap [default = %d]\n", iOutput );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
} }
@ -7451,12 +7532,13 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
pParams->fGlobal = 0; // compute global cuts pParams->fGlobal = 0; // compute global cuts
pParams->fLocal = 0; // compute local cuts pParams->fLocal = 0; // compute local cuts
pParams->fFancy = 0; // compute something fancy pParams->fFancy = 0; // compute something fancy
pParams->fRecordAig= 1; // compute something fancy pParams->fRecordAig = 1; // compute something fancy
pParams->fMap = 0; // compute mapping delay pParams->fMap = 0; // compute mapping delay
pParams->fAdjust = 1; // removes useless fanouts pParams->fAdjust = 0; // removes useless fanouts
pParams->fNpnSave = 0; // enables dumping truth tables
pParams->fVerbose = 0; // the verbosiness flag pParams->fVerbose = 0; // the verbosiness flag
Extra_UtilGetoptReset(); Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzamjvoh" ) ) != EOF ) while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdxyglzamjvosh" ) ) != EOF )
{ {
switch ( c ) switch ( c )
{ {
@ -7521,6 +7603,9 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'o': case 'o':
fOracle ^= 1; fOracle ^= 1;
break; break;
case 's':
pParams->fNpnSave ^= 1;
break;
case 'h': case 'h':
goto usage; goto usage;
default: default:
@ -7549,6 +7634,12 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
return 1; return 1;
} }
if ( pParams->fNpnSave )
{
pParams->nVarsMax = 6;
pParams->fTruth = 1;
}
if ( fOracle ) if ( fOracle )
pParams->fRecord = 1; pParams->fRecord = 1;
pCutMan = Abc_NtkCuts( pNtk, pParams ); pCutMan = Abc_NtkCuts( pNtk, pParams );
@ -7564,7 +7655,7 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
Abc_Print( -2, "usage: cut [-K num] [-M num] [-tfdcovamjvh]\n" ); Abc_Print( -2, "usage: cut [-K num] [-M num] [-tfdcovamjsvh]\n" );
Abc_Print( -2, "\t computes k-feasible cuts for the AIG\n" ); Abc_Print( -2, "\t computes k-feasible cuts for the AIG\n" );
Abc_Print( -2, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax ); Abc_Print( -2, "\t-K num : max number of leaves (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, pParams->nVarsMax );
Abc_Print( -2, "\t-M num : max number of cuts stored at a node [default = %d]\n", pParams->nKeepMax ); Abc_Print( -2, "\t-M num : max number of cuts stored at a node [default = %d]\n", pParams->nKeepMax );
@ -7579,6 +7670,7 @@ usage:
Abc_Print( -2, "\t-a : toggle recording cut functions [default = %s]\n", pParams->fRecordAig?"yes": "no" ); Abc_Print( -2, "\t-a : toggle recording cut functions [default = %s]\n", pParams->fRecordAig?"yes": "no" );
Abc_Print( -2, "\t-m : toggle delay-oriented FPGA mapping [default = %s]\n", pParams->fMap? "yes": "no" ); Abc_Print( -2, "\t-m : toggle delay-oriented FPGA mapping [default = %s]\n", pParams->fMap? "yes": "no" );
Abc_Print( -2, "\t-j : toggle removing fanouts due to XOR/MUX [default = %s]\n", pParams->fAdjust? "yes": "no" ); Abc_Print( -2, "\t-j : toggle removing fanouts due to XOR/MUX [default = %s]\n", pParams->fAdjust? "yes": "no" );
Abc_Print( -2, "\t-s : toggle creating library of 6-var functions [default = %s]\n", pParams->fNpnSave? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
return 1; return 1;
@ -8298,18 +8390,22 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
goto usage; goto usage;
} }
} }
/*
if ( pNtk == NULL ) if ( pNtk == NULL )
{ {
Abc_Print( -1, "Empty network.\n" ); Abc_Print( -1, "Empty network.\n" );
return 1; return 1;
} }
if ( Abc_NtkIsSeq(pNtk) ) if ( Abc_NtkLatchNum(pNtk) == 0 )
{ {
Abc_Print( -1, "Only works for non-sequential networks.\n" ); Abc_Print( -1, "Only works for sequential networks.\n" );
return 1; return 1;
} }
*/ {
extern void Abc_NtkDarTest( Abc_Ntk_t * pNtk );
Abc_NtkDarTest( pNtk );
}
// Abc_NtkTestEsop( pNtk ); // Abc_NtkTestEsop( pNtk );
// Abc_NtkTestSop( pNtk ); // Abc_NtkTestSop( pNtk );
@ -10578,6 +10674,87 @@ usage:
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandNpnLoad( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Npn_ManLoad( char * pFileName );
char * pFileName;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
pFileName = argv[globalUtilOptind];
Npn_ManLoad( pFileName );
return 0;
usage:
Abc_Print( -2, "usage: npnload <filename>\n" );
Abc_Print( -2, "\t loads previously saved 6-input function library from file\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandNpnSave( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Npn_ManSave( char * pFileName );
char * pFileName;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
default:
goto usage;
}
}
if ( argc != globalUtilOptind + 1 )
goto usage;
pFileName = argv[globalUtilOptind];
Npn_ManSave( pFileName );
return 0;
usage:
Abc_Print( -2, "usage: npnsave <filename>\n" );
Abc_Print( -2, "\t saves current 6-input function library into file\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************
@ -11629,7 +11806,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv )
} }
if ( fAreaOnly ) if ( fAreaOnly )
DelayTarget = 100000.0; DelayTarget = ABC_INFINITY;
if ( !Abc_NtkIsStrash(pNtk) ) if ( !Abc_NtkIsStrash(pNtk) )
{ {
@ -19341,7 +19518,7 @@ int Abc_CommandBm( Abc_Frame_t * pAbc, int argc, char ** argv )
p_equivalence = 1; p_equivalence = 1;
break; break;
default: default:
fprintf( pErr, "Unkown switch.\n"); Abc_Print( -2, "Unkown switch.\n");
goto usage; goto usage;
} }
} }
@ -19353,7 +19530,7 @@ int Abc_CommandBm( Abc_Frame_t * pAbc, int argc, char ** argv )
if( (unsigned)Abc_NtkPiNum(pNtk1) != (unsigned)Abc_NtkPiNum(pNtk2) || (unsigned)Abc_NtkPoNum(pNtk1) != (unsigned)Abc_NtkPoNum(pNtk2) ) if( (unsigned)Abc_NtkPiNum(pNtk1) != (unsigned)Abc_NtkPiNum(pNtk2) || (unsigned)Abc_NtkPoNum(pNtk1) != (unsigned)Abc_NtkPoNum(pNtk2) )
{ {
fprintf( pErr, "Mismatch in the number of inputs or outputs\n"); Abc_Print( -2, "Mismatch in the number of inputs or outputs\n");
if ( fDelete1 ) Abc_NtkDelete( pNtk1 ); if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
if ( fDelete2 ) Abc_NtkDelete( pNtk2 ); if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
return 1; return 1;
@ -19366,25 +19543,106 @@ int Abc_CommandBm( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0; return 0;
usage: usage:
fprintf( pErr, "usage: bm [-P] <file1> <file2>\n" ); Abc_Print( -2, "usage: bm [-P] <file1> <file2>\n" );
fprintf( pErr, "\t performs Boolean matching (P-equivalence & PP-equivalence)\n" ); Abc_Print( -2, "\t performs Boolean matching (P-equivalence & PP-equivalence)\n" );
fprintf( pErr, "\t for equivalent circuits, I/O matches are printed in IOmatch.txt\n" ); Abc_Print( -2, "\t for equivalent circuits, I/O matches are printed in IOmatch.txt\n" );
fprintf( pErr, "\t-P : performs P-equivalnce checking\n"); Abc_Print( -2, "\t-P : performs P-equivalnce checking\n");
fprintf( pErr, "\t default is PP-equivalence checking (when -P is not provided)\n" ); Abc_Print( -2, "\t default is PP-equivalence checking (when -P is not provided)\n" );
fprintf( pErr, "\t-h : print the command usage\n"); Abc_Print( -2, "\t-h : print the command usage\n");
fprintf( pErr, "\tfile1 : the file with the first network\n"); Abc_Print( -2, "\tfile1 : the file with the first network\n");
fprintf( pErr, "\tfile2 : the file with the second network\n"); Abc_Print( -2, "\tfile2 : the file with the second network\n");
fprintf( pErr, "\t \n" ); Abc_Print( -2, "\t \n" );
fprintf( pErr, "\t This command was contributed by Hadi Katebi from U Michigan.\n" ); Abc_Print( -2, "\t This command was contributed by Hadi Katebi from U Michigan.\n" );
fprintf( pErr, "\t The paper describing the method: H. Katebi and I. L. Markov.\n" ); Abc_Print( -2, "\t The paper describing the method: H. Katebi and I. L. Markov.\n" );
fprintf( pErr, "\t \"Large-scale Boolean matching\". Proc. DATE 2010. \n" ); Abc_Print( -2, "\t \"Large-scale Boolean matching\". Proc. DATE 2010. \n" );
fprintf( pErr, "\t http://www.eecs.umich.edu/~imarkov/pubs/conf/date10-match.pdf\n" ); Abc_Print( -2, "\t http://www.eecs.umich.edu/~imarkov/pubs/conf/date10-match.pdf\n" );
fprintf( pErr, "\t \n" ); Abc_Print( -2, "\t \n" );
return 1; return 1;
} }
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandTestCex( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Abc_Ntk_t * pNtk;
int c;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
{
switch ( c )
{
case 'h':
goto usage;
}
}
if ( pAbc->pCex == NULL )
{
Abc_Print( 1, "There is no current cex.\n");
return 0;
}
// check the main AIG
pNtk = Abc_FrameReadNtk(pAbc);
if ( pNtk == NULL )
Abc_Print( 1, "Main AIG: There is no current network.\n");
else if ( !Abc_NtkIsStrash(pNtk) )
Abc_Print( 1, "Main AIG: The current network is not an AIG.\n");
else if ( Abc_NtkPiNum(pNtk) != pAbc->pCex->nPis )
Abc_Print( 1, "Main AIG: The number of PIs (%d) is different from cex (%d).\n", Abc_NtkPiNum(pNtk), pAbc->pCex->nPis );
else if ( Abc_NtkLatchNum(pNtk) != pAbc->pCex->nRegs )
Abc_Print( 1, "Main AIG: The number of registers (%d) is different from cex (%d).\n", Abc_NtkLatchNum(pNtk), pAbc->pCex->nRegs );
else if ( Abc_NtkPoNum(pNtk) <= pAbc->pCex->iPo )
Abc_Print( 1, "Main AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Abc_NtkPoNum(pNtk), pAbc->pCex->iPo );
else
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
Gia_Man_t * pGia = Gia_ManFromAigSimple( pAig );
Aig_ManStop( pAig );
if ( !Gia_ManVerifyCounterExample( pGia, pAbc->pCex, 0 ) )
Abc_Print( 1, "Main AIG: The cex does not fail any outputs.\n" );
else
Abc_Print( 1, "Main AIG: The cex is correct.\n" );
Gia_ManStop( pGia );
}
// check the AND AIG
if ( pAbc->pGia == NULL )
Abc_Print( 1, "And AIG: There is no current network.\n");
else if ( Gia_ManPiNum(pAbc->pGia) != pAbc->pCex->nPis )
Abc_Print( 1, "And AIG: The number of PIs (%d) is different from cex (%d).\n", Gia_ManPiNum(pAbc->pGia), pAbc->pCex->nPis );
else if ( Gia_ManRegNum(pAbc->pGia) != pAbc->pCex->nRegs )
Abc_Print( 1, "And AIG: The number of registers (%d) is different from cex (%d).\n", Gia_ManRegNum(pAbc->pGia), pAbc->pCex->nRegs );
else if ( Gia_ManPoNum(pAbc->pGia) <= pAbc->pCex->iPo )
Abc_Print( 1, "And AIG: The number of POs (%d) is less than the PO index in cex (%d).\n", Gia_ManPoNum(pAbc->pGia), pAbc->pCex->iPo );
else
{
if ( !Gia_ManVerifyCounterExample( pAbc->pGia, pAbc->pCex, 0 ) )
Abc_Print( 1, "And AIG: The cex does not fail any outputs.\n" );
else
Abc_Print( 1, "And AIG: The cex is correct.\n" );
}
return 0;
usage:
Abc_Print( -2, "usage: testcex -h\n" );
Abc_Print( -2, "\t tests the current cex against the current AIG and &-AIG\n" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}
/**Function************************************************************* /**Function*************************************************************