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