abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcFault.c File Reference
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Macros

#define FFTEST_MAX_VARS   2
 DECLARATIONS ///. More...
 
#define FFTEST_MAX_PARS   8
 

Functions

void Gia_ParFfSetDefault (Bmc_ParFf_t *p)
 FUNCTION DEFINITIONS ///. More...
 
static int Cnf_AddCardinConstr (sat_solver *p, Vec_Int_t *vVars)
 
void Cnf_AddCardinConstrTest ()
 
static Cnf_Dat_tCnf_DeriveGiaRemapped (Gia_Man_t *p)
 
static void Cnf_DataLiftGia (Cnf_Dat_t *p, Gia_Man_t *pGia, int nVarsPlus)
 
Gia_Man_tGia_ManFaultUnfold (Gia_Man_t *p, int fUseMuxes)
 
Gia_Man_tGia_ManStuckAtUnfold (Gia_Man_t *p, Vec_Int_t *vMap)
 
Gia_Man_tGia_ManFlipUnfold (Gia_Man_t *p, Vec_Int_t *vMap)
 
Gia_Man_tGia_ManFOFUnfold (Gia_Man_t *p, Vec_Int_t *vMap)
 
int Gia_FormStrCount (char *pStr, int *pnVars, int *pnPars)
 
void Gia_FormStrTransform (char *pStr, char *pForm)
 
char * Gia_ManFormulaEndToken (char *pForm)
 
int Gia_ManRealizeFormula_rec (Gia_Man_t *p, int *pVars, int *pPars, char *pBeg, char *pEnd, int nPars)
 
int Gia_ManRealizeFormula (Gia_Man_t *p, int *pVars, int *pPars, char *pStr, int nPars)
 
Gia_Man_tGia_ManFormulaUnfold (Gia_Man_t *p, char *pForm)
 
Gia_Man_tGia_ManFaultCofactor (Gia_Man_t *p, Vec_Int_t *vValues)
 
void Gia_ManDumpTests (Vec_Int_t *vTests, int nIter, char *pFileName)
 
void Gia_ManPrintResults (Gia_Man_t *p, sat_solver *pSat, int nIter, abctime clk)
 
int Gia_ManFaultAddOne (Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, Vec_Int_t *vLits, int nFuncVars)
 
int Gia_ManDumpUntests (Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, int nFuncVars, char *pFileName, int fVerbose)
 
Vec_Int_tGia_ManGetTestPatterns (char *pFileName)
 
Gia_Man_tGia_ManDeriveDup (Gia_Man_t *p, int nPisNew)
 
int Gia_ManFaultAnalyze (sat_solver *pSat, Vec_Int_t *vPars, Vec_Int_t *vMap, Vec_Int_t *vLits, int Iter)
 
int Gia_ManFaultPrepare (Gia_Man_t *p, Gia_Man_t *pG, Bmc_ParFf_t *pPars, int nFuncVars, Vec_Int_t *vMap, Vec_Int_t *vTests, Vec_Int_t *vLits, Gia_Man_t **ppMiter, Cnf_Dat_t **ppCnf, sat_solver **ppSat, int fWarmUp)
 
void Gia_ManFaultTest (Gia_Man_t *p, Gia_Man_t *pG, Bmc_ParFf_t *pPars)
 

Macro Definition Documentation

#define FFTEST_MAX_PARS   8

Definition at line 34 of file bmcFault.c.

#define FFTEST_MAX_VARS   2

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcFault.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Checking for functional faults.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
bmcFault.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 33 of file bmcFault.c.

Function Documentation

static int Cnf_AddCardinConstr ( sat_solver p,
Vec_Int_t vVars 
)
inlinestatic

Function*************************************************************

Synopsis [Add constraint that no more than 1 variable is 1.]

Description []

SideEffects []

SeeAlso []

Definition at line 76 of file bmcFault.c.

77 {
78  int i, k, pLits[2], iVar, nVars = sat_solver_nvars(p);
79  Vec_IntForEachEntry( vVars, iVar, i )
80  assert( iVar >= 0 && iVar < nVars );
81  iVar = nVars;
82  sat_solver_setnvars( p, nVars + Vec_IntSize(vVars) - 1 );
83  while ( Vec_IntSize(vVars) > 1 )
84  {
85  for ( k = i = 0; i < Vec_IntSize(vVars)/2; i++ )
86  {
87  pLits[0] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i), 1 );
88  pLits[1] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i+1), 1 );
89  sat_solver_addclause( p, pLits, pLits + 2 );
90  sat_solver_add_and( p, iVar, Vec_IntEntry(vVars, 2*i), Vec_IntEntry(vVars, 2*i+1), 1, 1, 1 );
91  Vec_IntWriteEntry( vVars, k++, iVar++ );
92  }
93  if ( Vec_IntSize(vVars) & 1 )
94  Vec_IntWriteEntry( vVars, k++, Vec_IntEntryLast(vVars) );
95  Vec_IntShrink( vVars, k );
96  }
97  return iVar;
98 }
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
static int Vec_IntEntryLast(Vec_Int_t *p)
Definition: bblif.c:319
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int sat_solver_add_and(sat_solver *pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1, int fCompl)
Definition: satSolver.h:324
void Cnf_AddCardinConstrTest ( )

Definition at line 99 of file bmcFault.c.

100 {
101  int i, status, nVars = 7;
102  Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
103  sat_solver * pSat = sat_solver_new();
104  sat_solver_setnvars( pSat, nVars );
105  Cnf_AddCardinConstr( pSat, vVars );
106  while ( 1 )
107  {
108  status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
109  if ( status != l_True )
110  break;
111  Vec_IntClear( vVars );
112  for ( i = 0; i < nVars; i++ )
113  {
114  Vec_IntPush( vVars, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
115  printf( "%d", sat_solver_var_value(pSat, i) );
116  }
117  printf( "\n" );
118  status = sat_solver_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
119  if ( status == 0 )
120  break;
121  }
122  sat_solver_delete( pSat );
123  Vec_IntFree( vVars );
124 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
#define l_True
Definition: SolverTypes.h:84
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
static int Cnf_AddCardinConstr(sat_solver *p, Vec_Int_t *vVars)
Definition: bmcFault.c:76
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static void Cnf_DataLiftGia ( Cnf_Dat_t p,
Gia_Man_t pGia,
int  nVarsPlus 
)
inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 159 of file bmcFault.c.

160 {
161  Gia_Obj_t * pObj;
162  int v;
163  Gia_ManForEachObj( pGia, pObj, v )
164  if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 )
165  p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus;
166  for ( v = 0; v < p->nLiterals; v++ )
167  p->pClauses[0][v] += 2*nVarsPlus;
168 }
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
if(last==0)
Definition: sparse_int.h:34
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static Cnf_Dat_t* Cnf_DeriveGiaRemapped ( Gia_Man_t p)
inlinestatic

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file bmcFault.c.

138 {
139  Cnf_Dat_t * pCnf;
140  Aig_Man_t * pAig = Gia_ManToAigSimple( p );
141  pAig->nRegs = 0;
142  pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
143  Aig_ManStop( pAig );
144  return pCnf;
145 // return Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
146 }
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Definition: cnf.h:56
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
int Gia_FormStrCount ( char *  pStr,
int *  pnVars,
int *  pnPars 
)

Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file bmcFault.c.

383 {
384  int i, Counter = 0;
385  if ( pStr[0] != '(' )
386  {
387  printf( "The first symbol should be the opening paranthesis \"(\".\n" );
388  return 1;
389  }
390  if ( pStr[strlen(pStr)-1] != ')' )
391  {
392  printf( "The last symbol should be the closing paranthesis \")\".\n" );
393  return 1;
394  }
395  for ( i = 0; pStr[i]; i++ )
396  if ( pStr[i] == '(' )
397  Counter++;
398  else if ( pStr[i] == ')' )
399  Counter--;
400  if ( Counter != 0 )
401  {
402  printf( "The number of opening and closing parantheses is not equal.\n" );
403  return 1;
404  }
405  *pnVars = 0;
406  *pnPars = 0;
407  for ( i = 0; pStr[i]; i++ )
408  {
409  if ( pStr[i] >= 'a' && pStr[i] <= 'b' )
410  *pnVars = Abc_MaxInt( *pnVars, pStr[i] - 'a' + 1 );
411  else if ( pStr[i] >= 'p' && pStr[i] <= 's' )
412  *pnPars = Abc_MaxInt( *pnPars, pStr[i] - 'p' + 1 );
413  else if ( pStr[i] == '(' || pStr[i] == ')' )
414  {}
415  else if ( pStr[i] == '&' || pStr[i] == '|' || pStr[i] == '^' )
416  {}
417  else if ( pStr[i] == '?' || pStr[i] == ':' )
418  {}
419  else if ( pStr[i] == '~' )
420  {
421  if ( pStr[i+1] < 'a' || pStr[i+1] > 'z' )
422  {
423  printf( "Expecting alphabetic symbol (instead of \"%c\") after negation (~)\n", pStr[i+1] );
424  return 1;
425  }
426  }
427  else
428  {
429  printf( "Unknown symbol (%c) in the formula (%s)\n", pStr[i], pStr );
430  return 1;
431  }
432  }
433  if ( *pnVars != FFTEST_MAX_VARS )
434  { printf( "The number of input variables (%d) should be 2\n", *pnVars ); return 1; }
435  if ( *pnPars < 1 && *pnPars > FFTEST_MAX_PARS )
436  { printf( "The number of parameters should be between 1 and %d\n", *pnPars ); return 1; }
437  return 0;
438 }
#define FFTEST_MAX_PARS
Definition: bmcFault.c:34
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
#define FFTEST_MAX_VARS
DECLARATIONS ///.
Definition: bmcFault.c:33
static int Counter
int strlen()
void Gia_FormStrTransform ( char *  pStr,
char *  pForm 
)

Definition at line 439 of file bmcFault.c.

440 {
441  int i, k;
442  for ( k = i = 0; pForm[i]; i++ )
443  {
444  if ( pForm[i] == '~' )
445  {
446  i++;
447  assert( pForm[i] >= 'a' && pForm[i] <= 'z' );
448  pStr[k++] = 'A' + pForm[i] - 'a';
449  }
450  else
451  pStr[k++] = pForm[i];
452  }
453  pStr[k] = 0;
454 }
#define assert(ex)
Definition: util_old.h:213
Gia_Man_t* Gia_ManDeriveDup ( Gia_Man_t p,
int  nPisNew 
)

Function*************************************************************

Synopsis [Derive the second AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 826 of file bmcFault.c.

827 {
828  int i;
829  Gia_Man_t * pNew = Gia_ManDup(p);
830  for ( i = 0; i < nPisNew; i++ )
831  Gia_ManAppendCi( pNew );
832  return pNew;
833 }
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:95
void Gia_ManDumpTests ( Vec_Int_t vTests,
int  nIter,
char *  pFileName 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 622 of file bmcFault.c.

623 {
624  FILE * pFile = fopen( pFileName, "wb" );
625  int i, k, v, nVars = Vec_IntSize(vTests) / nIter;
626  assert( Vec_IntSize(vTests) % nIter == 0 );
627  for ( v = i = 0; i < nIter; i++, fprintf(pFile, "\n") )
628  for ( k = 0; k < nVars; k++ )
629  fprintf( pFile, "%d", Vec_IntEntry(vTests, v++) );
630  fclose( pFile );
631 }
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
int Gia_ManDumpUntests ( Gia_Man_t pM,
Cnf_Dat_t pCnf,
sat_solver pSat,
int  nFuncVars,
char *  pFileName,
int  fVerbose 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 728 of file bmcFault.c.

729 {
730  FILE * pFile = fopen( pFileName, "wb" );
731  Vec_Int_t * vLits;
732  Gia_Obj_t * pObj;
733  int nItersMax = 10000;
734  int i, nIters, status, Value, Count = 0;
735  vLits = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
736  for ( nIters = 0; nIters < nItersMax; nIters++ )
737  {
738  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
739  if ( status == l_Undef )
740  printf( "Timeout reached after dumping %d untestable faults.\n", nIters );
741  if ( status == l_Undef )
742  break;
743  if ( status == l_False )
744  break;
745  // collect literals
746  Vec_IntClear( vLits );
747  Gia_ManForEachPi( pM, pObj, i )
748  if ( i >= nFuncVars )
749  Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)])) );
750  // dump the fault
751  Vec_IntForEachEntry( vLits, Value, i )
752  if ( Abc_LitIsCompl(Value) )
753  break;
754  if ( i < Vec_IntSize(vLits) )
755  {
756  if ( fVerbose )
757  {
758  printf( "Untestable fault %4d : ", ++Count );
759  Vec_IntForEachEntry( vLits, Value, i )
760  if ( Abc_LitIsCompl(Value) )
761  printf( "%d ", i );
762  printf( "\n" );
763  }
764  Vec_IntForEachEntry( vLits, Value, i )
765  if ( Abc_LitIsCompl(Value) )
766  fprintf( pFile, "%d ", i );
767  fprintf( pFile, "\n" );
768  }
769  // add this clause
770  if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
771  break;
772  }
773  Vec_IntFree( vLits );
774  fclose( pFile );
775  return nIters;
776 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define l_Undef
Definition: SolverTypes.h:86
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Definition: gia.h:75
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define l_False
Definition: SolverTypes.h:85
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Gia_ManFaultAddOne ( Gia_Man_t pM,
Cnf_Dat_t pCnf,
sat_solver pSat,
Vec_Int_t vLits,
int  nFuncVars 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 675 of file bmcFault.c.

676 {
677  Gia_Man_t * pC;
678  Cnf_Dat_t * pCnf2;
679  Gia_Obj_t * pObj;
680  int i, Lit;
681  // derive the cofactor
682  pC = Gia_ManFaultCofactor( pM, vLits );
683 //Gia_AigerWrite( pC, "fftest_cof.aig", 0, 0 );
684 //printf( "Dumped cofactor circuit into file \"%s\".\n", "fftest_cof.aig" );
685  // derive new CNF
686  pCnf2 = Cnf_DeriveGiaRemapped( pC );
687  Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) );
688  // add timeframe clauses
689  for ( i = 0; i < pCnf2->nClauses; i++ )
690  if ( !sat_solver_addclause( pSat, pCnf2->pClauses[i], pCnf2->pClauses[i+1] ) )
691  {
692  Cnf_DataFree( pCnf2 );
693  Gia_ManStop( pC );
694  return 0;
695  }
696  // add constraint clauses
697  Gia_ManForEachPo( pC, pObj, i )
698  {
699  Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 );
700  if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
701  {
702  Cnf_DataFree( pCnf2 );
703  Gia_ManStop( pC );
704  return 0;
705  }
706  }
707  // add connection clauses
708  Gia_ManForEachPi( pM, pObj, i )
709  if ( i >= nFuncVars )
710  sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 );
711  Cnf_DataFree( pCnf2 );
712  Gia_ManStop( pC );
713  return 1;
714 }
static void Cnf_DataLiftGia(Cnf_Dat_t *p, Gia_Man_t *pGia, int nVarsPlus)
Definition: bmcFault.c:159
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
int nClauses
Definition: cnf.h:61
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
int * pVarNums
Definition: cnf.h:63
Definition: cnf.h:56
Definition: gia.h:75
static int sat_solver_add_buffer(sat_solver *pSat, int iVarA, int iVarB, int fCompl)
Definition: satSolver.h:288
Gia_Man_t * Gia_ManFaultCofactor(Gia_Man_t *p, Vec_Int_t *vValues)
Definition: bmcFault.c:585
static Cnf_Dat_t * Cnf_DeriveGiaRemapped(Gia_Man_t *p)
Definition: bmcFault.c:137
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
int ** pClauses
Definition: cnf.h:62
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
if(last==0)
Definition: sparse_int.h:34
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Definition: gia.h:95
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
int Gia_ManFaultAnalyze ( sat_solver pSat,
Vec_Int_t vPars,
Vec_Int_t vMap,
Vec_Int_t vLits,
int  Iter 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 846 of file bmcFault.c.

847 {
848  int nConfLimit = 100;
849  int status, i, v, iVar, Lit;
850  int nUnsats = 0, nRuns = 0;
851  abctime clk = Abc_Clock();
852  assert( Vec_IntSize(vPars) == Vec_IntSize(vMap) );
853  // check presence of each variable
854  Vec_IntClear( vLits );
855  Vec_IntAppend( vLits, vMap );
856  for ( v = 0; v < Vec_IntSize(vPars); v++ )
857  {
858  if ( !Vec_IntEntry(vLits, v) )
859  continue;
860  assert( Vec_IntEntry(vLits, v) == 1 );
861  nRuns++;
862  Lit = Abc_Var2Lit( Vec_IntEntry(vPars, v), 0 );
863  status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
864  if ( status == l_Undef )
865  continue;
866  if ( status == l_False )
867  {
868  nUnsats++;
869  assert( Vec_IntEntry(vMap, v) == 1 );
870  Vec_IntWriteEntry( vMap, v, 0 );
871  Lit = Abc_LitNot(Lit);
872  //status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
873  //assert( status );
874  continue;
875  }
876  Vec_IntForEachEntry( vPars, iVar, i )
877  if ( Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) )
878  Vec_IntWriteEntry( vLits, i, 0 );
879  assert( Vec_IntEntry(vLits, v) == 0 );
880  }
881  printf( "Iteration %3d has determined %5d (out of %5d) parameters after %6d SAT calls. ", Iter, Vec_IntSize(vMap) - Vec_IntCountPositive(vMap), Vec_IntSize(vPars), nRuns );
882  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
883  return nUnsats;
884 }
static int Vec_IntCountPositive(Vec_Int_t *p)
Definition: vecInt.h:1175
#define l_Undef
Definition: SolverTypes.h:86
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
static abctime Abc_Clock()
Definition: abc_global.h:279
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define l_False
Definition: SolverTypes.h:85
#define assert(ex)
Definition: util_old.h:213
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_Man_t* Gia_ManFaultCofactor ( Gia_Man_t p,
Vec_Int_t vValues 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 585 of file bmcFault.c.

586 {
587  Gia_Man_t * pNew, * pTemp;
588  Gia_Obj_t * pObj;
589  int i;
590  pNew = Gia_ManStart( Gia_ManObjNum(p) );
591  pNew->pName = Abc_UtilStrsav( p->pName );
592  Gia_ManHashAlloc( pNew );
593  Gia_ManConst0(p)->Value = 0;
594  Gia_ManForEachPi( p, pObj, i )
595  {
596  pObj->Value = Gia_ManAppendCi( pNew );
597  if ( i < Vec_IntSize(vValues) )
598  pObj->Value = Vec_IntEntry( vValues, i );
599  }
600  Gia_ManForEachAnd( p, pObj, i )
601  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
602  Gia_ManForEachCo( p, pObj, i )
603  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
604  pNew = Gia_ManCleanup( pTemp = pNew );
605  Gia_ManStop( pTemp );
606  assert( Gia_ManPiNum(pNew) == Gia_ManPiNum(p) );
607  return pNew;
608 
609 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
int Gia_ManFaultPrepare ( Gia_Man_t p,
Gia_Man_t pG,
Bmc_ParFf_t pPars,
int  nFuncVars,
Vec_Int_t vMap,
Vec_Int_t vTests,
Vec_Int_t vLits,
Gia_Man_t **  ppMiter,
Cnf_Dat_t **  ppCnf,
sat_solver **  ppSat,
int  fWarmUp 
)

Function*************************************************************

Synopsis [Generate miter, CNF and solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 897 of file bmcFault.c.

898 {
899  Gia_Man_t * p0 = NULL, * p1 = NULL, * pM;
900  Gia_Obj_t * pObj;
901  Cnf_Dat_t * pCnf;
902  sat_solver * pSat;
903  int i, Iter, status;
904  abctime clkSat = 0;
905 
906  if ( Vec_IntSize(vTests) && (Vec_IntSize(vTests) % nFuncVars != 0) )
907  {
908  printf( "The number of symbols in the input patterns (%d) does not divide evenly on the number of test variables (%d).\n", Vec_IntSize(vTests), nFuncVars );
909  Vec_IntFree( vTests );
910  return 0;
911  }
912 
913  // select algorithm
914  if ( pPars->Algo == 0 )
915  p1 = Gia_ManFormulaUnfold( p, pPars->pFormStr );
916  else if ( pPars->Algo == 1 )
917  {
918  assert( Gia_ManRegNum(p) > 0 );
919  p0 = Gia_ManFaultUnfold( pG, 0 );
920  p1 = Gia_ManFaultUnfold( p, 1 );
921  }
922  else if ( pPars->Algo == 2 )
923  p1 = Gia_ManStuckAtUnfold( p, vMap );
924  else if ( pPars->Algo == 3 )
925  p1 = Gia_ManFlipUnfold( p, vMap );
926  else if ( pPars->Algo == 4 )
927  p1 = Gia_ManFOFUnfold( p, vMap );
928  if ( pPars->Algo != 1 )
929  p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
930 // Gia_AigerWrite( p1, "newfault.aig", 0, 0 );
931 // printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
932 
933  // create miter
934  pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
935  pCnf = Cnf_DeriveGiaRemapped( pM );
936  Gia_ManStop( p0 );
937  Gia_ManStop( p1 );
938 
939  // start the SAT solver
940  pSat = sat_solver_new();
941  sat_solver_setnvars( pSat, pCnf->nVars );
942  sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
943  // add timeframe clauses
944  for ( i = 0; i < pCnf->nClauses; i++ )
945  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
946  assert( 0 );
947 
948  // add one large OR clause
949  Vec_IntClear( vLits );
950  Gia_ManForEachCo( pM, pObj, i )
951  Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
952  sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
953 
954  // add cardinality constraint
955  if ( pPars->fBasic )
956  {
957  Vec_IntClear( vLits );
958  Gia_ManForEachPi( pM, pObj, i )
959  if ( i >= nFuncVars )
960  Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
961  Cnf_AddCardinConstr( pSat, vLits );
962  }
963 
964  // add available test-patterns
965  if ( Vec_IntSize(vTests) > 0 )
966  {
967  int nTests = Vec_IntSize(vTests) / nFuncVars;
968  assert( Vec_IntSize(vTests) % nFuncVars == 0 );
969  if ( pPars->pFileName )
970  printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName );
971  else
972  printf( "Reading %d pre-computed test patterns from previous rounds.\n", Vec_IntSize(vTests) / nFuncVars );
973  for ( Iter = 0; Iter < nTests; Iter++ )
974  {
975  if ( fWarmUp )
976  {
977  abctime clk = Abc_Clock();
978  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
979  clkSat += Abc_Clock() - clk;
980  if ( status == l_Undef )
981  {
982  if ( pPars->fVerbose )
983  printf( "\n" );
984  printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter );
985  return 0;
986  }
987  if ( status == l_False )
988  {
989  if ( pPars->fVerbose )
990  printf( "\n" );
991  printf( "The problem is UNSAT after adding %d tests.\n", Iter );
992  return 0;
993  }
994  }
995  // get pattern
996  Vec_IntClear( vLits );
997  for ( i = 0; i < nFuncVars; i++ )
998  Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
999  if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) )
1000  {
1001  if ( pPars->fVerbose )
1002  printf( "\n" );
1003  printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1004  return 0;
1005  }
1006  if ( pPars->fVerbose )
1007  {
1008  printf( "Iter%6d : ", Iter );
1009  printf( "Var =%10d ", sat_solver_nvars(pSat) );
1010  printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
1011  printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
1012  //Abc_PrintTime( 1, "Time", clkSat );
1013  ABC_PRTr( "Solver time", clkSat );
1014  }
1015  }
1016  }
1017  else if ( pPars->fStartPats )
1018  {
1019  for ( Iter = 0; Iter < 2; Iter++ )
1020  {
1021  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1022  if ( status == l_Undef )
1023  {
1024  if ( pPars->fVerbose )
1025  printf( "\n" );
1026  printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
1027  return 0;
1028  }
1029  if ( status == l_False )
1030  {
1031  if ( pPars->fVerbose )
1032  printf( "\n" );
1033  printf( "The problem is UNSAT after %d iterations.\n", Iter );
1034  return 0;
1035  }
1036  // initialize simple pattern
1037  Vec_IntFill( vLits, nFuncVars, Iter );
1038  Vec_IntAppend( vTests, vLits );
1039  if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) )
1040  {
1041  if ( pPars->fVerbose )
1042  printf( "\n" );
1043  printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1044  return 0;
1045  }
1046  }
1047  }
1048 
1049  printf( "Using miter with: AIG nodes = %6d. CNF variables = %6d. CNF clauses = %8d.\n", Gia_ManAndNum(pM), pCnf->nVars, pCnf->nClauses );
1050 
1051  *ppMiter = pM;
1052  *ppCnf = pCnf;
1053  *ppSat = pSat;
1054  return 1;
1055 }
int Algo
Definition: bmc.h:128
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Gia_Man_t * Gia_ManFormulaUnfold(Gia_Man_t *p, char *pForm)
Definition: bmcFault.c:539
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Gia_Man_t * Gia_ManDeriveDup(Gia_Man_t *p, int nPisNew)
Definition: bmcFault.c:826
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_Man_t * Gia_ManStuckAtUnfold(Gia_Man_t *p, Vec_Int_t *vMap)
Definition: bmcFault.c:232
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
#define l_Undef
Definition: SolverTypes.h:86
int nClauses
Definition: cnf.h:61
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
int nVars
Definition: cnf.h:59
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Gia_Man_t * Gia_ManFOFUnfold(Gia_Man_t *p, Vec_Int_t *vMap)
Definition: bmcFault.c:316
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
int nTimeOut
Definition: bmc.h:131
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Cnf_AddCardinConstr(sat_solver *p, Vec_Int_t *vVars)
Definition: bmcFault.c:76
Definition: cnf.h:56
Definition: gia.h:75
int fVerbose
Definition: bmc.h:136
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static Cnf_Dat_t * Cnf_DeriveGiaRemapped(Gia_Man_t *p)
Definition: bmcFault.c:137
int ** pClauses
Definition: cnf.h:62
#define ABC_PRTr(a, t)
Definition: abc_global.h:221
Gia_Man_t * Gia_ManFaultUnfold(Gia_Man_t *p, int fUseMuxes)
Definition: bmcFault.c:181
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
int fStartPats
Definition: bmc.h:130
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
Gia_Man_t * Gia_ManFlipUnfold(Gia_Man_t *p, Vec_Int_t *vMap)
Definition: bmcFault.c:277
#define l_False
Definition: SolverTypes.h:85
char * pFileName
Definition: bmc.h:126
#define assert(ex)
Definition: util_old.h:213
char * pFormStr
Definition: bmc.h:127
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition: giaDup.c:2128
int Gia_ManFaultAddOne(Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, Vec_Int_t *vLits, int nFuncVars)
Definition: bmcFault.c:675
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Gia_ManFaultTest ( Gia_Man_t p,
Gia_Man_t pG,
Bmc_ParFf_t pPars 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 1068 of file bmcFault.c.

1069 {
1070  int nIterMax = 1000000, nVars, nPars;
1071  int i, Iter, Iter2, status, nFuncVars = -1;
1072  abctime clk, clkSat = 0, clkTotal = Abc_Clock();
1073  Vec_Int_t * vLits, * vMap = NULL, * vTests, * vPars = NULL;
1074  Gia_Man_t * pM;
1075  Gia_Obj_t * pObj;
1076  Cnf_Dat_t * pCnf;
1077  sat_solver * pSat;
1078 
1079  if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) )
1080  return;
1081 
1082  // select algorithm
1083  if ( pPars->Algo == 0 )
1084  printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr );
1085  else if ( pPars->Algo == 1 )
1086  printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" );
1087  else if ( pPars->Algo == 2 )
1088  printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" );
1089  else if ( pPars->Algo == 3 )
1090  printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" );
1091  else if ( pPars->Algo == 4 )
1092  printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" );
1093  else
1094  {
1095  printf( "Unrecognized algorithm (%d).\n", pPars->Algo );
1096  return;
1097  }
1098 
1099  // select algorithm
1100  if ( pPars->Algo == 0 )
1101  nFuncVars = Gia_ManCiNum(p);
1102  else if ( pPars->Algo == 1 )
1103  nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
1104  else if ( pPars->Algo == 2 )
1105  nFuncVars = Gia_ManCiNum(p);
1106  else if ( pPars->Algo == 3 )
1107  nFuncVars = Gia_ManCiNum(p);
1108  else if ( pPars->Algo == 4 )
1109  nFuncVars = Gia_ManCiNum(p);
1110 
1111  // collect test patterns from file
1112  if ( pPars->pFileName )
1113  vTests = Gia_ManGetTestPatterns( pPars->pFileName );
1114  else
1115  vTests = Vec_IntAlloc( 10000 );
1116  if ( vTests == NULL )
1117  return;
1118 
1119  // select algorithm
1120  vMap = Vec_IntAlloc( 0 );
1121  if ( pPars->Algo == 2 )
1122  Vec_IntFill( vMap, 2 * Gia_ManAndNum(p), 1 );
1123  else if ( pPars->Algo == 3 )
1124  Vec_IntFill( vMap, Gia_ManAndNum(p), 1 );
1125  else if ( pPars->Algo == 4 )
1126  Vec_IntFill( vMap, 4 * Gia_ManAndNum(p), 1 );
1127 
1128  // prepare SAT solver
1129  vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
1130  if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 1) )
1131  return;
1132 
1133  // iterate through the test vectors
1134  for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
1135  {
1136  // collect parameter variables
1137  if ( pPars->nIterCheck && vPars == NULL )
1138  {
1139  vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
1140  Gia_ManForEachPi( pM, pObj, i )
1141  if ( i >= nFuncVars )
1142  Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
1143  assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars );
1144  }
1145  // derive unit parameter variables
1146  if ( Iter && pPars->nIterCheck && (Iter % pPars->nIterCheck) == 0 )
1147  {
1148  Gia_ManFaultAnalyze( pSat, vPars, vMap, vLits, Iter );
1149  // cleanup
1150  Gia_ManStop( pM );
1151  Cnf_DataFree( pCnf );
1152  sat_solver_delete( pSat );
1153  // recompute
1154  if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 0) )
1155  {
1156  printf( "This should never happen.\n" );
1157  return;
1158  }
1159  Vec_IntFreeP( &vPars );
1160  }
1161  // solve
1162  clk = Abc_Clock();
1163  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1164  clkSat += Abc_Clock() - clk;
1165  if ( pPars->fVerbose )
1166  {
1167  printf( "Iter%6d : ", Iter );
1168  printf( "Var =%10d ", sat_solver_nvars(pSat) );
1169  printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
1170  printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
1171  //Abc_PrintTime( 1, "Time", clkSat );
1172  ABC_PRTr( "Solver time", clkSat );
1173  }
1174  if ( status == l_Undef )
1175  {
1176  if ( pPars->fVerbose )
1177  printf( "\n" );
1178  printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
1179  goto finish;
1180  }
1181  if ( status == l_False )
1182  {
1183  if ( pPars->fVerbose )
1184  printf( "\n" );
1185  printf( "The problem is UNSAT after %d iterations. ", Iter );
1186  break;
1187  }
1188  assert( status == l_True );
1189  // collect SAT assignment
1190  Vec_IntClear( vLits );
1191  Gia_ManForEachPi( pM, pObj, i )
1192  if ( i < nFuncVars )
1193  Vec_IntPush( vLits, sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) );
1194  Vec_IntAppend( vTests, vLits );
1195  // add constraint
1196  if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) )
1197  {
1198  if ( pPars->fVerbose )
1199  printf( "\n" );
1200  printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1201  break;
1202  }
1203  }
1204 finish:
1205  // print results
1206 // if ( status == l_False )
1207 // Gia_ManPrintResults( p, pSat, Iter, Abc_Clock() - clkTotal );
1208  // cleanup
1209  Abc_PrintTime( 1, "Testing runtime", Abc_Clock() - clkTotal );
1210  // dump the test suite
1211  if ( pPars->fDump )
1212  {
1213  char * pFileName = "tests.txt";
1214  Gia_ManDumpTests( vTests, Iter, pFileName );
1215  printf( "Dumping %d computed test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
1216  }
1217 
1218  // compute untestable faults
1219  if ( Iter && (p != pG || pPars->fDumpUntest) )
1220  {
1221  abctime clkTotal = Abc_Clock();
1222  // restart the SAT solver
1223  sat_solver_delete( pSat );
1224  pSat = sat_solver_new();
1225  sat_solver_setnvars( pSat, pCnf->nVars );
1226  sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
1227  // add timeframe clauses
1228  for ( i = 0; i < pCnf->nClauses; i++ )
1229  if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1230  assert( 0 );
1231  // add constraint to rule out no fault
1232 // if ( p == pG )
1233  {
1234  Vec_IntClear( vLits );
1235  Gia_ManForEachPi( pM, pObj, i )
1236  if ( i >= nFuncVars )
1237  Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
1238  sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
1239  }
1240  // add cardinality constraint
1241  if ( pPars->fBasic )
1242  {
1243  Vec_IntClear( vLits );
1244  Gia_ManForEachPi( pM, pObj, i )
1245  if ( i >= nFuncVars )
1246  Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
1247  Cnf_AddCardinConstr( pSat, vLits );
1248  }
1249  // add output clauses
1250  Gia_ManForEachCo( pM, pObj, i )
1251  {
1252  int Lit = Abc_Var2Lit( pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1 );
1253  sat_solver_addclause( pSat, &Lit, &Lit + 1 );
1254  }
1255  // simplify the SAT solver
1256  status = sat_solver_simplify( pSat );
1257  assert( status );
1258 
1259  // add test patterns
1260  assert( Vec_IntSize(vTests) == Iter * nFuncVars );
1261  for ( Iter2 = 0; ; Iter2++ )
1262  {
1263  abctime clk = Abc_Clock();
1264  status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1265  clkSat += Abc_Clock() - clk;
1266  if ( pPars->fVerbose )
1267  {
1268  printf( "Iter%6d : ", Iter2 );
1269  printf( "Var =%10d ", sat_solver_nvars(pSat) );
1270  printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
1271  printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
1272  //Abc_PrintTime( 1, "Time", clkSat );
1273  ABC_PRTr( "Solver time", clkSat );
1274  }
1275  if ( status == l_Undef )
1276  {
1277  if ( pPars->fVerbose )
1278  printf( "\n" );
1279  printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter2 );
1280  goto finish;
1281  }
1282  if ( Iter2 == Iter )
1283  break;
1284  assert( status == l_True );
1285  // get pattern
1286  Vec_IntClear( vLits );
1287  for ( i = 0; i < nFuncVars; i++ )
1288  Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter2*nFuncVars + i) );
1289  if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars ) )
1290  {
1291  printf( "The problem is UNSAT after adding %d tests.\n", Iter2 );
1292  goto finish;
1293  }
1294  }
1295  assert( Iter2 == Iter );
1296  if ( pPars->fVerbose )
1297  printf( "\n" );
1298  if ( p == pG )
1299  {
1300  if ( status == l_True )
1301  printf( "There are untestable faults. " );
1302  else if ( status == l_False )
1303  printf( "There is no untestable faults. " );
1304  else assert( 0 );
1305  Abc_PrintTime( 1, "Fault computation runtime", Abc_Clock() - clkTotal );
1306  }
1307  else
1308  {
1309  if ( status == l_True )
1310  printf( "The circuit is rectifiable. " );
1311  else if ( status == l_False )
1312  printf( "The circuit is not rectifiable (or equivalent to the golden one). " );
1313  else assert( 0 );
1314  Abc_PrintTime( 1, "Rectification runtime", Abc_Clock() - clkTotal );
1315  }
1316  // dump untestable faults
1317  if ( pPars->fDumpUntest && status == l_True )
1318  {
1319  abctime clk = Abc_Clock();
1320  char * pFileName = "untest.txt";
1321  int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose );
1322  if ( p == pG )
1323  printf( "Dumped %d untestable multiple faults into file \"%s\". ", nUntests, pFileName );
1324  else
1325  printf( "Dumped %d ways of rectifying the circuit into file \"%s\". ", nUntests, pFileName );
1326  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1327  }
1328  }
1329  sat_solver_delete( pSat );
1330  Cnf_DataFree( pCnf );
1331  Gia_ManStop( pM );
1332  Vec_IntFree( vTests );
1333  Vec_IntFree( vMap );
1334  Vec_IntFree( vLits );
1335  Vec_IntFreeP( &vPars );
1336 }
int fBasic
Definition: bmc.h:133
int Algo
Definition: bmc.h:128
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
void Gia_ManDumpTests(Vec_Int_t *vTests, int nIter, char *pFileName)
Definition: bmcFault.c:622
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
#define l_Undef
Definition: SolverTypes.h:86
int Gia_ManFaultAnalyze(sat_solver *pSat, Vec_Int_t *vPars, Vec_Int_t *vMap, Vec_Int_t *vLits, int Iter)
Definition: bmcFault.c:846
int nIterCheck
Definition: bmc.h:132
int nClauses
Definition: cnf.h:61
int sat_solver_solve(sat_solver *s, lit *begin, lit *end, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, ABC_INT64_T nConfLimitGlobal, ABC_INT64_T nInsLimitGlobal)
Definition: satSolver.c:1700
int nVars
Definition: cnf.h:59
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
int * pVarNums
Definition: cnf.h:63
#define l_True
Definition: SolverTypes.h:84
int fDumpUntest
Definition: bmc.h:135
int nTimeOut
Definition: bmc.h:131
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Cnf_AddCardinConstr(sat_solver *p, Vec_Int_t *vVars)
Definition: bmcFault.c:76
Definition: cnf.h:56
Definition: gia.h:75
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
int fVerbose
Definition: bmc.h:136
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
int ** pClauses
Definition: cnf.h:62
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
int Gia_ManDumpUntests(Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, int nFuncVars, char *pFileName, int fVerbose)
Definition: bmcFault.c:728
#define ABC_PRTr(a, t)
Definition: abc_global.h:221
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
int fStartPats
Definition: bmc.h:130
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
Vec_Int_t * Gia_ManGetTestPatterns(char *pFileName)
Definition: bmcFault.c:789
int Gia_ManFaultPrepare(Gia_Man_t *p, Gia_Man_t *pG, Bmc_ParFf_t *pPars, int nFuncVars, Vec_Int_t *vMap, Vec_Int_t *vTests, Vec_Int_t *vLits, Gia_Man_t **ppMiter, Cnf_Dat_t **ppCnf, sat_solver **ppSat, int fWarmUp)
Definition: bmcFault.c:897
#define l_False
Definition: SolverTypes.h:85
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
int Gia_FormStrCount(char *pStr, int *pnVars, int *pnPars)
Definition: bmcFault.c:382
char * pFileName
Definition: bmc.h:126
#define assert(ex)
Definition: util_old.h:213
char * pFormStr
Definition: bmc.h:127
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
ABC_INT64_T abctime
Definition: abc_global.h:278
int Gia_ManFaultAddOne(Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, Vec_Int_t *vLits, int nFuncVars)
Definition: bmcFault.c:675
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
int fDump
Definition: bmc.h:134
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_Man_t* Gia_ManFaultUnfold ( Gia_Man_t p,
int  fUseMuxes 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 181 of file bmcFault.c.

182 {
183  Gia_Man_t * pNew, * pTemp;
184  Gia_Obj_t * pObj;
185  int i, iCtrl, iThis;
186  pNew = Gia_ManStart( (2 + 3 * fUseMuxes) * Gia_ManObjNum(p) );
187  pNew->pName = Abc_UtilStrsav( p->pName );
188  Gia_ManHashAlloc( pNew );
189  Gia_ManConst0(p)->Value = 0;
190  // add first timeframe
191  Gia_ManForEachRo( p, pObj, i )
192  pObj->Value = Gia_ManAppendCi( pNew );
193  Gia_ManForEachPi( p, pObj, i )
194  pObj->Value = Gia_ManAppendCi( pNew );
195  Gia_ManForEachAnd( p, pObj, i )
196  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
197  Gia_ManForEachCo( p, pObj, i )
198  pObj->Value = Gia_ObjFanin0Copy(pObj);
199  // add second timeframe
200  Gia_ManForEachRo( p, pObj, i )
201  pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
202  Gia_ManForEachPi( p, pObj, i )
203  pObj->Value = Gia_ManAppendCi( pNew );
204  Gia_ManForEachAnd( p, pObj, i )
205  {
206  iCtrl = Gia_ManAppendCi(pNew);
207  iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
208  if ( fUseMuxes )
209  pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis );
210  else
211  pObj->Value = iThis;
212  }
213  Gia_ManForEachCo( p, pObj, i )
214  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
215  pNew = Gia_ManCleanup( pTemp = pNew );
216  Gia_ManStop( pTemp );
217  assert( Gia_ManPiNum(pNew) == Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p) + Gia_ManAndNum(p) );
218  return pNew;
219 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_Man_t* Gia_ManFlipUnfold ( Gia_Man_t p,
Vec_Int_t vMap 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file bmcFault.c.

278 {
279  Gia_Man_t * pNew, * pTemp;
280  Gia_Obj_t * pObj;
281  int i, iFuncVars = 0;
282  pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) );
283  pNew->pName = Abc_UtilStrsav( p->pName );
284  Gia_ManHashAlloc( pNew );
285  Gia_ManConst0(p)->Value = 0;
286  Gia_ManForEachCi( p, pObj, i )
287  pObj->Value = Gia_ManAppendCi( pNew );
288  Gia_ManForEachAnd( p, pObj, i )
289  {
290  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
291  if ( Vec_IntEntry(vMap, iFuncVars++) )
292  pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value );
293  else
294  Gia_ManAppendCi(pNew);
295  }
296  assert( iFuncVars == Vec_IntSize(vMap) );
297  Gia_ManForEachCo( p, pObj, i )
298  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
299  pNew = Gia_ManCleanup( pTemp = pNew );
300  Gia_ManStop( pTemp );
301  assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + Gia_ManAndNum(p) );
302  return pNew;
303 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_Man_t* Gia_ManFOFUnfold ( Gia_Man_t p,
Vec_Int_t vMap 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file bmcFault.c.

317 {
318  Gia_Man_t * pNew, * pTemp;
319  Gia_Obj_t * pObj;
320  int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0;
321  pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
322  pNew->pName = Abc_UtilStrsav( p->pName );
323  Gia_ManHashAlloc( pNew );
324  Gia_ManConst0(p)->Value = 0;
325  Gia_ManForEachCi( p, pObj, i )
326  pObj->Value = Gia_ManAppendCi( pNew );
327  Gia_ManForEachAnd( p, pObj, i )
328  {
329  if ( Vec_IntEntry(vMap, iFuncVars++) )
330  iCtrl0 = Gia_ManAppendCi(pNew);
331  else
332  iCtrl0 = 0, Gia_ManAppendCi(pNew);
333 
334  if ( Vec_IntEntry(vMap, iFuncVars++) )
335  iCtrl1 = Gia_ManAppendCi(pNew);
336  else
337  iCtrl1 = 0, Gia_ManAppendCi(pNew);
338 
339  if ( Vec_IntEntry(vMap, iFuncVars++) )
340  iCtrl2 = Gia_ManAppendCi(pNew);
341  else
342  iCtrl2 = 0, Gia_ManAppendCi(pNew);
343 
344  if ( Vec_IntEntry(vMap, iFuncVars++) )
345  iCtrl3 = Gia_ManAppendCi(pNew);
346  else
347  iCtrl3 = 0, Gia_ManAppendCi(pNew);
348 
349  if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
350  iCtrl0 = Abc_LitNot(iCtrl0);
351  else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
352  iCtrl1 = Abc_LitNot(iCtrl1);
353  else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
354  iCtrl2 = Abc_LitNot(iCtrl2);
355  else //if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
356  iCtrl3 = Abc_LitNot(iCtrl3);
357 
358  iMuxA = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl1, iCtrl0 );
359  iMuxB = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl3, iCtrl2 );
360  pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin1(pObj)->Value, iMuxB, iMuxA );
361  }
362  assert( iFuncVars == Vec_IntSize(vMap) );
363  Gia_ManForEachCo( p, pObj, i )
364  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
365  pNew = Gia_ManCleanup( pTemp = pNew );
366  Gia_ManStop( pTemp );
367  assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 4 * Gia_ManAndNum(p) );
368  return pNew;
369 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
char * pName
Definition: gia.h:97
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
char* Gia_ManFormulaEndToken ( char *  pForm)

Function*************************************************************

Synopsis [Implements fault model formula using functional/parameter vars.]

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file bmcFault.c.

469 {
470  int Counter = 0;
471  char * pThis;
472  for ( pThis = pForm; *pThis; pThis++ )
473  {
474  assert( *pThis != '~' );
475  if ( *pThis == '(' )
476  Counter++;
477  else if ( *pThis == ')' )
478  Counter--;
479  if ( Counter == 0 )
480  return pThis + 1;
481  }
482  assert( 0 );
483  return NULL;
484 }
static int Counter
#define assert(ex)
Definition: util_old.h:213
Gia_Man_t* Gia_ManFormulaUnfold ( Gia_Man_t p,
char *  pForm 
)

Definition at line 539 of file bmcFault.c.

540 {
541  char pStr[100];
542  Gia_Man_t * pNew, * pTemp;
543  Gia_Obj_t * pObj;
544  int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS];
545  int nVars, nPars;
546  assert( strlen(pForm) < 100 );
547  Gia_FormStrCount( pForm, &nVars, &nPars );
548  assert( nVars == 2 );
549  Gia_FormStrTransform( pStr, pForm );
550  pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
551  pNew->pName = Abc_UtilStrsav( p->pName );
552  Gia_ManHashAlloc( pNew );
553  Gia_ManConst0(p)->Value = 0;
554  Gia_ManForEachCi( p, pObj, i )
555  pObj->Value = Gia_ManAppendCi( pNew );
556  Gia_ManForEachAnd( p, pObj, i )
557  {
558  for ( k = 0; k < nPars; k++ )
559  iCtrl[k] = Gia_ManAppendCi(pNew);
560  iFans[0] = Gia_ObjFanin0Copy(pObj);
561  iFans[1] = Gia_ObjFanin1Copy(pObj);
562  pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars );
563  }
564  Gia_ManForEachCo( p, pObj, i )
565  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
566  pNew = Gia_ManCleanup( pTemp = pNew );
567  Gia_ManStop( pTemp );
568  assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * Gia_ManAndNum(p) );
569 // if ( fUseFaults )
570 // Gia_AigerWrite( pNew, "newfault.aig", 0, 0 );
571  return pNew;
572 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
int Gia_ManRealizeFormula(Gia_Man_t *p, int *pVars, int *pPars, char *pStr, int nPars)
Definition: bmcFault.c:535
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
#define FFTEST_MAX_PARS
Definition: bmcFault.c:34
Definition: gia.h:75
#define FFTEST_MAX_VARS
DECLARATIONS ///.
Definition: bmcFault.c:33
void Gia_FormStrTransform(char *pStr, char *pForm)
Definition: bmcFault.c:439
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
int Gia_FormStrCount(char *pStr, int *pnVars, int *pnPars)
Definition: bmcFault.c:382
#define assert(ex)
Definition: util_old.h:213
int strlen()
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Vec_Int_t* Gia_ManGetTestPatterns ( char *  pFileName)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 789 of file bmcFault.c.

790 {
791  FILE * pFile = fopen( pFileName, "rb" );
792  Vec_Int_t * vTests; int c;
793  if ( pFile == NULL )
794  {
795  printf( "Cannot open input file \"%s\".\n", pFileName );
796  return NULL;
797  }
798  vTests = Vec_IntAlloc( 10000 );
799  while ( (c = fgetc(pFile)) != EOF )
800  {
801  if ( c == ' ' || c == '\t' || c == '\r' || c == '\n' )
802  continue;
803  if ( c != '0' && c != '1' )
804  {
805  printf( "Wring symbol (%c) in the input file.\n", c );
806  Vec_IntFreeP( &vTests );
807  break;
808  }
809  Vec_IntPush( vTests, c - '0' );
810  }
811  fclose( pFile );
812  return vTests;
813 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
void Gia_ManPrintResults ( Gia_Man_t p,
sat_solver pSat,
int  nIter,
abctime  clk 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 644 of file bmcFault.c.

645 {
646  FILE * pTable = fopen( "fault_stats.txt", "a+" );
647 
648  fprintf( pTable, "%s ", Gia_ManName(p) );
649  fprintf( pTable, "%d ", Gia_ManPiNum(p) );
650  fprintf( pTable, "%d ", Gia_ManPoNum(p) );
651  fprintf( pTable, "%d ", Gia_ManRegNum(p) );
652  fprintf( pTable, "%d ", Gia_ManAndNum(p) );
653 
654  fprintf( pTable, "%d ", sat_solver_nvars(pSat) );
655  fprintf( pTable, "%d ", sat_solver_nclauses(pSat) );
656  fprintf( pTable, "%d ", sat_solver_nconflicts(pSat) );
657 
658  fprintf( pTable, "%d ", nIter );
659  fprintf( pTable, "%.2f", 1.0*clk/CLOCKS_PER_SEC );
660  fprintf( pTable, "\n" );
661  fclose( pTable );
662 }
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static char * Gia_ManName(Gia_Man_t *p)
Definition: gia.h:382
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Gia_ManRealizeFormula ( Gia_Man_t p,
int *  pVars,
int *  pPars,
char *  pStr,
int  nPars 
)

Definition at line 535 of file bmcFault.c.

536 {
537  return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars );
538 }
int Gia_ManRealizeFormula_rec(Gia_Man_t *p, int *pVars, int *pPars, char *pBeg, char *pEnd, int nPars)
Definition: bmcFault.c:485
int strlen()
int Gia_ManRealizeFormula_rec ( Gia_Man_t p,
int *  pVars,
int *  pPars,
char *  pBeg,
char *  pEnd,
int  nPars 
)

Definition at line 485 of file bmcFault.c.

486 {
487  int iFans[3], Oper = -1;
488  char * pEndNew;
489  if ( pBeg + 1 == pEnd )
490  {
491  if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
492  return pVars[pBeg[0] - 'a'];
493  if ( pBeg[0] >= 'A' && pBeg[0] <= 'B' )
494  return Abc_LitNot( pVars[pBeg[0] - 'A'] );
495  if ( pBeg[0] >= 'p' && pBeg[0] <= 'w' ) // pqrstuvw
496  return pPars[pBeg[0] - 'p'];
497  if ( pBeg[0] >= 'P' && pBeg[0] <= 'W' )
498  return Abc_LitNot( pPars[pBeg[0] - 'P'] );
499  assert( 0 );
500  return -1;
501  }
502  if ( pBeg[0] == '(' )
503  {
504  pEndNew = Gia_ManFormulaEndToken( pBeg );
505  if ( pEndNew == pEnd )
506  {
507  assert( pBeg[0] == '(' );
508  assert( pBeg[pEnd-pBeg-1] == ')' );
509  return Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd - 1, nPars );
510  }
511  }
512  // get first part
513  pEndNew = Gia_ManFormulaEndToken( pBeg );
514  iFans[0] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
515  Oper = pEndNew[0];
516  // get second part
517  pBeg = pEndNew + 1;
518  pEndNew = Gia_ManFormulaEndToken( pBeg );
519  iFans[1] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
520  // derive the formula
521  if ( Oper == '&' )
522  return Gia_ManHashAnd( p, iFans[0], iFans[1] );
523  if ( Oper == '|' )
524  return Gia_ManHashOr( p, iFans[0], iFans[1] );
525  if ( Oper == '^' )
526  return Gia_ManHashXor( p, iFans[0], iFans[1] );
527  // get third part
528  assert( Oper == '?' );
529  assert( pEndNew[0] == ':' );
530  pBeg = pEndNew + 1;
531  pEndNew = Gia_ManFormulaEndToken( pBeg );
532  iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
533  return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] );
534 }
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
char * Gia_ManFormulaEndToken(char *pForm)
Definition: bmcFault.c:468
int Gia_ManRealizeFormula_rec(Gia_Man_t *p, int *pVars, int *pPars, char *pBeg, char *pEnd, int nPars)
Definition: bmcFault.c:485
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
#define assert(ex)
Definition: util_old.h:213
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_Man_t* Gia_ManStuckAtUnfold ( Gia_Man_t p,
Vec_Int_t vMap 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 232 of file bmcFault.c.

233 {
234  Gia_Man_t * pNew, * pTemp;
235  Gia_Obj_t * pObj;
236  int i, iFuncVars = 0;
237  pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) );
238  pNew->pName = Abc_UtilStrsav( p->pName );
239  Gia_ManHashAlloc( pNew );
240  Gia_ManConst0(p)->Value = 0;
241  Gia_ManForEachCi( p, pObj, i )
242  pObj->Value = Gia_ManAppendCi( pNew );
243  Gia_ManForEachAnd( p, pObj, i )
244  {
245  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
246 
247  if ( Vec_IntEntry(vMap, iFuncVars++) )
248  pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value );
249  else
250  Gia_ManAppendCi(pNew);
251 
252  if ( Vec_IntEntry(vMap, iFuncVars++) )
253  pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value );
254  else
255  Gia_ManAppendCi(pNew);
256  }
257  assert( iFuncVars == Vec_IntSize(vMap) );
258  Gia_ManForEachCo( p, pObj, i )
259  pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
260  pNew = Gia_ManCleanup( pTemp = pNew );
261  Gia_ManStop( pTemp );
262  assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 2 * Gia_ManAndNum(p) );
263  return pNew;
264 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Definition: gia.h:75
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
char * pName
Definition: gia.h:97
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ParFfSetDefault ( Bmc_ParFf_t p)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [This procedure sets default parameters.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file bmcFault.c.

52 {
53  memset( p, 0, sizeof(Bmc_ParFf_t) );
54  p->pFileName = NULL;
55  p->Algo = 0;
56  p->fStartPats = 0;
57  p->nTimeOut = 0;
58  p->nIterCheck = 0;
59  p->fBasic = 0;
60  p->fDump = 0;
61  p->fDumpUntest = 0;
62  p->fVerbose = 0;
63 }
int fBasic
Definition: bmc.h:133
char * memset()
int Algo
Definition: bmc.h:128
int nIterCheck
Definition: bmc.h:132
int fDumpUntest
Definition: bmc.h:135
int nTimeOut
Definition: bmc.h:131
int fVerbose
Definition: bmc.h:136
int fStartPats
Definition: bmc.h:130
char * pFileName
Definition: bmc.h:126
int fDump
Definition: bmc.h:134