summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c50
-rw-r--r--src/sat/bmc/bmcFault.c86
2 files changed, 105 insertions, 31 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 7b45de68..c01757b1 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -399,7 +399,7 @@ static int Abc_CommandAbc9MultiProve ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Bmc ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9ICheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9SatTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9FunFaTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9FFTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Inse ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Maxi ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -966,10 +966,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&bmc", Abc_CommandAbc9Bmc, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&icheck", Abc_CommandAbc9ICheck, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&sattest", Abc_CommandAbc9SatTest, 0 );
- Cmd_CommandAdd( pAbc, "ABC9", "&funfatest", Abc_CommandAbc9FunFaTest, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&fftest", Abc_CommandAbc9FFTest, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&inse", Abc_CommandAbc9Inse, 0 );
- Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 );
- Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&maxi", Abc_CommandAbc9Maxi, 0 );
+ Cmd_CommandAdd( pAbc, "ABC9", "&bmci", Abc_CommandAbc9Bmci, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&popart2", Abc_CommandAbc9PoPart2, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexcut", Abc_CommandAbc9CexCut, 0 );
// Cmd_CommandAdd( pAbc, "ABC9", "&cexmerge", Abc_CommandAbc9CexMerge, 0 );
@@ -32855,15 +32855,26 @@ usage:
SeeAlso []
***********************************************************************/
-int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9FFTest( Abc_Frame_t * pAbc, int argc, char ** argv )
{
- extern void Gia_ManFaultTest( Gia_Man_t * p, int fStuckAt, int fComplVars, int nTimeOut, int fDump, int fVerbose );
- int c, fStuckAt = 0, fComplVars = 0, nTimeOut = 0, fDump = 0, fVerbose = 0;
+ extern void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose );
+ int c, Algo = 0, fComplVars = 0, nTimeOut = 0, fDump = 0, fVerbose = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "Tscdvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "ATcdvh" ) ) != EOF )
{
switch ( c )
{
+ case 'A':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ Algo = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( Algo < 1 || Algo > 3 )
+ goto usage;
+ break;
case 'T':
if ( globalUtilOptind >= argc )
{
@@ -32875,9 +32886,6 @@ int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nTimeOut < 0 )
goto usage;
break;
- case 's':
- fStuckAt ^= 1;
- break;
case 'c':
fComplVars ^= 1;
break;
@@ -32895,23 +32903,27 @@ int Abc_CommandAbc9FunFaTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->pGia == NULL )
{
- Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): There is no AIG.\n" );
+ Abc_Print( -1, "Abc_CommandAbc9FFTest(): There is no AIG.\n" );
return 0;
}
- if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+ if ( Gia_ManRegNum(pAbc->pGia) == 0 && Algo == 1 )
{
- Abc_Print( -1, "Abc_CommandAbc9FunFaTest(): AIG is combinational.\n" );
+ Abc_Print( -1, "Abc_CommandAbc9FFTest(): For delay testing, AIG should be sequential.\n" );
return 0;
}
- Gia_ManFaultTest( pAbc->pGia, fStuckAt, fComplVars, nTimeOut, fDump, fVerbose );
+ Gia_ManFaultTest( pAbc->pGia, Algo, fComplVars, nTimeOut, fDump, fVerbose );
return 0;
usage:
- Abc_Print( -2, "usage: &funfatest [-T num] [-scdvh]\n" );
+ Abc_Print( -2, "usage: &fftest [-AT num] [-cdvh]\n" );
Abc_Print( -2, "\t performs functional fault test generation\n" );
- Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
- Abc_Print( -2, "\t-s : toggles generating tests for stuck-at faults [default = %s]\n", fStuckAt? "yes": "no" );
- Abc_Print( -2, "\t-c : toggles complementing control variables [default = %s]\n", fComplVars? "yes": "no" );
+ Abc_Print( -2, "\t-A num : selects test generation algorithm [default = %d]\n", Algo );
+ Abc_Print( -2, "\t 0: algorithm is not selected\n" );
+ Abc_Print( -2, "\t 1: delay fault testing for sequential circuits\n" );
+ Abc_Print( -2, "\t 2: traditional stuck-at testing\n" );
+ Abc_Print( -2, "\t 3: complement fault testing\n" );
+ Abc_Print( -2, "\t-T num : specifies approximate runtime limit in seconds [default = %d]\n", nTimeOut );
+ Abc_Print( -2, "\t-c : toggles complementing control variables [default = %s]\n", fComplVars? "active-high": "active-low" );
Abc_Print( -2, "\t-d : toggles dumping test patterns into file \"tests.txt\" [default = %s]\n", fDump? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
diff --git a/src/sat/bmc/bmcFault.c b/src/sat/bmc/bmcFault.c
index d5615a75..524b305f 100644
--- a/src/sat/bmc/bmcFault.c
+++ b/src/sat/bmc/bmcFault.c
@@ -116,7 +116,7 @@ Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fComplVars )
iCtrl = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
if ( fUseMuxes )
- pObj->Value = Gia_ManHashMux( pNew, iCtrl, iThis, pObj->Value );
+ pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis );
else
pObj->Value = iThis;
}
@@ -157,8 +157,8 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars
iCtrl1 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
if ( fUseFaults )
{
- pObj->Value = Gia_ManHashAnd( pNew, iCtrl0, pObj->Value );
- pObj->Value = Gia_ManHashOr( pNew, Abc_LitNot(iCtrl1), pObj->Value );
+ pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(iCtrl0), pObj->Value );
+ pObj->Value = Gia_ManHashOr( pNew, iCtrl1, pObj->Value );
}
}
Gia_ManForEachCo( p, pObj, i )
@@ -180,6 +180,43 @@ Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars
SeeAlso []
***********************************************************************/
+Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, int fUseFaults, int fComplVars )
+{
+ Gia_Man_t * pNew, * pTemp;
+ Gia_Obj_t * pObj;
+ int i, iCtrl0;
+ pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) );
+ pNew->pName = Abc_UtilStrsav( p->pName );
+ Gia_ManHashAlloc( pNew );
+ Gia_ManConst0(p)->Value = 0;
+ Gia_ManForEachCi( p, pObj, i )
+ pObj->Value = Gia_ManAppendCi( pNew );
+ Gia_ManForEachAnd( p, pObj, i )
+ {
+ pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+ iCtrl0 = Abc_LitNotCond( Gia_ManAppendCi(pNew), fComplVars );
+ if ( fUseFaults )
+ pObj->Value = Gia_ManHashXor( pNew, iCtrl0, pObj->Value );
+ }
+ Gia_ManForEachCo( p, pObj, i )
+ pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+ pNew = Gia_ManCleanup( pTemp = pNew );
+ Gia_ManStop( pTemp );
+ assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + Gia_ManAndNum(p) );
+ return pNew;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
{
Gia_Man_t * pNew, * pTemp;
@@ -270,24 +307,49 @@ void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime c
SeeAlso []
***********************************************************************/
-void Gia_ManFaultTest( Gia_Man_t * p, int fStuckAt, int fComplVars, int nTimeOut, int fDump, int fVerbose )
+void Gia_ManFaultTest( Gia_Man_t * p, int Algo, int fComplVars, int nTimeOut, int fDump, int fVerbose )
{
int nIterMax = 1000000;
- int i, Iter, status;
+ int i, Iter, status, nFuncVars = -1;
abctime clkTotal = Abc_Clock();
abctime clkSat = 0;
- int nFuncVars = fStuckAt ? Gia_ManCiNum(p) : Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
Vec_Int_t * vLits, * vTests;
sat_solver * pSat;
Gia_Obj_t * pObj;
- Gia_Man_t * pC;
- Gia_Man_t * p0 = fStuckAt ? Gia_ManStuckAtUnfold(p, 0, fComplVars) : Gia_ManFaultUnfold(p, 0, fComplVars);
- Gia_Man_t * p1 = fStuckAt ? Gia_ManStuckAtUnfold(p, 1, fComplVars) : Gia_ManFaultUnfold(p, 1, fComplVars);
- Gia_Man_t * pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
- Cnf_Dat_t * pCnf = Cnf_DeriveGiaRemapped( pM ), * pCnf2;
+ Gia_Man_t * pC, * p0, * p1, * pM;
+ Cnf_Dat_t * pCnf, * pCnf2;
+
+ // select algorithm
+ if ( Algo == 1 )
+ {
+ assert( Gia_ManRegNum(p) > 0 );
+ nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
+ p0 = Gia_ManFaultUnfold( p, 0, fComplVars );
+ p1 = Gia_ManFaultUnfold( p, 1, fComplVars );
+ }
+ else if ( Algo == 2 )
+ {
+ nFuncVars = Gia_ManCiNum(p);
+ p0 = Gia_ManStuckAtUnfold( p, 0, fComplVars );
+ p1 = Gia_ManStuckAtUnfold( p, 1, fComplVars );
+ }
+ else if ( Algo == 3 )
+ {
+ nFuncVars = Gia_ManCiNum(p);
+ p0 = Gia_ManFlipUnfold( p, 0, fComplVars );
+ p1 = Gia_ManFlipUnfold( p, 1, fComplVars );
+ }
+ else
+ {
+ printf( "Unregnized algorithm (%d).\n", Algo );
+ return;
+ }
+
+ // create miter
+ pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
+ pCnf = Cnf_DeriveGiaRemapped( pM );
Gia_ManStop( p0 );
Gia_ManStop( p1 );
- assert( Gia_ManRegNum(p) > 0 );
// start the SAT solver
pSat = sat_solver_new();
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-01 01:55:49 +0000