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 #include "misc/extra/extra.h"
26
27 ABC_NAMESPACE_IMPL_START
28
29
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 #define FFTEST_MAX_VARS 2
35 #define FFTEST_MAX_PARS 8
36
37 ////////////////////////////////////////////////////////////////////////
38 /// FUNCTION DEFINITIONS ///
39 ////////////////////////////////////////////////////////////////////////
40
41 /**Function*************************************************************
42
43 Synopsis [This procedure sets default parameters.]
44
45 Description []
46
47 SideEffects []
48
49 SeeAlso []
50
51 ***********************************************************************/
Gia_DeriveFormula_rec(Gia_Man_t * pGia,char ** ppNamesIn,Vec_Str_t * vStr,int iLit)52 void Gia_DeriveFormula_rec( Gia_Man_t * pGia, char ** ppNamesIn, Vec_Str_t * vStr, int iLit )
53 {
54 Gia_Obj_t * pObj = Gia_ManObj( pGia, Abc_Lit2Var(iLit) );
55 int fCompl = Abc_LitIsCompl(iLit);
56 if ( Gia_ObjIsAnd(pObj) )
57 {
58 Vec_StrPush( vStr, '(' );
59 if ( Gia_ObjIsMux(pGia, pObj) )
60 {
61 Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Gia_ObjFaninLit0p(pGia, pObj) );
62 Vec_StrPush( vStr, '?' );
63 Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit1p(pGia, pObj), fCompl ) );
64 Vec_StrPush( vStr, ':' );
65 Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit2p(pGia, pObj), fCompl ) );
66 }
67 else
68 {
69 Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit0p(pGia, pObj), fCompl ) );
70 Vec_StrPush( vStr, (char)(Gia_ObjIsXor(pObj) ? '^' : (char)(fCompl ? '|' : '&')) );
71 Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Abc_LitNotCond( Gia_ObjFaninLit1p(pGia, pObj), fCompl ) );
72 }
73 Vec_StrPush( vStr, ')' );
74 }
75 else
76 {
77 if ( fCompl ) Vec_StrPush( vStr, '~' );
78 Vec_StrPrintF( vStr, "%s", ppNamesIn[Gia_ObjCioId(pObj)] );
79 }
80 }
Gia_DeriveFormula(Gia_Man_t * pGia,char ** ppNamesIn)81 char * Gia_DeriveFormula( Gia_Man_t * pGia, char ** ppNamesIn )
82 {
83 char * pResult;
84 Vec_Str_t * vStr = Vec_StrAlloc( 1000 );
85 Gia_Man_t * pMuxes = Gia_ManDupMuxes( pGia, 2 );
86 Gia_Obj_t * pObj = Gia_ManCo( pGia, 0 );
87 Vec_StrPush( vStr, '(' );
88 Gia_DeriveFormula_rec( pGia, ppNamesIn, vStr, Gia_ObjFaninLit0p(pGia, pObj) );
89 Vec_StrPush( vStr, ')' );
90 Vec_StrPush( vStr, '\0' );
91 Gia_ManStop( pMuxes );
92 pResult = Vec_StrReleaseArray( vStr );
93 Vec_StrFree( vStr );
94 return pResult;
95 }
96
97 /**Function*************************************************************
98
99 Synopsis [This procedure sets default parameters.]
100
101 Description []
102
103 SideEffects []
104
105 SeeAlso []
106
107 ***********************************************************************/
Gia_ParFfSetDefault(Bmc_ParFf_t * p)108 void Gia_ParFfSetDefault( Bmc_ParFf_t * p )
109 {
110 memset( p, 0, sizeof(Bmc_ParFf_t) );
111 p->pFileName = NULL;
112 p->Algo = 0;
113 p->fStartPats = 0;
114 p->nTimeOut = 0;
115 p->nIterCheck = 0;
116 p->fBasic = 0;
117 p->fFfOnly = 0;
118 p->fCheckUntest = 0;
119 p->fDump = 0;
120 p->fDumpUntest = 0;
121 p->fVerbose = 0;
122 }
123
124 /**Function*************************************************************
125
126 Synopsis [Adds a general cardinality constraint in terms of vVars.]
127
128 Description [Strict is "exactly K out of N". Non-strict is
129 "less or equal than K out of N".]
130
131 SideEffects []
132
133 SeeAlso []
134
135 ***********************************************************************/
Cnf_AddSorder(sat_solver * p,int * pVars,int i,int k,int * pnVars)136 static inline void Cnf_AddSorder( sat_solver * p, int * pVars, int i, int k, int * pnVars )
137 {
138 int iVar1 = (*pnVars)++;
139 int iVar2 = (*pnVars)++;
140 sat_solver_add_and( p, iVar1, pVars[i], pVars[k], 1, 1, 1 );
141 sat_solver_add_and( p, iVar2, pVars[i], pVars[k], 0, 0, 0 );
142 pVars[i] = iVar1;
143 pVars[k] = iVar2;
144 }
Cnf_AddCardinConstrMerge(sat_solver * p,int * pVars,int lo,int hi,int r,int * pnVars)145 static inline void Cnf_AddCardinConstrMerge( sat_solver * p, int * pVars, int lo, int hi, int r, int * pnVars )
146 {
147 int i, step = r * 2;
148 if ( step < hi - lo )
149 {
150 Cnf_AddCardinConstrMerge( p, pVars, lo, hi-r, step, pnVars );
151 Cnf_AddCardinConstrMerge( p, pVars, lo+r, hi, step, pnVars );
152 for ( i = lo+r; i < hi-r; i += step )
153 Cnf_AddSorder( p, pVars, i, i+r, pnVars );
154 }
155 }
Cnf_AddCardinConstrRange(sat_solver * p,int * pVars,int lo,int hi,int * pnVars)156 static inline void Cnf_AddCardinConstrRange( sat_solver * p, int * pVars, int lo, int hi, int * pnVars )
157 {
158 if ( hi - lo >= 1 )
159 {
160 int i, mid = lo + (hi - lo) / 2;
161 for ( i = lo; i <= mid; i++ )
162 Cnf_AddSorder( p, pVars, i, i + (hi - lo + 1) / 2, pnVars );
163 Cnf_AddCardinConstrRange( p, pVars, lo, mid, pnVars );
164 Cnf_AddCardinConstrRange( p, pVars, mid+1, hi, pnVars );
165 Cnf_AddCardinConstrMerge( p, pVars, lo, hi, 1, pnVars );
166 }
167 }
Cnf_AddCardinConstrPairWise(sat_solver * p,Vec_Int_t * vVars,int K,int fStrict)168 void Cnf_AddCardinConstrPairWise( sat_solver * p, Vec_Int_t * vVars, int K, int fStrict )
169 {
170 int nVars = sat_solver_nvars(p);
171 int nSizeOld = Vec_IntSize(vVars);
172 int i, iVar, nSize, Lit, nVarsOld;
173 assert( nSizeOld >= 2 );
174 // check that vars are ok
175 Vec_IntForEachEntry( vVars, iVar, i )
176 assert( iVar >= 0 && iVar < nVars );
177 // make the size a degree of two
178 for ( nSize = 1; nSize < nSizeOld; nSize *= 2 );
179 // extend
180 sat_solver_setnvars( p, nVars + 1 + nSize * nSize / 2 );
181 if ( nSize != nSizeOld )
182 {
183 // fill in with const0
184 Vec_IntFillExtra( vVars, nSize, nVars );
185 // add const0 variable
186 Lit = Abc_Var2Lit( nVars++, 1 );
187 if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
188 assert( 0 );
189 }
190 // construct recursively
191 nVarsOld = nVars;
192 Cnf_AddCardinConstrRange( p, Vec_IntArray(vVars), 0, nSize - 1, &nVars );
193 // add final constraint
194 assert( K > 0 && K < nSizeOld );
195 Lit = Abc_Var2Lit( Vec_IntEntry(vVars, K), 1 );
196 if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
197 assert( 0 );
198 if ( fStrict )
199 {
200 Lit = Abc_Var2Lit( Vec_IntEntry(vVars, K-1), 0 );
201 if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
202 assert( 0 );
203 }
204 // return to the old size
205 Vec_IntShrink( vVars, 0 ); // make it unusable
206 //printf( "The %d input sorting network contains %d sorters.\n", nSize, (nVars - nVarsOld)/2 );
207 }
208
209 /**Function*************************************************************
210
211 Synopsis [Adds a general cardinality constraint in terms of vVars.]
212
213 Description [Strict is "exactly K out of N". Non-strict is
214 "less or equal than K out of N".]
215
216 SideEffects []
217
218 SeeAlso []
219
220 ***********************************************************************/
Cnf_AddCardinVar(int Level,int Base,Vec_Int_t * vVars,int k)221 static inline int Cnf_AddCardinVar( int Level, int Base, Vec_Int_t * vVars, int k )
222 {
223 return Level ? Base + k : Vec_IntEntry( vVars, k );
224 }
Cnf_AddCardinConstrGeneral(sat_solver * p,Vec_Int_t * vVars,int K,int fStrict)225 void Cnf_AddCardinConstrGeneral( sat_solver * p, Vec_Int_t * vVars, int K, int fStrict )
226 {
227 int i, k, iCur, iNext, iVar, Lit;
228 int nVars = sat_solver_nvars(p);
229 int nBits = Vec_IntSize(vVars);
230 Vec_IntForEachEntry( vVars, iVar, i )
231 assert( iVar >= 0 && iVar < nVars );
232 sat_solver_setnvars( p, nVars + nBits * nBits );
233 for ( i = 0; i < nBits; i++ )
234 {
235 iCur = nVars + nBits * (i-1);
236 iNext = nVars + nBits * i;
237 if ( i & 1 )
238 sat_solver_add_buffer( p, iNext, Cnf_AddCardinVar(i, iCur, vVars, 0), 0 );
239 for ( k = i & 1; k + 1 < nBits; k += 2 )
240 {
241 sat_solver_add_and( p, iNext+k , Cnf_AddCardinVar(i, iCur, vVars, k), Cnf_AddCardinVar(i, iCur, vVars, k+1), 1, 1, 1 );
242 sat_solver_add_and( p, iNext+k+1, Cnf_AddCardinVar(i, iCur, vVars, k), Cnf_AddCardinVar(i, iCur, vVars, k+1), 0, 0, 0 );
243 }
244 if ( k == nBits - 1 )
245 sat_solver_add_buffer( p, iNext + nBits-1, Cnf_AddCardinVar(i, iCur, vVars, nBits-1), 0 );
246 }
247 // add final constraint
248 assert( K > 0 && K < nBits );
249 Lit = Abc_Var2Lit( nVars + nBits * (nBits - 1) + K, 1 );
250 if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
251 assert( 0 );
252 if ( fStrict )
253 {
254 Lit = Abc_Var2Lit( nVars + nBits * (nBits - 1) + K - 1, 0 );
255 if ( !sat_solver_addclause( p, &Lit, &Lit+1 ) )
256 assert( 0 );
257 }
258 }
259 /**Function*************************************************************
260
261 Synopsis [Add constraint that no more than 1 variable is 1.]
262
263 Description []
264
265 SideEffects []
266
267 SeeAlso []
268
269 ***********************************************************************/
Cnf_AddCardinConstr(sat_solver * p,Vec_Int_t * vVars)270 static inline int Cnf_AddCardinConstr( sat_solver * p, Vec_Int_t * vVars )
271 {
272 int i, k, pLits[2], iVar, nVars = sat_solver_nvars(p);
273 Vec_IntForEachEntry( vVars, iVar, i )
274 assert( iVar >= 0 && iVar < nVars );
275 iVar = nVars;
276 sat_solver_setnvars( p, nVars + Vec_IntSize(vVars) - 1 );
277 while ( Vec_IntSize(vVars) > 1 )
278 {
279 for ( k = i = 0; i < Vec_IntSize(vVars)/2; i++ )
280 {
281 pLits[0] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i), 1 );
282 pLits[1] = Abc_Var2Lit( Vec_IntEntry(vVars, 2*i+1), 1 );
283 sat_solver_addclause( p, pLits, pLits + 2 );
284 sat_solver_add_and( p, iVar, Vec_IntEntry(vVars, 2*i), Vec_IntEntry(vVars, 2*i+1), 1, 1, 1 );
285 Vec_IntWriteEntry( vVars, k++, iVar++ );
286 }
287 if ( Vec_IntSize(vVars) & 1 )
288 Vec_IntWriteEntry( vVars, k++, Vec_IntEntryLast(vVars) );
289 Vec_IntShrink( vVars, k );
290 }
291 return iVar;
292 }
Cnf_AddCardinConstrTest()293 void Cnf_AddCardinConstrTest()
294 {
295 int i, status, Count = 1, nVars = 8;
296 Vec_Int_t * vVars = Vec_IntStartNatural( nVars );
297 sat_solver * pSat = sat_solver_new();
298 sat_solver_setnvars( pSat, nVars );
299 //Cnf_AddCardinConstr( pSat, vVars );
300 Cnf_AddCardinConstrPairWise( pSat, vVars, 2, 1 );
301 while ( 1 )
302 {
303 status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 );
304 if ( status != l_True )
305 break;
306 Vec_IntClear( vVars );
307 printf( "%3d : ", Count++ );
308 for ( i = 0; i < nVars; i++ )
309 {
310 Vec_IntPush( vVars, Abc_Var2Lit(i, sat_solver_var_value(pSat, i)) );
311 printf( "%d", sat_solver_var_value(pSat, i) );
312 }
313 printf( "\n" );
314 status = sat_solver_addclause( pSat, Vec_IntArray(vVars), Vec_IntArray(vVars) + Vec_IntSize(vVars) );
315 if ( status == 0 )
316 break;
317 }
318 sat_solver_delete( pSat );
319 Vec_IntFree( vVars );
320 }
321
322 /**Function*************************************************************
323
324 Synopsis []
325
326 Description []
327
328 SideEffects []
329
330 SeeAlso []
331
332 ***********************************************************************/
Cnf_DeriveGiaRemapped(Gia_Man_t * p)333 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
334 {
335 Cnf_Dat_t * pCnf;
336 Aig_Man_t * pAig = Gia_ManToAigSimple( p );
337 pAig->nRegs = 0;
338 pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
339 Aig_ManStop( pAig );
340 return pCnf;
341 // return (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, 0, 0 );
342 }
343
344 /**Function*************************************************************
345
346 Synopsis []
347
348 Description []
349
350 SideEffects []
351
352 SeeAlso []
353
354 ***********************************************************************/
Cnf_DataLiftGia(Cnf_Dat_t * p,Gia_Man_t * pGia,int nVarsPlus)355 static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus )
356 {
357 Gia_Obj_t * pObj;
358 int v;
359 Gia_ManForEachObj( pGia, pObj, v )
360 if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 )
361 p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus;
362 for ( v = 0; v < p->nLiterals; v++ )
363 p->pClauses[0][v] += 2*nVarsPlus;
364 }
365
366 /**Function*************************************************************
367
368 Synopsis []
369
370 Description []
371
372 SideEffects []
373
374 SeeAlso []
375
376 ***********************************************************************/
Gia_ManFaultUnfold(Gia_Man_t * p,int fUseMuxes,int fFfOnly)377 Gia_Man_t * Gia_ManFaultUnfold( Gia_Man_t * p, int fUseMuxes, int fFfOnly )
378 {
379 Gia_Man_t * pNew, * pTemp;
380 Gia_Obj_t * pObj;
381 int i, iCtrl, iThis;
382 pNew = Gia_ManStart( (2 + 3 * fUseMuxes) * Gia_ManObjNum(p) );
383 pNew->pName = Abc_UtilStrsav( p->pName );
384 Gia_ManHashAlloc( pNew );
385 Gia_ManConst0(p)->Value = 0;
386 // add first timeframe
387 Gia_ManForEachRo( p, pObj, i )
388 pObj->Value = Gia_ManAppendCi( pNew );
389 Gia_ManForEachPi( p, pObj, i )
390 pObj->Value = Gia_ManAppendCi( pNew );
391 Gia_ManForEachAnd( p, pObj, i )
392 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
393 Gia_ManForEachCo( p, pObj, i )
394 pObj->Value = Gia_ObjFanin0Copy(pObj);
395 // add second timeframe
396 Gia_ManForEachRo( p, pObj, i )
397 pObj->Value = Gia_ObjRoToRi(p, pObj)->Value;
398 Gia_ManForEachPi( p, pObj, i )
399 pObj->Value = Gia_ManAppendCi( pNew );
400 if ( fFfOnly )
401 {
402 Gia_ManForEachAnd( p, pObj, i )
403 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
404 Gia_ManForEachPo( p, pObj, i )
405 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
406 Gia_ManForEachRi( p, pObj, i )
407 {
408 iCtrl = Gia_ManAppendCi(pNew);
409 iThis = Gia_ObjFanin0Copy(pObj);
410 if ( fUseMuxes )
411 pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis );
412 else
413 pObj->Value = iThis;
414 pObj->Value = Gia_ManAppendCo( pNew, pObj->Value );
415 }
416 }
417 else
418 {
419 Gia_ManForEachAnd( p, pObj, i )
420 {
421 iCtrl = Gia_ManAppendCi(pNew);
422 iThis = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
423 if ( fUseMuxes )
424 pObj->Value = Gia_ManHashMux( pNew, iCtrl, pObj->Value, iThis );
425 else
426 pObj->Value = iThis;
427 }
428 Gia_ManForEachCo( p, pObj, i )
429 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
430 }
431 pNew = Gia_ManCleanup( pTemp = pNew );
432 Gia_ManStop( pTemp );
433 assert( Gia_ManPiNum(pNew) == Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p) + (fFfOnly ? Gia_ManRegNum(p) : Gia_ManAndNum(p)) );
434 return pNew;
435 }
436
437 /**Function*************************************************************
438
439 Synopsis []
440
441 Description []
442
443 SideEffects []
444
445 SeeAlso []
446
447 ***********************************************************************/
Gia_ManStuckAtUnfold(Gia_Man_t * p,Vec_Int_t * vMap)448 Gia_Man_t * Gia_ManStuckAtUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
449 {
450 Gia_Man_t * pNew, * pTemp;
451 Gia_Obj_t * pObj;
452 int i, iFuncVars = 0;
453 pNew = Gia_ManStart( 3 * Gia_ManObjNum(p) );
454 pNew->pName = Abc_UtilStrsav( p->pName );
455 Gia_ManHashAlloc( pNew );
456 Gia_ManConst0(p)->Value = 0;
457 Gia_ManForEachCi( p, pObj, i )
458 pObj->Value = Gia_ManAppendCi( pNew );
459 Gia_ManForEachAnd( p, pObj, i )
460 {
461 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
462
463 if ( Vec_IntEntry(vMap, iFuncVars++) )
464 pObj->Value = Gia_ManHashAnd( pNew, Abc_LitNot(Gia_ManAppendCi(pNew)), pObj->Value );
465 else
466 Gia_ManAppendCi(pNew);
467
468 if ( Vec_IntEntry(vMap, iFuncVars++) )
469 pObj->Value = Gia_ManHashOr( pNew, Gia_ManAppendCi(pNew), pObj->Value );
470 else
471 Gia_ManAppendCi(pNew);
472 }
473 assert( iFuncVars == Vec_IntSize(vMap) );
474 Gia_ManForEachCo( p, pObj, i )
475 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
476 pNew = Gia_ManCleanup( pTemp = pNew );
477 Gia_ManStop( pTemp );
478 assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 2 * Gia_ManAndNum(p) );
479 return pNew;
480 }
481
482 /**Function*************************************************************
483
484 Synopsis []
485
486 Description []
487
488 SideEffects []
489
490 SeeAlso []
491
492 ***********************************************************************/
Gia_ManFlipUnfold(Gia_Man_t * p,Vec_Int_t * vMap)493 Gia_Man_t * Gia_ManFlipUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
494 {
495 Gia_Man_t * pNew, * pTemp;
496 Gia_Obj_t * pObj;
497 int i, iFuncVars = 0;
498 pNew = Gia_ManStart( 4 * Gia_ManObjNum(p) );
499 pNew->pName = Abc_UtilStrsav( p->pName );
500 Gia_ManHashAlloc( pNew );
501 Gia_ManConst0(p)->Value = 0;
502 Gia_ManForEachCi( p, pObj, i )
503 pObj->Value = Gia_ManAppendCi( pNew );
504 Gia_ManForEachAnd( p, pObj, i )
505 {
506 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
507 if ( Vec_IntEntry(vMap, iFuncVars++) )
508 pObj->Value = Gia_ManHashXor( pNew, Gia_ManAppendCi(pNew), pObj->Value );
509 else
510 Gia_ManAppendCi(pNew);
511 }
512 assert( iFuncVars == Vec_IntSize(vMap) );
513 Gia_ManForEachCo( p, pObj, i )
514 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
515 pNew = Gia_ManCleanup( pTemp = pNew );
516 Gia_ManStop( pTemp );
517 assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + Gia_ManAndNum(p) );
518 return pNew;
519 }
520
521 /**Function*************************************************************
522
523 Synopsis []
524
525 Description []
526
527 SideEffects []
528
529 SeeAlso []
530
531 ***********************************************************************/
Gia_ManFOFUnfold(Gia_Man_t * p,Vec_Int_t * vMap)532 Gia_Man_t * Gia_ManFOFUnfold( Gia_Man_t * p, Vec_Int_t * vMap )
533 {
534 Gia_Man_t * pNew, * pTemp;
535 Gia_Obj_t * pObj;
536 int i, iCtrl0, iCtrl1, iCtrl2, iCtrl3, iMuxA, iMuxB, iFuncVars = 0;
537 int VarLimit = 4 * Gia_ManAndNum(p);
538 pNew = Gia_ManStart( 9 * Gia_ManObjNum(p) );
539 pNew->pName = Abc_UtilStrsav( p->pName );
540 Gia_ManHashAlloc( pNew );
541 Gia_ManConst0(p)->Value = 0;
542 Gia_ManForEachCi( p, pObj, i )
543 pObj->Value = Gia_ManAppendCi( pNew );
544 Gia_ManForEachAnd( p, pObj, i )
545 {
546 if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
547 iCtrl0 = Gia_ManAppendCi(pNew);
548 else
549 iCtrl0 = 0, Gia_ManAppendCi(pNew);
550
551 if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
552 iCtrl1 = Gia_ManAppendCi(pNew);
553 else
554 iCtrl1 = 0, Gia_ManAppendCi(pNew);
555
556 if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
557 iCtrl2 = Gia_ManAppendCi(pNew);
558 else
559 iCtrl2 = 0, Gia_ManAppendCi(pNew);
560
561 if ( Vec_IntEntry(vMap, iFuncVars++) && iFuncVars < VarLimit )
562 iCtrl3 = Gia_ManAppendCi(pNew);
563 else
564 iCtrl3 = 0, Gia_ManAppendCi(pNew);
565
566 if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
567 iCtrl0 = Abc_LitNot(iCtrl0);
568 else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) )
569 iCtrl1 = Abc_LitNot(iCtrl1);
570 else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
571 iCtrl2 = Abc_LitNot(iCtrl2);
572 else //if ( !Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) )
573 iCtrl3 = Abc_LitNot(iCtrl3);
574
575 iMuxA = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl1, iCtrl0 );
576 iMuxB = Gia_ManHashMux( pNew, Gia_ObjFanin0(pObj)->Value, iCtrl3, iCtrl2 );
577 pObj->Value = Gia_ManHashMux( pNew, Gia_ObjFanin1(pObj)->Value, iMuxB, iMuxA );
578 }
579 assert( iFuncVars == Vec_IntSize(vMap) );
580 Gia_ManForEachCo( p, pObj, i )
581 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
582 pNew = Gia_ManCleanup( pTemp = pNew );
583 Gia_ManStop( pTemp );
584 assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + 4 * Gia_ManAndNum(p) );
585 return pNew;
586 }
587
588 /**Function*************************************************************
589
590 Synopsis [This procedure sets default parameters.]
591
592 Description []
593
594 SideEffects []
595
596 SeeAlso []
597
598 ***********************************************************************/
Gia_FormStrCount(char * pStr,int * pnVars,int * pnPars)599 int Gia_FormStrCount( char * pStr, int * pnVars, int * pnPars )
600 {
601 int i, Counter = 0;
602 if ( pStr[0] != '(' )
603 {
604 printf( "The first symbol should be the opening parenthesis \"(\".\n" );
605 return 1;
606 }
607 if ( pStr[strlen(pStr)-1] != ')' )
608 {
609 printf( "The last symbol should be the closing parenthesis \")\".\n" );
610 return 1;
611 }
612 for ( i = 0; pStr[i]; i++ )
613 if ( pStr[i] == '(' )
614 Counter++;
615 else if ( pStr[i] == ')' )
616 Counter--;
617 if ( Counter != 0 )
618 {
619 printf( "The number of opening and closing parentheses is not equal.\n" );
620 return 1;
621 }
622 *pnVars = 0;
623 *pnPars = 0;
624 for ( i = 0; pStr[i]; i++ )
625 {
626 if ( pStr[i] >= 'a' && pStr[i] <= 'b' )
627 *pnVars = Abc_MaxInt( *pnVars, pStr[i] - 'a' + 1 );
628 else if ( pStr[i] >= 'p' && pStr[i] <= 's' )
629 *pnPars = Abc_MaxInt( *pnPars, pStr[i] - 'p' + 1 );
630 else if ( pStr[i] == '(' || pStr[i] == ')' )
631 {}
632 else if ( pStr[i] == '&' || pStr[i] == '|' || pStr[i] == '^' )
633 {}
634 else if ( pStr[i] == '?' || pStr[i] == ':' )
635 {}
636 else if ( pStr[i] == '~' )
637 {
638 if ( pStr[i+1] < 'a' || pStr[i+1] > 'z' )
639 {
640 printf( "Expecting alphabetic symbol (instead of \"%c\") after negation (~)\n", pStr[i+1] );
641 return 1;
642 }
643 }
644 else
645 {
646 printf( "Unknown symbol (%c) in the formula (%s)\n", pStr[i], pStr );
647 return 1;
648 }
649 }
650 if ( *pnVars != FFTEST_MAX_VARS )
651 { printf( "The number of input variables (%d) should be 2\n", *pnVars ); return 1; }
652 if ( *pnPars < 1 || *pnPars > FFTEST_MAX_PARS )
653 { printf( "The number of parameters should be between 1 and %d\n", FFTEST_MAX_PARS ); return 1; }
654 return 0;
655 }
Gia_FormStrTransform(char * pStr,char * pForm)656 void Gia_FormStrTransform( char * pStr, char * pForm )
657 {
658 int i, k;
659 for ( k = i = 0; pForm[i]; i++ )
660 {
661 if ( pForm[i] == '~' )
662 {
663 i++;
664 assert( pForm[i] >= 'a' && pForm[i] <= 'z' );
665 pStr[k++] = 'A' + pForm[i] - 'a';
666 }
667 else
668 pStr[k++] = pForm[i];
669 }
670 pStr[k] = 0;
671 }
672
673 /**Function*************************************************************
674
675 Synopsis [Print formula.]
676
677 Description []
678
679 SideEffects []
680
681 SeeAlso []
682
683 ***********************************************************************/
Gia_ManFormulaEndToken(char * pForm)684 char * Gia_ManFormulaEndToken( char * pForm )
685 {
686 int Counter = 0;
687 char * pThis;
688 for ( pThis = pForm; *pThis; pThis++ )
689 {
690 assert( *pThis != '~' );
691 if ( *pThis == '(' )
692 Counter++;
693 else if ( *pThis == ')' )
694 Counter--;
695 if ( Counter == 0 )
696 return pThis + 1;
697 }
698 assert( 0 );
699 return NULL;
700 }
Gia_ManPrintFormula_rec(char * pBeg,char * pEnd)701 void Gia_ManPrintFormula_rec( char * pBeg, char * pEnd )
702 {
703 int Oper = -1;
704 char * pEndNew;
705 if ( pBeg + 1 == pEnd )
706 {
707 if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
708 printf( "%c", pBeg[0] );
709 else if ( pBeg[0] >= 'A' && pBeg[0] <= 'B' )
710 printf( "~%c", pBeg[0]-'A'+'a' );
711 else if ( pBeg[0] >= 'p' && pBeg[0] <= 'w' ) // pqrstuvw
712 printf( "%c", pBeg[0] );
713 else if ( pBeg[0] >= 'P' && pBeg[0] <= 'W' )
714 printf( "~%c", pBeg[0]-'A'+'a' );
715 return;
716 }
717 if ( pBeg[0] == '(' )
718 {
719 pEndNew = Gia_ManFormulaEndToken( pBeg );
720 if ( pEndNew == pEnd )
721 {
722 assert( pBeg[0] == '(' );
723 assert( pBeg[pEnd-pBeg-1] == ')' );
724 Gia_ManPrintFormula_rec( pBeg + 1, pEnd - 1 );
725 return;
726 }
727 }
728 // get first part
729 pEndNew = Gia_ManFormulaEndToken( pBeg );
730 printf( "(" );
731 Gia_ManPrintFormula_rec( pBeg, pEndNew );
732 printf( ")" );
733 Oper = pEndNew[0];
734 // derive the formula
735 if ( Oper == '&' )
736 printf( "&" );
737 else if ( Oper == '|' )
738 printf( "|" );
739 else if ( Oper == '^' )
740 printf( "^" );
741 else if ( Oper == '?' )
742 printf( "?" );
743 else assert( 0 );
744 // get second part
745 pBeg = pEndNew + 1;
746 pEndNew = Gia_ManFormulaEndToken( pBeg );
747 printf( "(" );
748 Gia_ManPrintFormula_rec( pBeg, pEndNew );
749 printf( ")" );
750 if ( Oper == '?' )
751 {
752 printf( ":" );
753 // get third part
754 assert( Oper == '?' );
755 assert( pEndNew[0] == ':' );
756 pBeg = pEndNew + 1;
757 pEndNew = Gia_ManFormulaEndToken( pBeg );
758 printf( "(" );
759 Gia_ManPrintFormula_rec( pBeg, pEndNew );
760 printf( ")" );
761 }
762 }
Gia_ManPrintFormula(char * pStr)763 void Gia_ManPrintFormula( char * pStr )
764 {
765 printf( "Using formula: " );
766 printf( "(" );
767 Gia_ManPrintFormula_rec( pStr, pStr + strlen(pStr) );
768 printf( ")" );
769 printf( "\n" );
770 }
771
772 /**Function*************************************************************
773
774 Synopsis [Implements fault model formula using functional/parameter vars.]
775
776 Description []
777
778 SideEffects []
779
780 SeeAlso []
781
782 ***********************************************************************/
Gia_ManRealizeFormula_rec(Gia_Man_t * p,int * pVars,int * pPars,char * pBeg,char * pEnd,int nPars)783 int Gia_ManRealizeFormula_rec( Gia_Man_t * p, int * pVars, int * pPars, char * pBeg, char * pEnd, int nPars )
784 {
785 int iFans[3], Oper = -1;
786 char * pEndNew;
787 if ( pBeg + 1 == pEnd )
788 {
789 if ( pBeg[0] >= 'a' && pBeg[0] <= 'b' )
790 return pVars[pBeg[0] - 'a'];
791 if ( pBeg[0] >= 'A' && pBeg[0] <= 'B' )
792 return Abc_LitNot( pVars[pBeg[0] - 'A'] );
793 if ( pBeg[0] >= 'p' && pBeg[0] <= 'w' ) // pqrstuvw
794 return pPars[pBeg[0] - 'p'];
795 if ( pBeg[0] >= 'P' && pBeg[0] <= 'W' )
796 return Abc_LitNot( pPars[pBeg[0] - 'P'] );
797 assert( 0 );
798 return -1;
799 }
800 if ( pBeg[0] == '(' )
801 {
802 pEndNew = Gia_ManFormulaEndToken( pBeg );
803 if ( pEndNew == pEnd )
804 {
805 assert( pBeg[0] == '(' );
806 assert( pBeg[pEnd-pBeg-1] == ')' );
807 return Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg + 1, pEnd - 1, nPars );
808 }
809 }
810 // get first part
811 pEndNew = Gia_ManFormulaEndToken( pBeg );
812 iFans[0] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
813 Oper = pEndNew[0];
814 // get second part
815 pBeg = pEndNew + 1;
816 pEndNew = Gia_ManFormulaEndToken( pBeg );
817 iFans[1] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
818 // derive the formula
819 if ( Oper == '&' )
820 return Gia_ManHashAnd( p, iFans[0], iFans[1] );
821 if ( Oper == '|' )
822 return Gia_ManHashOr( p, iFans[0], iFans[1] );
823 if ( Oper == '^' )
824 return Gia_ManHashXor( p, iFans[0], iFans[1] );
825 // get third part
826 assert( Oper == '?' );
827 assert( pEndNew[0] == ':' );
828 pBeg = pEndNew + 1;
829 pEndNew = Gia_ManFormulaEndToken( pBeg );
830 iFans[2] = Gia_ManRealizeFormula_rec( p, pVars, pPars, pBeg, pEndNew, nPars );
831 return Gia_ManHashMux( p, iFans[0], iFans[1], iFans[2] );
832 }
Gia_ManRealizeFormula(Gia_Man_t * p,int * pVars,int * pPars,char * pStr,int nPars)833 int Gia_ManRealizeFormula( Gia_Man_t * p, int * pVars, int * pPars, char * pStr, int nPars )
834 {
835 return Gia_ManRealizeFormula_rec( p, pVars, pPars, pStr, pStr + strlen(pStr), nPars );
836 }
Gia_ManFormulaUnfold(Gia_Man_t * p,char * pForm,int fFfOnly)837 Gia_Man_t * Gia_ManFormulaUnfold( Gia_Man_t * p, char * pForm, int fFfOnly )
838 {
839 char pStr[100];
840 int Count = 0;
841 Gia_Man_t * pNew, * pTemp;
842 Gia_Obj_t * pObj;
843 int i, k, iCtrl[FFTEST_MAX_PARS], iFans[FFTEST_MAX_VARS];
844 int nVars, nPars;
845 assert( strlen(pForm) < 100 );
846 Gia_FormStrCount( pForm, &nVars, &nPars );
847 assert( nVars == 2 );
848 Gia_FormStrTransform( pStr, pForm );
849 Gia_ManPrintFormula( pStr );
850 pNew = Gia_ManStart( 5 * Gia_ManObjNum(p) );
851 pNew->pName = Abc_UtilStrsav( p->pName );
852 Gia_ManHashAlloc( pNew );
853 Gia_ManConst0(p)->Value = 0;
854 Gia_ManForEachCi( p, pObj, i )
855 pObj->Value = Gia_ManAppendCi( pNew );
856 if ( fFfOnly )
857 {
858 Gia_ManCleanMark0( p );
859 Gia_ManForEachRi( p, pObj, i )
860 Gia_ObjFanin0(pObj)->fMark0 = 1;
861 Gia_ManForEachAnd( p, pObj, i )
862 {
863 if ( pObj->fMark0 )
864 {
865 for ( k = 0; k < nPars; k++ )
866 iCtrl[k] = Gia_ManAppendCi(pNew);
867 iFans[0] = Gia_ObjFanin0Copy(pObj);
868 iFans[1] = Gia_ObjFanin1Copy(pObj);
869 pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars );
870 Count++;
871 }
872 else
873 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
874 }
875 Gia_ManForEachRi( p, pObj, i )
876 Gia_ObjFanin0(pObj)->fMark0 = 0;
877 }
878 else
879 {
880 Gia_ManForEachAnd( p, pObj, i )
881 {
882 for ( k = 0; k < nPars; k++ )
883 iCtrl[k] = Gia_ManAppendCi(pNew);
884 iFans[0] = Gia_ObjFanin0Copy(pObj);
885 iFans[1] = Gia_ObjFanin1Copy(pObj);
886 pObj->Value = Gia_ManRealizeFormula( pNew, iFans, iCtrl, pStr, nPars );
887 }
888 }
889 Gia_ManForEachCo( p, pObj, i )
890 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
891 pNew = Gia_ManCleanup( pTemp = pNew );
892 Gia_ManStop( pTemp );
893 assert( Gia_ManPiNum(pNew) == Gia_ManCiNum(p) + nPars * (fFfOnly ? Count : Gia_ManAndNum(p)) );
894 // if ( fUseFaults )
895 // Gia_AigerWrite( pNew, "newfault.aig", 0, 0, 0 );
896 return pNew;
897 }
898
899 /**Function*************************************************************
900
901 Synopsis []
902
903 Description []
904
905 SideEffects []
906
907 SeeAlso []
908
909 ***********************************************************************/
Gia_ManFaultCofactor(Gia_Man_t * p,Vec_Int_t * vValues)910 Gia_Man_t * Gia_ManFaultCofactor( Gia_Man_t * p, Vec_Int_t * vValues )
911 {
912 Gia_Man_t * pNew, * pTemp;
913 Gia_Obj_t * pObj;
914 int i;
915 pNew = Gia_ManStart( Gia_ManObjNum(p) );
916 pNew->pName = Abc_UtilStrsav( p->pName );
917 Gia_ManHashAlloc( pNew );
918 Gia_ManConst0(p)->Value = 0;
919 Gia_ManForEachPi( p, pObj, i )
920 {
921 pObj->Value = Gia_ManAppendCi( pNew );
922 if ( i < Vec_IntSize(vValues) )
923 pObj->Value = Vec_IntEntry( vValues, i );
924 }
925 Gia_ManForEachAnd( p, pObj, i )
926 pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
927 Gia_ManForEachCo( p, pObj, i )
928 pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
929 pNew = Gia_ManCleanup( pTemp = pNew );
930 Gia_ManStop( pTemp );
931 assert( Gia_ManPiNum(pNew) == Gia_ManPiNum(p) );
932 return pNew;
933
934 }
935
936 /**Function*************************************************************
937
938 Synopsis []
939
940 Description []
941
942 SideEffects []
943
944 SeeAlso []
945
946 ***********************************************************************/
Gia_ManDumpTests(Vec_Int_t * vTests,int nIter,char * pFileName)947 void Gia_ManDumpTests( Vec_Int_t * vTests, int nIter, char * pFileName )
948 {
949 FILE * pFile = fopen( pFileName, "wb" );
950 int i, k, v, nVars = Vec_IntSize(vTests) / nIter;
951 assert( Vec_IntSize(vTests) % nIter == 0 );
952 for ( v = i = 0; i < nIter; i++, fprintf(pFile, "\n") )
953 for ( k = 0; k < nVars; k++ )
954 fprintf( pFile, "%d", Vec_IntEntry(vTests, v++) );
955 fclose( pFile );
956 }
957
958 /**Function*************************************************************
959
960 Synopsis []
961
962 Description []
963
964 SideEffects []
965
966 SeeAlso []
967
968 ***********************************************************************/
Gia_ManDumpTestsSimulate(Gia_Man_t * p,Vec_Int_t * vValues)969 void Gia_ManDumpTestsSimulate( Gia_Man_t * p, Vec_Int_t * vValues )
970 {
971 Gia_Obj_t * pObj; int k;
972 assert( Vec_IntSize(vValues) == Gia_ManCiNum(p) );
973 Gia_ManConst0(p)->fMark0 = 0;
974 Gia_ManForEachCi( p, pObj, k )
975 pObj->fMark0 = Vec_IntEntry( vValues, k );
976 Gia_ManForEachAnd( p, pObj, k )
977 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
978 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
979 Gia_ManForEachCo( p, pObj, k )
980 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
981 // collect flop input values
982 Vec_IntClear( vValues );
983 Gia_ManForEachRi( p, pObj, k )
984 Vec_IntPush( vValues, pObj->fMark0 );
985 assert( Vec_IntSize(vValues) == Gia_ManRegNum(p) );
986 }
Gia_ManDumpTestsDelay(Vec_Int_t * vTests,int nIter,char * pFileName,Gia_Man_t * p)987 void Gia_ManDumpTestsDelay( Vec_Int_t * vTests, int nIter, char * pFileName, Gia_Man_t * p )
988 {
989 FILE * pFile = fopen( pFileName, "wb" );
990 Vec_Int_t * vValues = Vec_IntAlloc( Gia_ManCiNum(p) );
991 int i, v, nVars = Vec_IntSize(vTests) / nIter;
992 assert( Vec_IntSize(vTests) % nIter == 0 );
993 assert( nVars == 2 * Gia_ManPiNum(p) + Gia_ManRegNum(p) );
994 for ( i = 0; i < nIter; i++ )
995 {
996 // collect PIs followed by flops
997 Vec_IntClear( vValues );
998 for ( v = Gia_ManRegNum(p); v < Gia_ManCiNum(p); v++ )
999 {
1000 fprintf( pFile, "%d", Vec_IntEntry(vTests, i * nVars + v) );
1001 Vec_IntPush( vValues, Vec_IntEntry(vTests, i * nVars + v) );
1002 }
1003 for ( v = 0; v < Gia_ManRegNum(p); v++ )
1004 {
1005 fprintf( pFile, "%d", Vec_IntEntry(vTests, i * nVars + v) );
1006 Vec_IntPush( vValues, Vec_IntEntry(vTests, i * nVars + v) );
1007 }
1008 fprintf( pFile, "\n" );
1009 // derive next-state values
1010 Gia_ManDumpTestsSimulate( p, vValues );
1011 // collect PIs followed by flops
1012 for ( v = Gia_ManCiNum(p); v < nVars; v++ )
1013 fprintf( pFile, "%d", Vec_IntEntry(vTests, i * nVars + v) );
1014 for ( v = 0; v < Vec_IntSize(vValues); v++ )
1015 fprintf( pFile, "%d", Vec_IntEntry(vValues, v) );
1016 fprintf( pFile, "\n" );
1017 }
1018 Gia_ManCleanMark0(p);
1019 fclose( pFile );
1020 Vec_IntFree( vValues );
1021 }
1022
1023 /**Function*************************************************************
1024
1025 Synopsis []
1026
1027 Description []
1028
1029 SideEffects []
1030
1031 SeeAlso []
1032
1033 ***********************************************************************/
Gia_ManPrintResults(Gia_Man_t * p,sat_solver * pSat,int nIter,abctime clk)1034 void Gia_ManPrintResults( Gia_Man_t * p, sat_solver * pSat, int nIter, abctime clk )
1035 {
1036 FILE * pTable = fopen( "fault_stats.txt", "a+" );
1037
1038 fprintf( pTable, "%s ", Gia_ManName(p) );
1039 fprintf( pTable, "%d ", Gia_ManPiNum(p) );
1040 fprintf( pTable, "%d ", Gia_ManPoNum(p) );
1041 fprintf( pTable, "%d ", Gia_ManRegNum(p) );
1042 fprintf( pTable, "%d ", Gia_ManAndNum(p) );
1043
1044 fprintf( pTable, "%d ", sat_solver_nvars(pSat) );
1045 fprintf( pTable, "%d ", sat_solver_nclauses(pSat) );
1046 fprintf( pTable, "%d ", sat_solver_nconflicts(pSat) );
1047
1048 fprintf( pTable, "%d ", nIter );
1049 fprintf( pTable, "%.2f", 1.0*clk/CLOCKS_PER_SEC );
1050 fprintf( pTable, "\n" );
1051 fclose( pTable );
1052 }
1053
1054 /**Function*************************************************************
1055
1056 Synopsis []
1057
1058 Description []
1059
1060 SideEffects []
1061
1062 SeeAlso []
1063
1064 ***********************************************************************/
Gia_ManFaultAddOne(Gia_Man_t * pM,Cnf_Dat_t * pCnf,sat_solver * pSat,Vec_Int_t * vLits,int nFuncVars,int fAddOr,Gia_Man_t * pGiaCnf)1065 int Gia_ManFaultAddOne( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, Vec_Int_t * vLits, int nFuncVars, int fAddOr, Gia_Man_t * pGiaCnf )
1066 {
1067 Gia_Man_t * pC;//, * pTemp;
1068 Cnf_Dat_t * pCnf2;
1069 Gia_Obj_t * pObj;
1070 int i, Lit;
1071 // derive the cofactor
1072 pC = Gia_ManFaultCofactor( pM, vLits );
1073 // derive new CNF
1074 pCnf2 = Cnf_DeriveGiaRemapped( pC );
1075 Cnf_DataLiftGia( pCnf2, pC, sat_solver_nvars(pSat) );
1076 // add timeframe clauses
1077 for ( i = 0; i < pCnf2->nClauses; i++ )
1078 if ( !sat_solver_addclause( pSat, pCnf2->pClauses[i], pCnf2->pClauses[i+1] ) )
1079 {
1080 Cnf_DataFree( pCnf2 );
1081 Gia_ManStop( pC );
1082 return 0;
1083 }
1084 // add constraint clauses
1085 if ( fAddOr )
1086 {
1087 // add one OR gate to assert difference of at least one output of the miter
1088 Vec_Int_t * vOrGate = Vec_IntAlloc( Gia_ManPoNum(pC) );
1089 Gia_ManForEachPo( pC, pObj, i )
1090 {
1091 Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 0 );
1092 Vec_IntPush( vOrGate, Lit );
1093 }
1094 if ( !sat_solver_addclause( pSat, Vec_IntArray(vOrGate), Vec_IntArray(vOrGate) + Vec_IntSize(vOrGate) ) )
1095 assert( 0 );
1096 Vec_IntFree( vOrGate );
1097 }
1098 else
1099 {
1100 // add negative literals to assert equality of all outputs of the miter
1101 Gia_ManForEachPo( pC, pObj, i )
1102 {
1103 Lit = Abc_Var2Lit( pCnf2->pVarNums[Gia_ObjId(pC, pObj)], 1 );
1104 if ( !sat_solver_addclause( pSat, &Lit, &Lit+1 ) )
1105 {
1106 Cnf_DataFree( pCnf2 );
1107 Gia_ManStop( pC );
1108 return 0;
1109 }
1110 }
1111 }
1112 // add connection clauses
1113 if ( pGiaCnf )
1114 {
1115 Gia_ManForEachPi( pGiaCnf, pObj, i )
1116 if ( i >= nFuncVars )
1117 sat_solver_add_buffer( pSat, pCnf->pVarNums[Gia_ObjId(pGiaCnf, pObj)], pCnf2->pVarNums[Gia_ObjId(pC, Gia_ManPi(pC, i))], 0 );
1118 }
1119 Cnf_DataFree( pCnf2 );
1120 Gia_ManStop( pC );
1121 return 1;
1122 }
1123
1124
1125 /**Function*************************************************************
1126
1127 Synopsis []
1128
1129 Description []
1130
1131 SideEffects []
1132
1133 SeeAlso []
1134
1135 ***********************************************************************/
Gia_ManDumpUntests(Gia_Man_t * pM,Cnf_Dat_t * pCnf,sat_solver * pSat,int nFuncVars,char * pFileName,int fVerbose)1136 int Gia_ManDumpUntests( Gia_Man_t * pM, Cnf_Dat_t * pCnf, sat_solver * pSat, int nFuncVars, char * pFileName, int fVerbose )
1137 {
1138 FILE * pFile = fopen( pFileName, "wb" );
1139 Vec_Int_t * vLits;
1140 Gia_Obj_t * pObj;
1141 int nItersMax = 10000;
1142 int i, nIters, status, Value, Count = 0;
1143 vLits = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
1144 for ( nIters = 0; nIters < nItersMax; nIters++ )
1145 {
1146 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1147 if ( status == l_Undef )
1148 printf( "Timeout reached after dumping %d untestable faults.\n", nIters );
1149 if ( status == l_Undef )
1150 break;
1151 if ( status == l_False )
1152 break;
1153 // collect literals
1154 Vec_IntClear( vLits );
1155 Gia_ManForEachPi( pM, pObj, i )
1156 if ( i >= nFuncVars )
1157 Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)])) );
1158 // dump the fault
1159 Vec_IntForEachEntry( vLits, Value, i )
1160 if ( Abc_LitIsCompl(Value) )
1161 break;
1162 if ( i < Vec_IntSize(vLits) )
1163 {
1164 if ( fVerbose )
1165 {
1166 printf( "Untestable fault %4d : ", ++Count );
1167 Vec_IntForEachEntry( vLits, Value, i )
1168 if ( Abc_LitIsCompl(Value) )
1169 printf( "%d ", i );
1170 printf( "\n" );
1171 }
1172 Vec_IntForEachEntry( vLits, Value, i )
1173 if ( Abc_LitIsCompl(Value) )
1174 fprintf( pFile, "%d ", i );
1175 fprintf( pFile, "\n" );
1176 }
1177 // add this clause
1178 if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) ) )
1179 break;
1180 }
1181 Vec_IntFree( vLits );
1182 fclose( pFile );
1183 return nIters;
1184 }
1185
1186 /**Function*************************************************************
1187
1188 Synopsis []
1189
1190 Description []
1191
1192 SideEffects []
1193
1194 SeeAlso []
1195
1196 ***********************************************************************/
Gia_ManGetTestPatterns(char * pFileName)1197 Vec_Int_t * Gia_ManGetTestPatterns( char * pFileName )
1198 {
1199 FILE * pFile = fopen( pFileName, "rb" );
1200 Vec_Int_t * vTests; int c;
1201 if ( pFile == NULL )
1202 {
1203 printf( "Cannot open input file \"%s\".\n", pFileName );
1204 return NULL;
1205 }
1206 vTests = Vec_IntAlloc( 10000 );
1207 while ( (c = fgetc(pFile)) != EOF )
1208 {
1209 if ( c == ' ' || c == '\t' || c == '\r' || c == '\n' )
1210 continue;
1211 if ( c != '0' && c != '1' )
1212 {
1213 printf( "Wrong symbol (%c) in the input file.\n", c );
1214 Vec_IntFreeP( &vTests );
1215 break;
1216 }
1217 Vec_IntPush( vTests, c - '0' );
1218 }
1219 fclose( pFile );
1220 return vTests;
1221 }
1222
1223 /**Function*************************************************************
1224
1225 Synopsis [Derive the second AIG.]
1226
1227 Description []
1228
1229 SideEffects []
1230
1231 SeeAlso []
1232
1233 ***********************************************************************/
Gia_ManDeriveDup(Gia_Man_t * p,int nPisNew)1234 Gia_Man_t * Gia_ManDeriveDup( Gia_Man_t * p, int nPisNew )
1235 {
1236 int i;
1237 Gia_Man_t * pNew = Gia_ManDup(p);
1238 for ( i = 0; i < nPisNew; i++ )
1239 Gia_ManAppendCi( pNew );
1240 return pNew;
1241 }
1242
1243 /**Function*************************************************************
1244
1245 Synopsis []
1246
1247 Description []
1248
1249 SideEffects []
1250
1251 SeeAlso []
1252
1253 ***********************************************************************/
Gia_ManFaultAnalyze(sat_solver * pSat,Vec_Int_t * vPars,Vec_Int_t * vMap,Vec_Int_t * vLits,int Iter)1254 int Gia_ManFaultAnalyze( sat_solver * pSat, Vec_Int_t * vPars, Vec_Int_t * vMap, Vec_Int_t * vLits, int Iter )
1255 {
1256 int nConfLimit = 100;
1257 int status, i, v, iVar, Lit;
1258 int nUnsats = 0, nRuns = 0;
1259 abctime clk = Abc_Clock();
1260 assert( Vec_IntSize(vPars) == Vec_IntSize(vMap) );
1261 // check presence of each variable
1262 Vec_IntClear( vLits );
1263 Vec_IntAppend( vLits, vMap );
1264 for ( v = 0; v < Vec_IntSize(vPars); v++ )
1265 {
1266 if ( !Vec_IntEntry(vLits, v) )
1267 continue;
1268 assert( Vec_IntEntry(vLits, v) == 1 );
1269 nRuns++;
1270 Lit = Abc_Var2Lit( Vec_IntEntry(vPars, v), 0 );
1271 status = sat_solver_solve( pSat, &Lit, &Lit+1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1272 if ( status == l_Undef )
1273 continue;
1274 if ( status == l_False )
1275 {
1276 nUnsats++;
1277 assert( Vec_IntEntry(vMap, v) == 1 );
1278 Vec_IntWriteEntry( vMap, v, 0 );
1279 Lit = Abc_LitNot(Lit);
1280 //status = sat_solver_addclause( pSat, &Lit, &Lit+1 );
1281 //assert( status );
1282 continue;
1283 }
1284 Vec_IntForEachEntry( vPars, iVar, i )
1285 if ( Vec_IntEntry(vLits, i) && sat_solver_var_value(pSat, iVar) )
1286 Vec_IntWriteEntry( vLits, i, 0 );
1287 assert( Vec_IntEntry(vLits, v) == 0 );
1288 }
1289 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 );
1290 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1291 return nUnsats;
1292 }
1293
1294 /**Function*************************************************************
1295
1296 Synopsis [Dump faults detected by the new test, which are not detected by previous tests.]
1297
1298 Description []
1299
1300 SideEffects []
1301
1302 SeeAlso []
1303
1304 ***********************************************************************/
Gia_ManFaultDumpNewFaults(Gia_Man_t * pM,int nFuncVars,Vec_Int_t * vTests,Vec_Int_t * vTestNew,Bmc_ParFf_t * pPars)1305 int Gia_ManFaultDumpNewFaults( Gia_Man_t * pM, int nFuncVars, Vec_Int_t * vTests, Vec_Int_t * vTestNew, Bmc_ParFf_t * pPars )
1306 {
1307 char * pFileName = "newfaults.txt";
1308 abctime clk;
1309 Gia_Man_t * pC;
1310 Cnf_Dat_t * pCnf2;
1311 sat_solver * pSat;
1312 Vec_Int_t * vLits;
1313 int i, Iter, IterMax, nNewFaults;
1314
1315 // derive the cofactor
1316 pC = Gia_ManFaultCofactor( pM, vTestNew );
1317 // derive new CNF
1318 pCnf2 = Cnf_DeriveGiaRemapped( pC );
1319
1320 // create SAT solver
1321 pSat = sat_solver_new();
1322 sat_solver_setnvars( pSat, 1 );
1323 sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
1324 // create the first cofactor
1325 Gia_ManFaultAddOne( pM, NULL, pSat, vTestNew, nFuncVars, 1, NULL );
1326
1327 // add other test patterns
1328 assert( Vec_IntSize(vTests) % nFuncVars == 0 );
1329 IterMax = Vec_IntSize(vTests) / nFuncVars;
1330 vLits = Vec_IntAlloc( nFuncVars );
1331 for ( Iter = 0; Iter < IterMax; Iter++ )
1332 {
1333 // get pattern
1334 Vec_IntClear( vLits );
1335 for ( i = 0; i < nFuncVars; i++ )
1336 Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
1337 // the resulting problem cannot be UNSAT, because the new test is guaranteed
1338 // to detect something that the given test set does not detect
1339 if ( !Gia_ManFaultAddOne( pM, pCnf2, pSat, vLits, nFuncVars, 0, pC ) )
1340 assert( 0 );
1341 }
1342 Vec_IntFree( vLits );
1343
1344 // dump the new faults
1345 clk = Abc_Clock();
1346 nNewFaults = Gia_ManDumpUntests( pC, pCnf2, pSat, nFuncVars, pFileName, pPars->fVerbose );
1347 printf( "Dumped %d new multiple faults into file \"%s\". ", nNewFaults, pFileName );
1348 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1349
1350 // cleanup
1351 sat_solver_delete( pSat );
1352 Cnf_DataFree( pCnf2 );
1353 Gia_ManStop( pC );
1354 return 1;
1355 }
1356
1357 /**Function*************************************************************
1358
1359 Synopsis [Generate miter, CNF and solver.]
1360
1361 Description []
1362
1363 SideEffects []
1364
1365 SeeAlso []
1366
1367 ***********************************************************************/
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)1368 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 )
1369 {
1370 Gia_Man_t * p0 = NULL, * p1 = NULL, * pM;
1371 Gia_Obj_t * pObj;
1372 Cnf_Dat_t * pCnf;
1373 sat_solver * pSat;
1374 int i, Iter, status;
1375 abctime clkSat = 0;
1376
1377 if ( Vec_IntSize(vTests) && (Vec_IntSize(vTests) % nFuncVars != 0) )
1378 {
1379 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 );
1380 Vec_IntFree( vTests );
1381 return 0;
1382 }
1383
1384 // select algorithm
1385 if ( pPars->Algo == 0 )
1386 p1 = Gia_ManFormulaUnfold( p, pPars->pFormStr, pPars->fFfOnly );
1387 else if ( pPars->Algo == 1 )
1388 {
1389 assert( Gia_ManRegNum(p) > 0 );
1390 p0 = Gia_ManFaultUnfold( pG, 0, pPars->fFfOnly );
1391 p1 = Gia_ManFaultUnfold( p, 1, pPars->fFfOnly );
1392 }
1393 else if ( pPars->Algo == 2 )
1394 p1 = Gia_ManStuckAtUnfold( p, vMap );
1395 else if ( pPars->Algo == 3 )
1396 p1 = Gia_ManFlipUnfold( p, vMap );
1397 else if ( pPars->Algo == 4 )
1398 p1 = Gia_ManFOFUnfold( p, vMap );
1399 if ( pPars->Algo != 1 )
1400 p0 = Gia_ManDeriveDup( pG, Gia_ManCiNum(p1) - Gia_ManCiNum(pG) );
1401 // Gia_AigerWrite( p1, "newfault.aig", 0, 0, 0 );
1402 // printf( "Dumped circuit with fault parameters into file \"newfault.aig\".\n" );
1403
1404 // create miter
1405 pM = Gia_ManMiter( p0, p1, 0, 0, 0, 0, 0 );
1406 pCnf = Cnf_DeriveGiaRemapped( pM );
1407 Gia_ManStop( p0 );
1408 Gia_ManStop( p1 );
1409
1410 // start the SAT solver
1411 pSat = sat_solver_new();
1412 sat_solver_setnvars( pSat, pCnf->nVars );
1413 sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
1414 // add timeframe clauses
1415 for ( i = 0; i < pCnf->nClauses; i++ )
1416 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1417 assert( 0 );
1418
1419 // add one large OR clause
1420 Vec_IntClear( vLits );
1421 Gia_ManForEachCo( pM, pObj, i )
1422 Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
1423 sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
1424
1425 // save return data
1426 *ppMiter = pM;
1427 *ppCnf = pCnf;
1428 *ppSat = pSat;
1429
1430 // add cardinality constraint
1431 if ( pPars->fBasic )
1432 {
1433 Vec_IntClear( vLits );
1434 Gia_ManForEachPi( pM, pObj, i )
1435 if ( i >= nFuncVars )
1436 Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
1437 Cnf_AddCardinConstr( pSat, vLits );
1438 }
1439 else if ( pPars->nCardConstr )
1440 {
1441 Vec_IntClear( vLits );
1442 Gia_ManForEachPi( pM, pObj, i )
1443 if ( i >= nFuncVars )
1444 Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
1445 Cnf_AddCardinConstrGeneral( pSat, vLits, pPars->nCardConstr, !pPars->fNonStrict );
1446 }
1447
1448 // add available test-patterns
1449 if ( Vec_IntSize(vTests) > 0 )
1450 {
1451 int nTests = Vec_IntSize(vTests) / nFuncVars;
1452 assert( Vec_IntSize(vTests) % nFuncVars == 0 );
1453 if ( pPars->pFileName )
1454 printf( "Reading %d pre-computed test patterns from file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pPars->pFileName );
1455 else
1456 printf( "Reading %d pre-computed test patterns from previous rounds.\n", Vec_IntSize(vTests) / nFuncVars );
1457 for ( Iter = 0; Iter < nTests; Iter++ )
1458 {
1459 if ( fWarmUp )
1460 {
1461 abctime clk = Abc_Clock();
1462 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1463 clkSat += Abc_Clock() - clk;
1464 if ( status == l_Undef )
1465 {
1466 if ( pPars->fVerbose )
1467 printf( "\n" );
1468 printf( "Timeout reached after %d seconds and adding %d tests.\n", pPars->nTimeOut, Iter );
1469 Vec_IntShrink( vTests, Iter * nFuncVars );
1470 return 0;
1471 }
1472 if ( status == l_False )
1473 {
1474 if ( pPars->fVerbose )
1475 printf( "\n" );
1476 printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1477 Vec_IntShrink( vTests, Iter * nFuncVars );
1478 return 0;
1479 }
1480 }
1481 // get pattern
1482 Vec_IntClear( vLits );
1483 for ( i = 0; i < nFuncVars; i++ )
1484 Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter*nFuncVars + i) );
1485 if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) )
1486 {
1487 if ( pPars->fVerbose )
1488 printf( "\n" );
1489 printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1490 Vec_IntShrink( vTests, Iter * nFuncVars );
1491 return 0;
1492 }
1493 if ( pPars->fVerbose )
1494 {
1495 printf( "Iter%6d : ", Iter );
1496 printf( "Var =%10d ", sat_solver_nvars(pSat) );
1497 printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
1498 printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
1499 //Abc_PrintTime( 1, "Time", clkSat );
1500 ABC_PRTr( "Solver time", clkSat );
1501 }
1502 }
1503 }
1504 else if ( pPars->fStartPats )
1505 {
1506 for ( Iter = 0; Iter < 2; Iter++ )
1507 {
1508 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1509 if ( status == l_Undef )
1510 {
1511 if ( pPars->fVerbose )
1512 printf( "\n" );
1513 printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
1514 Vec_IntShrink( vTests, Iter * nFuncVars );
1515 return 0;
1516 }
1517 if ( status == l_False )
1518 {
1519 if ( pPars->fVerbose )
1520 printf( "\n" );
1521 printf( "The problem is UNSAT after %d iterations.\n", Iter );
1522 Vec_IntShrink( vTests, Iter * nFuncVars );
1523 return 0;
1524 }
1525 // initialize simple pattern
1526 Vec_IntFill( vLits, nFuncVars, Iter );
1527 Vec_IntAppend( vTests, vLits );
1528 if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) )
1529 {
1530 if ( pPars->fVerbose )
1531 printf( "\n" );
1532 printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1533 Vec_IntShrink( vTests, Iter * nFuncVars );
1534 return 0;
1535 }
1536 }
1537 }
1538
1539 printf( "Using miter with: AIG nodes = %6d. CNF variables = %6d. CNF clauses = %8d.\n", Gia_ManAndNum(pM), pCnf->nVars, pCnf->nClauses );
1540 return 1;
1541 }
1542
1543 /**Function*************************************************************
1544
1545 Synopsis []
1546
1547 Description []
1548
1549 SideEffects []
1550
1551 SeeAlso []
1552
1553 ***********************************************************************/
Gia_ManFaultTest(Gia_Man_t * p,Gia_Man_t * pG,Bmc_ParFf_t * pPars)1554 void Gia_ManFaultTest( Gia_Man_t * p, Gia_Man_t * pG, Bmc_ParFf_t * pPars )
1555 {
1556 int nIterMax = 1000000, nVars, nPars;
1557 int i, Iter, Iter2, status, nFuncVars = -1;
1558 abctime clk, clkSat = 0, clkTotal = Abc_Clock();
1559 Vec_Int_t * vLits, * vMap = NULL, * vTests, * vPars = NULL;
1560 Gia_Man_t * pM;
1561 Gia_Obj_t * pObj;
1562 Cnf_Dat_t * pCnf;
1563 sat_solver * pSat = NULL;
1564
1565 if ( pPars->Algo == 0 && Gia_FormStrCount( pPars->pFormStr, &nVars, &nPars ) )
1566 return;
1567
1568 // select algorithm
1569 if ( pPars->Algo == 0 )
1570 printf( "FFTEST is computing test patterns for fault model \"%s\"...\n", pPars->pFormStr );
1571 else if ( pPars->Algo == 1 )
1572 printf( "FFTEST is computing test patterns for %sdelay faults...\n", pPars->fBasic ? "single " : "" );
1573 else if ( pPars->Algo == 2 )
1574 printf( "FFTEST is computing test patterns for %sstuck-at faults...\n", pPars->fBasic ? "single " : "" );
1575 else if ( pPars->Algo == 3 )
1576 printf( "FFTEST is computing test patterns for %scomplement faults...\n", pPars->fBasic ? "single " : "" );
1577 else if ( pPars->Algo == 4 )
1578 printf( "FFTEST is computing test patterns for %sfunctionally observable faults...\n", pPars->fBasic ? "single " : "" );
1579 else
1580 {
1581 printf( "Unrecognized algorithm (%d).\n", pPars->Algo );
1582 return;
1583 }
1584
1585 printf( "Options: " );
1586 printf( "Untestable faults = %s. ", pPars->fCheckUntest || pPars->fDumpDelay ? "yes": "no" );
1587 if ( pPars->nCardConstr )
1588 printf( "Using %sstrict cardinality %d. ", pPars->fNonStrict ? "non-" : "", pPars->nCardConstr );
1589 if ( pPars->fFfOnly )
1590 printf( "Faults at FF outputs only = yes. " );
1591 if ( pPars->nTimeOut )
1592 printf( "Runtime limit = %d sec. ", pPars->nTimeOut );
1593 if ( p != pG && pG->pSpec )
1594 printf( "Golden model = %s. ", pG->pSpec );
1595 printf( "Verbose = %s. ", pPars->fVerbose ? "yes": "no" );
1596 printf( "\n" );
1597
1598 // select algorithm
1599 if ( pPars->Algo == 0 )
1600 nFuncVars = Gia_ManCiNum(p);
1601 else if ( pPars->Algo == 1 )
1602 nFuncVars = Gia_ManRegNum(p) + 2 * Gia_ManPiNum(p);
1603 else if ( pPars->Algo == 2 )
1604 nFuncVars = Gia_ManCiNum(p);
1605 else if ( pPars->Algo == 3 )
1606 nFuncVars = Gia_ManCiNum(p);
1607 else if ( pPars->Algo == 4 )
1608 nFuncVars = Gia_ManCiNum(p);
1609
1610 // collect test patterns from file
1611 if ( pPars->pFileName )
1612 vTests = Gia_ManGetTestPatterns( pPars->pFileName );
1613 else
1614 vTests = Vec_IntAlloc( 10000 );
1615 if ( vTests == NULL )
1616 return;
1617
1618 // select algorithm
1619 vMap = Vec_IntAlloc( 0 );
1620 if ( pPars->Algo == 2 )
1621 Vec_IntFill( vMap, 2 * Gia_ManAndNum(p), 1 );
1622 else if ( pPars->Algo == 3 )
1623 Vec_IntFill( vMap, Gia_ManAndNum(p), 1 );
1624 else if ( pPars->Algo == 4 )
1625 Vec_IntFill( vMap, 4 * Gia_ManAndNum(p), 1 );
1626
1627 // prepare SAT solver
1628 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
1629
1630 // add user-speicified test-vectors (if given) and create missing ones (if needed)
1631 if ( Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 1) )
1632 for ( Iter = pPars->fStartPats ? 2 : Vec_IntSize(vTests) / nFuncVars; Iter < nIterMax; Iter++ )
1633 {
1634 // collect parameter variables
1635 if ( pPars->nIterCheck && vPars == NULL )
1636 {
1637 vPars = Vec_IntAlloc( Gia_ManPiNum(pM) - nFuncVars );
1638 Gia_ManForEachPi( pM, pObj, i )
1639 if ( i >= nFuncVars )
1640 Vec_IntPush( vPars, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
1641 assert( Vec_IntSize(vPars) == Gia_ManPiNum(pM) - nFuncVars );
1642 }
1643 // derive unit parameter variables
1644 if ( Iter && pPars->nIterCheck && (Iter % pPars->nIterCheck) == 0 )
1645 {
1646 Gia_ManFaultAnalyze( pSat, vPars, vMap, vLits, Iter );
1647 // cleanup
1648 Gia_ManStop( pM );
1649 Cnf_DataFree( pCnf );
1650 sat_solver_delete( pSat );
1651 // recompute
1652 if ( !Gia_ManFaultPrepare(p, pG, pPars, nFuncVars, vMap, vTests, vLits, &pM, &pCnf, &pSat, 0) )
1653 {
1654 printf( "This should never happen.\n" );
1655 return;
1656 }
1657 Vec_IntFreeP( &vPars );
1658 }
1659 // solve
1660 clk = Abc_Clock();
1661 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1662 clkSat += Abc_Clock() - clk;
1663 if ( pPars->fVerbose )
1664 {
1665 printf( "Iter%6d : ", Iter );
1666 printf( "Var =%10d ", sat_solver_nvars(pSat) );
1667 printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
1668 printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
1669 //Abc_PrintTime( 1, "Time", clkSat );
1670 ABC_PRTr( "Solver time", clkSat );
1671 }
1672 if ( status == l_Undef )
1673 {
1674 if ( pPars->fVerbose )
1675 printf( "\n" );
1676 printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter );
1677 goto finish;
1678 }
1679 if ( status == l_False )
1680 {
1681 if ( pPars->fVerbose )
1682 printf( "\n" );
1683 printf( "The problem is UNSAT after %d iterations. ", Iter );
1684 break;
1685 }
1686 assert( status == l_True );
1687 // collect SAT assignment
1688 Vec_IntClear( vLits );
1689 Gia_ManForEachPi( pM, pObj, i )
1690 if ( i < nFuncVars )
1691 Vec_IntPush( vLits, sat_solver_var_value(pSat, pCnf->pVarNums[Gia_ObjId(pM, pObj)]) );
1692 // if the user selected to generate new faults detected by this test (vLits)
1693 // and not detected by the given test set (vTests), we compute the new faults here and quit
1694 if ( pPars->fDumpNewFaults )
1695 {
1696 if ( Vec_IntSize(vTests) == 0 )
1697 printf( "The input test patterns are not given.\n" );
1698 else
1699 Gia_ManFaultDumpNewFaults( pM, nFuncVars, vTests, vLits, pPars );
1700 goto finish_all;
1701 }
1702 Vec_IntAppend( vTests, vLits );
1703 // add constraint
1704 if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) )
1705 {
1706 if ( pPars->fVerbose )
1707 printf( "\n" );
1708 printf( "The problem is UNSAT after adding %d tests.\n", Iter );
1709 break;
1710 }
1711 }
1712 else Iter = Vec_IntSize(vTests) / nFuncVars;
1713 finish:
1714 // print results
1715 // if ( status == l_False )
1716 // Gia_ManPrintResults( p, pSat, Iter, Abc_Clock() - clkTotal );
1717 // cleanup
1718 Abc_PrintTime( 1, "Testing runtime", Abc_Clock() - clkTotal );
1719 // dump the test suite
1720 if ( pPars->fDump )
1721 {
1722 char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_tests.txt") : "tests.txt";
1723 if ( pPars->fDumpDelay && pPars->Algo == 1 )
1724 {
1725 Gia_ManDumpTestsDelay( vTests, Iter, pFileName, p );
1726 printf( "Dumping %d pairs of test patterns (total %d pattern) into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, 2*Vec_IntSize(vTests) / nFuncVars, pFileName );
1727 }
1728 else
1729 {
1730 Gia_ManDumpTests( vTests, Iter, pFileName );
1731 printf( "Dumping %d test patterns into file \"%s\".\n", Vec_IntSize(vTests) / nFuncVars, pFileName );
1732 }
1733 }
1734
1735 // compute untestable faults
1736 if ( Iter && (p != pG || pPars->fDumpUntest || pPars->fCheckUntest) )
1737 {
1738 abctime clkTotal = Abc_Clock();
1739 // restart the SAT solver
1740 sat_solver_delete( pSat );
1741 pSat = sat_solver_new();
1742 sat_solver_setnvars( pSat, pCnf->nVars );
1743 sat_solver_set_runtime_limit( pSat, pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
1744 // add timeframe clauses
1745 for ( i = 0; i < pCnf->nClauses; i++ )
1746 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
1747 assert( 0 );
1748 // add constraint to rule out no fault
1749 // if ( p == pG )
1750 {
1751 Vec_IntClear( vLits );
1752 Gia_ManForEachPi( pM, pObj, i )
1753 if ( i >= nFuncVars )
1754 Vec_IntPush( vLits, Abc_Var2Lit(pCnf->pVarNums[Gia_ObjId(pM, pObj)], 0) );
1755 sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
1756 }
1757 // add cardinality constraint
1758 if ( pPars->fBasic )
1759 {
1760 Vec_IntClear( vLits );
1761 Gia_ManForEachPi( pM, pObj, i )
1762 if ( i >= nFuncVars )
1763 Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pM, pObj)] );
1764 Cnf_AddCardinConstr( pSat, vLits );
1765 }
1766 // add output clauses
1767 Gia_ManForEachCo( pM, pObj, i )
1768 {
1769 int Lit = Abc_Var2Lit( pCnf->pVarNums[Gia_ObjId(pM, pObj)], 1 );
1770 sat_solver_addclause( pSat, &Lit, &Lit + 1 );
1771 }
1772 // simplify the SAT solver
1773 status = sat_solver_simplify( pSat );
1774 assert( status );
1775
1776 // add test patterns
1777 assert( Vec_IntSize(vTests) == Iter * nFuncVars );
1778 for ( Iter2 = 0; ; Iter2++ )
1779 {
1780 abctime clk = Abc_Clock();
1781 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
1782 clkSat += Abc_Clock() - clk;
1783 if ( pPars->fVerbose )
1784 {
1785 printf( "Iter%6d : ", Iter2 );
1786 printf( "Var =%10d ", sat_solver_nvars(pSat) );
1787 printf( "Clause =%10d ", sat_solver_nclauses(pSat) );
1788 printf( "Conflict =%10d ", sat_solver_nconflicts(pSat) );
1789 //Abc_PrintTime( 1, "Time", clkSat );
1790 ABC_PRTr( "Solver time", clkSat );
1791 }
1792 if ( status == l_Undef )
1793 {
1794 if ( pPars->fVerbose )
1795 printf( "\n" );
1796 printf( "Timeout reached after %d seconds and %d iterations.\n", pPars->nTimeOut, Iter2 );
1797 goto finish;
1798 }
1799 if ( Iter2 == Iter )
1800 break;
1801 assert( status == l_True );
1802 // get pattern
1803 Vec_IntClear( vLits );
1804 for ( i = 0; i < nFuncVars; i++ )
1805 Vec_IntPush( vLits, Vec_IntEntry(vTests, Iter2*nFuncVars + i) );
1806 if ( !Gia_ManFaultAddOne( pM, pCnf, pSat, vLits, nFuncVars, 0, pM ) )
1807 {
1808 printf( "The problem is UNSAT after adding %d tests.\n", Iter2 );
1809 goto finish;
1810 }
1811 }
1812 assert( Iter2 == Iter );
1813 if ( pPars->fVerbose )
1814 printf( "\n" );
1815 if ( p == pG )
1816 {
1817 if ( status == l_True )
1818 printf( "There are untestable faults. " );
1819 else if ( status == l_False )
1820 printf( "There is no untestable faults. " );
1821 else assert( 0 );
1822 Abc_PrintTime( 1, "Fault computation runtime", Abc_Clock() - clkTotal );
1823 }
1824 else
1825 {
1826 if ( status == l_True )
1827 printf( "The circuit is rectifiable. " );
1828 else if ( status == l_False )
1829 printf( "The circuit is not rectifiable (or equivalent to the golden one). " );
1830 else assert( 0 );
1831 Abc_PrintTime( 1, "Rectification runtime", Abc_Clock() - clkTotal );
1832 }
1833 // dump untestable faults
1834 if ( pPars->fDumpUntest && status == l_True )
1835 {
1836 abctime clk = Abc_Clock();
1837 char * pFileName = p->pSpec ? Extra_FileNameGenericAppend(p->pSpec, "_untest.txt") : "untest.txt";
1838 int nUntests = Gia_ManDumpUntests( pM, pCnf, pSat, nFuncVars, pFileName, pPars->fVerbose );
1839 if ( p == pG )
1840 printf( "Dumped %d untestable multiple faults into file \"%s\". ", nUntests, pFileName );
1841 else
1842 printf( "Dumped %d ways of rectifying the circuit into file \"%s\". ", nUntests, pFileName );
1843 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1844 }
1845 }
1846 finish_all:
1847 sat_solver_delete( pSat );
1848 Cnf_DataFree( pCnf );
1849 Gia_ManStop( pM );
1850 Vec_IntFree( vTests );
1851 Vec_IntFree( vMap );
1852 Vec_IntFree( vLits );
1853 Vec_IntFreeP( &vPars );
1854 }
1855
1856
1857
1858 ////////////////////////////////////////////////////////////////////////
1859 /// END OF FILE ///
1860 ////////////////////////////////////////////////////////////////////////
1861
1862
1863 ABC_NAMESPACE_IMPL_END
1864
1865