abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcFault.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcFault.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Checking for functional faults.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcFault.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "aig/gia/giaAig.h"
25 
26 ABC_NAMESPACE_IMPL_START
27 
28 
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32 
33 #define FFTEST_MAX_VARS 2
34 #define FFTEST_MAX_PARS 8
35 
36 ////////////////////////////////////////////////////////////////////////
37 /// FUNCTION DEFINITIONS ///
38 ////////////////////////////////////////////////////////////////////////
39 
40 /**Function*************************************************************
41 
42  Synopsis [This procedure sets default parameters.]
43 
44  Description []
45 
46  SideEffects []
47 
48  SeeAlso []
49 
50 ***********************************************************************/
51 void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
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 }
64 
65 /**Function*************************************************************
66 
67  Synopsis [Add constraint that no more than 1 variable is 1.]
68 
69  Description []
70 
71  SideEffects []
72 
73  SeeAlso []
74 
75 ***********************************************************************/
76 static inline int Cnf_AddCardinConstr( sat_solver * p, Vec_Int_t * vVars )
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 }
99 void Cnf_AddCardinConstrTest()
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 }
125 
126 /**Function*************************************************************
127 
128  Synopsis []
129 
130  Description []
131 
132  SideEffects []
133 
134  SeeAlso []
135 
136 ***********************************************************************/
137 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
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 }
147 
148 /**Function*************************************************************
149 
150  Synopsis []
151 
152  Description []
153 
154  SideEffects []
155 
156  SeeAlso []
157 
158 ***********************************************************************/
159 static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus )
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 }
169 
170 /**Function*************************************************************
171 
172  Synopsis []
173 
174  Description []
175 
176  SideEffects []
177 
178  SeeAlso []
179 
180 ***********************************************************************/
181 Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes )
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 }
220 
221 /**Function*************************************************************
222 
223  Synopsis []
224 
225  Description []
226 
227  SideEffects []
228 
229  SeeAlso []
230 
231 ***********************************************************************/
232 Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
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 }
265 
266 /**Function*************************************************************
267 
268  Synopsis []
269 
270  Description []
271 
272  SideEffects []
273 
274  SeeAlso []
275 
276 ***********************************************************************/
277 Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
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 }
304 
305 /**Function*************************************************************
306 
307  Synopsis []
308 
309  Description []
310 
311  SideEffects []
312 
313  SeeAlso []
314 
315 ***********************************************************************/
316 Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
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 }
370 
371 /**Function*************************************************************
372 
373  Synopsis [This procedure sets default parameters.]
374 
375  Description []
376 
377  SideEffects []
378 
379  SeeAlso []
380 
381 ***********************************************************************/
382 int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars )
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 }
439 void Gia_FormStrTransform( char * pStr, char * pForm )
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 }
455 
456 
457 /**Function*************************************************************
458 
459  Synopsis [Implements fault model formula using functional/parameter vars.]
460 
461  Description []
462 
463  SideEffects []
464 
465  SeeAlso []
466 
467 ***********************************************************************/
468 char * Gia_ManFormulaEndToken( char * pForm )
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 }
485 int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nPars )
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 }
535 int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr, int nPars )
536 {
537  return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars );
538 }
539 Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm )
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 }
573 
574 /**Function*************************************************************
575 
576  Synopsis []
577 
578  Description []
579 
580  SideEffects []
581 
582  SeeAlso []
583 
584 ***********************************************************************/
585 Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
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 }
610 
611 /**Function*************************************************************
612 
613  Synopsis []
614 
615  Description []
616 
617  SideEffects []
618 
619  SeeAlso []
620 
621 ***********************************************************************/
622 void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter, char * pFileName )
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 }
632 
633 /**Function*************************************************************
634 
635  Synopsis []
636 
637  Description []
638 
639  SideEffects []
640 
641  SeeAlso []
642 
643 ***********************************************************************/
644 void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime clk )
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 }
663 
664 /**Function*************************************************************
665 
666  Synopsis []
667 
668  Description []
669 
670  SideEffects []
671 
672  SeeAlso []
673 
674 ***********************************************************************/
675 int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars )
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 }
715 
716 
717 /**Function*************************************************************
718 
719  Synopsis []
720 
721  Description []
722 
723  SideEffects []
724 
725  SeeAlso []
726 
727 ***********************************************************************/
728 int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int nFuncVars, char * pFileName, int fVerbose )
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 }
777 
778 /**Function*************************************************************
779 
780  Synopsis []
781 
782  Description []
783 
784  SideEffects []
785 
786  SeeAlso []
787 
788 ***********************************************************************/
789 Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
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 }
814 
815 /**Function*************************************************************
816 
817  Synopsis [Derive the second AIG.]
818 
819  Description []
820 
821  SideEffects []
822 
823  SeeAlso []
824 
825 ***********************************************************************/
826 Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew )
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 }
834 
835 /**Function*************************************************************
836 
837  Synopsis []
838 
839  Description []
840 
841  SideEffects []
842 
843  SeeAlso []
844 
845 ***********************************************************************/
846 int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vMap, Vec_Int_t * vLits, int Iter )
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 }
885 
886 /**Function*************************************************************
887 
888  Synopsis [Generate miter, CNF and solver.]
889 
890  Description []
891 
892  SideEffects []
893 
894  SeeAlso []
895 
896 ***********************************************************************/
897 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 )
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 }
1056 
1057 /**Function*************************************************************
1058 
1059  Synopsis []
1060 
1061  Description []
1062 
1063  SideEffects []
1064 
1065  SeeAlso []
1066 
1067 ***********************************************************************/
1068 void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
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 }
1337 
1338 
1339 
1340 ////////////////////////////////////////////////////////////////////////
1341 /// END OF FILE ///
1342 ////////////////////////////////////////////////////////////////////////
1343 
1344 
1345 ABC_NAMESPACE_IMPL_END
1346 
Bmc_ParFf_t_::fBasic
int fBasic
Definition: bmc.h:133
memset
char * memset()
Vec_IntCountPositive
static int Vec_IntCountPositive(Vec_Int_t *p)
Definition: vecInt.h:1175
Bmc_ParFf_t_::Algo
int Algo
Definition: bmc.h:128
sat_solver_set_runtime_limit
static abctime sat_solver_set_runtime_limit(sat_solver *s, abctime Limit)
Definition: satSolver.h:233
Gia_ManFormulaUnfold
Gia_Man_t * Gia_ManFormulaUnfold(Gia_Man_t *p, char *pForm)
Definition: bmcFault.c:539
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Cnf_DataLiftGia
static void Cnf_DataLiftGia(Cnf_Dat_t *p, Gia_Man_t *pGia, int nVarsPlus)
Definition: bmcFault.c:159
Gia_ManDup
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
Gia_ManDeriveDup
Gia_Man_t * Gia_ManDeriveDup(Gia_Man_t *p, int nPisNew)
Definition: bmcFault.c:826
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManDumpTests
void Gia_ManDumpTests(Vec_Int_t *vTests, int nIter, char *pFileName)
Definition: bmcFault.c:622
Gia_ManStuckAtUnfold
Gia_Man_t * Gia_ManStuckAtUnfold(Gia_Man_t *p, Vec_Int_t *vMap)
Definition: bmcFault.c:232
Gia_ManPoNum
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Cnf_Derive
Cnf_Dat_t * Cnf_Derive(Aig_Man_t *pAig, int nOutputs)
Definition: cnfCore.c:165
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
sat_solver_addclause
int sat_solver_addclause(sat_solver *s, lit *begin, lit *end)
Definition: satSolver.c:1492
Gia_ManHashXor
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
l_Undef
#define l_Undef
Definition: SolverTypes.h:86
Gia_ManFaultAnalyze
int Gia_ManFaultAnalyze(sat_solver *pSat, Vec_Int_t *vPars, Vec_Int_t *vMap, Vec_Int_t *vLits, int Iter)
Definition: bmcFault.c:846
Gia_ManName
static char * Gia_ManName(Gia_Man_t *p)
Definition: gia.h:382
Bmc_ParFf_t_::nIterCheck
int nIterCheck
Definition: bmc.h:132
Cnf_Dat_t_::nClauses
int nClauses
Definition: cnf.h:61
Cnf_AddCardinConstrTest
void Cnf_AddCardinConstrTest()
Definition: bmcFault.c:99
Bmc_ParFf_t_
Definition: bmc.h:124
Gia_ParFfSetDefault
void Gia_ParFfSetDefault(Bmc_ParFf_t *p)
FUNCTION DEFINITIONS ///.
Definition: bmcFault.c:51
sat_solver_solve
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
Gia_ManRealizeFormula
int Gia_ManRealizeFormula(Gia_Man_t *p, int *pVars, int *pPars, char *pStr, int nPars)
Definition: bmcFault.c:535
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Cnf_Dat_t_::nVars
int nVars
Definition: cnf.h:59
sat_solver_delete
void sat_solver_delete(sat_solver *s)
Definition: satSolver.c:1141
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Gia_ManFOFUnfold
Gia_Man_t * Gia_ManFOFUnfold(Gia_Man_t *p, Vec_Int_t *vMap)
Definition: bmcFault.c:316
sat_solver_nconflicts
int sat_solver_nconflicts(sat_solver *s)
Definition: satSolver.c:1908
Cnf_Dat_t_::pVarNums
int * pVarNums
Definition: cnf.h:63
l_True
#define l_True
Definition: SolverTypes.h:84
Bmc_ParFf_t_::fDumpUntest
int fDumpUntest
Definition: bmc.h:135
Gia_ManFormulaEndToken
char * Gia_ManFormulaEndToken(char *pForm)
Definition: bmcFault.c:468
FFTEST_MAX_PARS
#define FFTEST_MAX_PARS
Definition: bmcFault.c:34
Bmc_ParFf_t_::nTimeOut
int nTimeOut
Definition: bmc.h:131
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ManRealizeFormula_rec
int Gia_ManRealizeFormula_rec(Gia_Man_t *p, int *pVars, int *pPars, char *pBeg, char *pEnd, int nPars)
Definition: bmcFault.c:485
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_IntStartNatural
static Vec_Int_t * Vec_IntStartNatural(int nSize)
Definition: bblif.c:192
Cnf_AddCardinConstr
static int Cnf_AddCardinConstr(sat_solver *p, Vec_Int_t *vVars)
Definition: bmcFault.c:76
Cnf_Dat_t_
Definition: cnf.h:56
Gia_Obj_t_
Definition: gia.h:75
sat_solver_var_value
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
sat_solver_add_buffer
static int sat_solver_add_buffer(sat_solver *pSat, int iVarA, int iVarB, int fCompl)
Definition: satSolver.h:288
FFTEST_MAX_VARS
#define FFTEST_MAX_VARS
DECLARATIONS ///.
Definition: bmcFault.c:33
Gia_ManFaultCofactor
Gia_Man_t * Gia_ManFaultCofactor(Gia_Man_t *p, Vec_Int_t *vValues)
Definition: bmcFault.c:585
Bmc_ParFf_t_::fVerbose
int fVerbose
Definition: bmc.h:136
Gia_FormStrTransform
void Gia_FormStrTransform(char *pStr, char *pForm)
Definition: bmcFault.c:439
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Gia_ManAndNum
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Cnf_DeriveGiaRemapped
static Cnf_Dat_t * Cnf_DeriveGiaRemapped(Gia_Man_t *p)
Definition: bmcFault.c:137
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
Cnf_Dat_t_::pClauses
int ** pClauses
Definition: cnf.h:62
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjFanin1Copy
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
Gia_ManDumpUntests
int Gia_ManDumpUntests(Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, int nFuncVars, char *pFileName, int fVerbose)
Definition: bmcFault.c:728
ABC_PRTr
#define ABC_PRTr(a, t)
Definition: abc_global.h:221
Gia_ManFaultTest
void Gia_ManFaultTest(Gia_Man_t *p, Gia_Man_t *pG, Bmc_ParFf_t *pPars)
Definition: bmcFault.c:1068
Gia_ManFaultUnfold
Gia_Man_t * Gia_ManFaultUnfold(Gia_Man_t *p, int fUseMuxes)
Definition: bmcFault.c:181
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
sat_solver_setnvars
void sat_solver_setnvars(sat_solver *s, int n)
Definition: satSolver.c:1072
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
sat_solver_nvars
int sat_solver_nvars(sat_solver *s)
Definition: satSolver.c:1896
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Gia_ManHashMux
int Gia_ManHashMux(Gia_Man_t *p, int iCtrl, int iData1, int iData0)
Definition: giaHash.c:677
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ManPrintResults
void Gia_ManPrintResults(Gia_Man_t *p, sat_solver *pSat, int nIter, abctime clk)
Definition: bmcFault.c:644
Vec_IntAppend
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
Definition: extraZddTrunc.c:126
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_ObjFanin0Copy
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
sat_solver_nclauses
int sat_solver_nclauses(sat_solver *s)
Definition: satSolver.c:1902
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Bmc_ParFf_t_::fStartPats
int fStartPats
Definition: bmc.h:130
Gia_ManCiNum
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
Vec_IntEntryLast
static int Vec_IntEntryLast(Vec_Int_t *p)
Definition: bblif.c:319
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
sat_solver_simplify
int sat_solver_simplify(sat_solver *s)
Definition: satSolver.c:1276
sat_solver_new
sat_solver * sat_solver_new(void)
Definition: satSolver.c:1001
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_IntShrink
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
Gia_Man_t_
Definition: gia.h:95
Gia_ManGetTestPatterns
Vec_Int_t * Gia_ManGetTestPatterns(char *pFileName)
Definition: bmcFault.c:789
Gia_ManFaultPrepare
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
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManFlipUnfold
Gia_Man_t * Gia_ManFlipUnfold(Gia_Man_t *p, Vec_Int_t *vMap)
Definition: bmcFault.c:277
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
l_False
#define l_False
Definition: SolverTypes.h:85
Cnf_DataFree
void Cnf_DataFree(Cnf_Dat_t *p)
Definition: cnfMan.c:180
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_FormStrCount
int Gia_FormStrCount(char *pStr, int *pnVars, int *pnPars)
Definition: bmcFault.c:382
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
sat_solver_t
Definition: satSolver.h:91
Bmc_ParFf_t_::pFileName
char * pFileName
Definition: bmc.h:126
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Bmc_ParFf_t_::pFormStr
char * pFormStr
Definition: bmc.h:127
Gia_ManHashAlloc
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
Cnf_Dat_t_::nLiterals
int nLiterals
Definition: cnf.h:60
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_ManMiter
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
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManFaultAddOne
int Gia_ManFaultAddOne(Gia_Man_t *pM, Cnf_Dat_t *pCnf, sat_solver *pSat, Vec_Int_t *vLits, int nFuncVars)
Definition: bmcFault.c:675
Gia_ManCoNum
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
sat_solver_add_and
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
Bmc_ParFf_t_::fDump
int fDump
Definition: bmc.h:134
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387