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

Usability improvements to &fftest.

This commit is contained in:
Alan Mishchenko 2018-11-11 23:06:05 -08:00
parent 8b310db513
commit e9c00fb024
3 changed files with 32 additions and 11 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -41762,7 +41762,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
int c;
Gia_ParFfSetDefault( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfdeunvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "ATNKSGkbsfcdeunvh" ) ) != EOF )
{
switch ( c )
{
@ -41840,6 +41840,9 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'f':
pPars->fFfOnly ^= 1;
break;
case 'c':
pPars->fCheckUntest ^= 1;
break;
case 'd':
pPars->fDump ^= 1;
break;
@ -41930,7 +41933,7 @@ int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfdeunvh] <file> [-G file] [-S str]\n" );
Abc_Print( -2, "usage: &fftest [-ATNK num] [-kbsfcdeunvh] <file> [-G file] [-S str]\n" );
Abc_Print( -2, "\t performs functional fault test generation\n" );
Abc_Print( -2, "\t-A num : selects fault model for all gates [default = %d]\n", pPars->Algo );
Abc_Print( -2, "\t 0: fault model is not selected (use -S str)\n" );
@ -41945,9 +41948,10 @@ usage:
Abc_Print( -2, "\t-b : toggles testing for single faults (the same as \"-K 1\") [default = %s]\n", pPars->fBasic? "yes": "no" );
Abc_Print( -2, "\t-s : toggles starting with the all-0 and all-1 patterns [default = %s]\n", pPars->fStartPats? "yes": "no" );
Abc_Print( -2, "\t-f : toggles faults at flop inputs only with \"-A 1\" and \"-S str\" [default = %s]\n", pPars->fFfOnly? "yes": "no" );
Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", pPars->fDump? "yes": "no" );
Abc_Print( -2, "\t-c : toggles checking if there are untestable faults [default = %s]\n", pPars->fCheckUntest? "yes": "no" );
Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"<file>_tests.txt\" [default = %s]\n", pPars->fDump? "yes": "no" );
Abc_Print( -2, "\t-e : toggles dumping test pattern pairs (delay faults only) [default = %s]\n", pPars->fDumpDelay? "yes": "no" );
Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" );
Abc_Print( -2, "\t-u : toggles dumping untestable faults into \"<file>_untest.txt\" [default = %s]\n", pPars->fDumpUntest? "yes": "no" );
Abc_Print( -2, "\t-n : toggles dumping faults not detected by a given test set [default = %s]\n", pPars->fDumpNewFaults? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");

1
src/sat/bmc/bmc.h
View File

@ -188,6 +188,7 @@ struct Bmc_ParFf_t_
int fNonStrict;
int fBasic;
int fFfOnly;
int fCheckUntest;
int fDump;
int fDumpDelay;
int fDumpUntest;

30
src/sat/bmc/bmcFault.c
View File

@ -22,6 +22,7 @@
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
@ -58,6 +59,7 @@ void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
p->nIterCheck = 0;
p->fBasic = 0;
p->fFfOnly = 0;
p->fCheckUntest = 0;
p->fDump = 0;
p->fDumpUntest = 0;
p->fVerbose = 0;
@ -476,6 +478,7 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0;
int VarLimit = 4 * Gia_ManAndNum(p);
pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
pNew->pName = Abc_UtilStrsav( p->pName );
Gia_ManHashAlloc( pNew );
@ -484,22 +487,22 @@ Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
pObj->Value = Gia_ManAppendCi( pNew );
Gia_ManForEachAnd( p, pObj, i )
{
if ( Vec_IntEntry(vMap, iFuncVars++) )
if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl0 = Gia_ManAppendCi(pNew);
else
iCtrl0 = 0, Gia_ManAppendCi(pNew);
if ( Vec_IntEntry(vMap, iFuncVars++) )
if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl1 = Gia_ManAppendCi(pNew);
else
iCtrl1 = 0, Gia_ManAppendCi(pNew);
if ( Vec_IntEntry(vMap, iFuncVars++) )
if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl2 = Gia_ManAppendCi(pNew);
else
iCtrl2 = 0, Gia_ManAppendCi(pNew);
if ( Vec_IntEntry(vMap, iFuncVars++) )
if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
iCtrl3 = Gia_ManAppendCi(pNew);
else
iCtrl3 = 0, Gia_ManAppendCi(pNew);
@ -1441,6 +1444,19 @@ void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
return;
}
printf( "Options: " );
printf( "Untestable faults = %s. ", pPars->fCheckUntest || pPars->fDumpDelay ? "yes": "no" );
if ( pPars->nCardConstr )
printf( "Using %sstrict cardinality %d. ", pPars->fNonStrict ? "non-" : "", pPars->nCardConstr );
if ( pPars->fFfOnly )
printf( "Faults at FF outputs only = yes. " );
if ( pPars->nTimeOut )
printf( "Runtime limit = %d sec. ", pPars->nTimeOut );
if ( p != pG && pG->pSpec )
printf( "Golden model = %s. ", pG->pSpec );
printf( "Verbose = %s. ", pPars->fVerbose ? "yes": "no" );
printf( "\n" );
// select algorithm
if ( pPars->Algo == 0 )
nFuncVars = Gia_ManCiNum(p);
@ -1565,7 +1581,7 @@ finish:
// dump the test suite
if ( pPars->fDump )
{
char * pFileName = "tests.txt";
char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_tests.txt") : "tests.txt";
if ( pPars->fDumpDelay && pPars->Algo == 1 )
{
Gia_ManDumpTestsDelay( vTests, Iter, pFileName, p );
@ -1579,7 +1595,7 @@ finish:
}
// compute untestable faults
if ( Iter && (p != pG || pPars->fDumpUntest) )
if ( Iter && (p != pG || pPars->fDumpUntest || pPars->fCheckUntest) )
{
abctime clkTotal = Abc_Clock();
// restart the SAT solver
@ -1680,7 +1696,7 @@ finish:
if ( pPars->fDumpUntest && status == l_True )
{
abctime clk = Abc_Clock();
char * pFileName = "untest.txt";
char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_untest.txt") : "untest.txt";
int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose );
if ( p == pG )
printf( "Dumped %d untestable multiple faults into file \"%s\". ", nUntests, pFileName );