1 /**CFile****************************************************************
2
3 FileName [bmcICheck.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [SAT-based bounded model checking.]
8
9 Synopsis [Performs specialized check.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: bmcICheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "bmc.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satStore.h"
24 #include "aig/gia/giaAig.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 ////////////////////////////////////////////////////////////////////////
34 /// FUNCTION DEFINITIONS ///
35 ////////////////////////////////////////////////////////////////////////
36
37 /**Function*************************************************************
38
39 Synopsis []
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Cnf_DeriveGiaRemapped(Gia_Man_t * p)48 static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p )
49 {
50 Cnf_Dat_t * pCnf;
51 Aig_Man_t * pAig = Gia_ManToAigSimple( p );
52 pAig->nRegs = 0;
53 pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) );
54 Aig_ManStop( pAig );
55 return pCnf;
56 }
57
58 /**Function*************************************************************
59
60 Synopsis []
61
62 Description []
63
64 SideEffects []
65
66 SeeAlso []
67
68 ***********************************************************************/
Cnf_DataLiftGia(Cnf_Dat_t * p,Gia_Man_t * pGia,int nVarsPlus)69 static inline void Cnf_DataLiftGia( Cnf_Dat_t * p, Gia_Man_t * pGia, int nVarsPlus )
70 {
71 Gia_Obj_t * pObj;
72 int v;
73 Gia_ManForEachObj( pGia, pObj, v )
74 if ( p->pVarNums[Gia_ObjId(pGia, pObj)] >= 0 )
75 p->pVarNums[Gia_ObjId(pGia, pObj)] += nVarsPlus;
76 for ( v = 0; v < p->nLiterals; v++ )
77 p->pClauses[0][v] += 2*nVarsPlus;
78 }
79
80 /**Function*************************************************************
81
82 Synopsis []
83
84 Description []
85
86 SideEffects []
87
88 SeeAlso []
89
90 ***********************************************************************/
Bmc_DeriveSolver(Gia_Man_t * p,Gia_Man_t * pMiter,Cnf_Dat_t * pCnf,int nFramesMax,int nTimeOut,int fVerbose)91 sat_solver * Bmc_DeriveSolver( Gia_Man_t * p, Gia_Man_t * pMiter, Cnf_Dat_t * pCnf, int nFramesMax, int nTimeOut, int fVerbose )
92 {
93 sat_solver * pSat;
94 Vec_Int_t * vLits;
95 Gia_Obj_t * pObj, * pObj0, * pObj1;
96 int i, k, iVar0, iVar1, iVarOut;
97 int VarShift = 0;
98
99 // start the SAT solver
100 pSat = sat_solver_new();
101 sat_solver_setnvars( pSat, Gia_ManRegNum(p) + Gia_ManCoNum(p) + pCnf->nVars * (nFramesMax + 1) );
102 sat_solver_set_runtime_limit( pSat, nTimeOut ? nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0 );
103
104 // add one large OR clause
105 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
106 Gia_ManForEachCo( p, pObj, i )
107 Vec_IntPush( vLits, Abc_Var2Lit(Gia_ManRegNum(p) + i, 0) );
108 sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
109
110 // load the last timeframe
111 Cnf_DataLiftGia( pCnf, pMiter, Gia_ManRegNum(p) + Gia_ManCoNum(p) );
112 VarShift += Gia_ManRegNum(p) + Gia_ManCoNum(p);
113
114 // add XOR clauses
115 Gia_ManForEachPo( p, pObj, i )
116 {
117 pObj0 = Gia_ManPo( pMiter, 2*i+0 );
118 pObj1 = Gia_ManPo( pMiter, 2*i+1 );
119 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
120 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
121 iVarOut = Gia_ManRegNum(p) + i;
122 sat_solver_add_xor( pSat, iVar0, iVar1, iVarOut, 0 );
123 }
124 Gia_ManForEachRi( p, pObj, i )
125 {
126 pObj0 = Gia_ManRi( pMiter, i );
127 pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
128 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
129 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
130 iVarOut = Gia_ManRegNum(p) + Gia_ManPoNum(p) + i;
131 sat_solver_add_xor_and( pSat, iVarOut, iVar0, iVar1, i );
132 }
133 // add timeframe clauses
134 for ( i = 0; i < pCnf->nClauses; i++ )
135 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
136 assert( 0 );
137
138 // add other timeframes
139 for ( k = 0; k < nFramesMax; k++ )
140 {
141 // collect variables of the RO nodes
142 Vec_IntClear( vLits );
143 Gia_ManForEachRo( pMiter, pObj, i )
144 Vec_IntPush( vLits, pCnf->pVarNums[Gia_ObjId(pMiter, pObj)] );
145 // lift CNF again
146 Cnf_DataLiftGia( pCnf, pMiter, pCnf->nVars );
147 VarShift += pCnf->nVars;
148 // stitch the clauses
149 Gia_ManForEachRi( pMiter, pObj, i )
150 {
151 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj)];
152 iVar1 = Vec_IntEntry( vLits, i );
153 if ( iVar1 == -1 )
154 continue;
155 sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
156 }
157 // add equality clauses for the COs
158 Gia_ManForEachPo( p, pObj, i )
159 {
160 pObj0 = Gia_ManPo( pMiter, 2*i+0 );
161 pObj1 = Gia_ManPo( pMiter, 2*i+1 );
162 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
163 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
164 sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
165 }
166 Gia_ManForEachRi( p, pObj, i )
167 {
168 pObj0 = Gia_ManRi( pMiter, i );
169 pObj1 = Gia_ManRi( pMiter, i + Gia_ManRegNum(p) );
170 iVar0 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj0)];
171 iVar1 = pCnf->pVarNums[Gia_ObjId(pMiter, pObj1)];
172 sat_solver_add_buffer_enable( pSat, iVar0, iVar1, i, 0 );
173 }
174 // add timeframe clauses
175 for ( i = 0; i < pCnf->nClauses; i++ )
176 if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
177 assert( 0 );
178 }
179 // sat_solver_compress( pSat );
180 Cnf_DataLiftGia( pCnf, pMiter, -VarShift );
181 Vec_IntFree( vLits );
182 return pSat;
183 }
184
185 /**Function*************************************************************
186
187 Synopsis []
188
189 Description []
190
191 SideEffects []
192
193 SeeAlso []
194
195 ***********************************************************************/
Bmc_PerformICheck(Gia_Man_t * p,int nFramesMax,int nTimeOut,int fEmpty,int fVerbose)196 void Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose )
197 {
198 int fUseOldCnf = 0;
199 Gia_Man_t * pMiter, * pTemp;
200 Cnf_Dat_t * pCnf;
201 sat_solver * pSat;
202 Vec_Int_t * vLits, * vUsed;
203 int i, status, Lit;
204 int nLitsUsed, nLits, * pLits;
205 abctime clkStart = Abc_Clock();
206 assert( nFramesMax > 0 );
207 assert( Gia_ManRegNum(p) > 0 );
208
209 if ( fVerbose )
210 printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops:\n",
211 Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p) );
212
213 // create miter
214 pTemp = Gia_ManDup( p );
215 pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
216 Gia_ManStop( pTemp );
217 assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
218 assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
219 // derive CNF
220 if ( fUseOldCnf )
221 pCnf = Cnf_DeriveGiaRemapped( pMiter );
222 else
223 {
224 pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
225 Gia_ManStop( pTemp );
226 pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
227 }
228
229 // collect positive literals
230 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
231 for ( i = 0; i < Gia_ManRegNum(p); i++ )
232 Vec_IntPush( vLits, Abc_Var2Lit(i, fEmpty) );
233
234 // iteratively compute a minimal M-inductive set of next-state functions
235 nLitsUsed = fEmpty ? 0 : Vec_IntSize(vLits);
236 vUsed = Vec_IntAlloc( Vec_IntSize(vLits) );
237 while ( 1 )
238 {
239 int fChanges = 0;
240 // derive SAT solver
241 pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
242 // sat_solver_bookmark( pSat );
243 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
244 if ( status == l_Undef )
245 {
246 printf( "Timeout reached after %d seconds.\n", nTimeOut );
247 break;
248 }
249 if ( status == l_True )
250 {
251 printf( "The problem is satisfiable (the current set is not M-inductive).\n" );
252 break;
253 }
254 assert( status == l_False );
255 // call analize_final
256 nLits = sat_solver_final( pSat, &pLits );
257 // mark used literals
258 Vec_IntFill( vUsed, Vec_IntSize(vLits), 0 );
259 for ( i = 0; i < nLits; i++ )
260 Vec_IntWriteEntry( vUsed, Abc_Lit2Var(pLits[i]), 1 );
261
262 // check if there are any positive unused
263 Vec_IntForEachEntry( vLits, Lit, i )
264 {
265 assert( i == Abc_Lit2Var(Lit) );
266 if ( Abc_LitIsCompl(Lit) )
267 continue;
268 if ( Vec_IntEntry(vUsed, i) )
269 continue;
270 // positive literal became unused
271 Vec_IntWriteEntry( vLits, i, Abc_LitNot(Lit) );
272 nLitsUsed--;
273 fChanges = 1;
274 }
275 // report the results
276 if ( fVerbose )
277 printf( "M =%4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
278 nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
279 Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
280 sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
281 if ( fVerbose )
282 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
283 // count the number of negative literals
284 sat_solver_delete( pSat );
285 if ( !fChanges || fEmpty )
286 break;
287 // break;
288 // sat_solver_rollback( pSat );
289 }
290 Cnf_DataFree( pCnf );
291 Gia_ManStop( pMiter );
292 Vec_IntFree( vLits );
293 Vec_IntFree( vUsed );
294 }
295
296 /**Function*************************************************************
297
298 Synopsis [Collect flops starting from the POs.]
299
300 Description []
301
302 SideEffects []
303
304 SeeAlso []
305
306 ***********************************************************************/
Bmc_PerformFindFlopOrder_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vRegs)307 void Bmc_PerformFindFlopOrder_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vRegs )
308 {
309 if ( Gia_ObjIsTravIdCurrent(p, pObj) )
310 return;
311 Gia_ObjSetTravIdCurrent(p, pObj);
312 if ( Gia_ObjIsCi(pObj) )
313 {
314 if ( Gia_ObjIsRo(p, pObj) )
315 Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
316 return;
317 }
318 assert( Gia_ObjIsAnd(pObj) );
319 Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
320 Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin1(pObj), vRegs );
321 }
Bmc_PerformFindFlopOrder(Gia_Man_t * p,Vec_Int_t * vRegs)322 void Bmc_PerformFindFlopOrder( Gia_Man_t * p, Vec_Int_t * vRegs )
323 {
324 Gia_Obj_t * pObj;
325 int i, iReg, k = 0;
326 // start with POs
327 Vec_IntClear( vRegs );
328 Gia_ManForEachPo( p, pObj, i )
329 Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
330 // add flop outputs in the B
331 Gia_ManIncrementTravId( p );
332 Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) );
333 Gia_ManForEachObjVec( vRegs, p, pObj, i )
334 {
335 assert( Gia_ObjIsPo(p, pObj) || Gia_ObjIsRo(p, pObj) );
336 if ( Gia_ObjIsRo(p, pObj) )
337 pObj = Gia_ObjRoToRi( p, pObj );
338 Bmc_PerformFindFlopOrder_rec( p, Gia_ObjFanin0(pObj), vRegs );
339 }
340 // add dangling flops
341 Gia_ManForEachRo( p, pObj, i )
342 if ( !Gia_ObjIsTravIdCurrent(p, pObj) )
343 Vec_IntPush( vRegs, Gia_ObjId(p, pObj) );
344 // remove POs; keep flop outputs only; remap ObjId into CiId
345 assert( Vec_IntSize(vRegs) == Gia_ManCoNum(p) );
346 Gia_ManForEachObjVec( vRegs, p, pObj, i )
347 {
348 if ( i < Gia_ManPoNum(p) )
349 continue;
350 iReg = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
351 assert( iReg >= 0 && iReg < Gia_ManRegNum(p) );
352 Vec_IntWriteEntry( vRegs, k++, iReg );
353 }
354 Vec_IntShrink( vRegs, k );
355 assert( Vec_IntSize(vRegs) == Gia_ManRegNum(p) );
356 }
357
358
359 /**Function*************************************************************
360
361 Synopsis []
362
363 Description []
364
365 SideEffects []
366
367 SeeAlso []
368
369 ***********************************************************************/
Bmc_PerformISearchOne(Gia_Man_t * p,int nFramesMax,int nTimeOut,int fReverse,int fBackTopo,int fVerbose,Vec_Int_t * vLits)370 int Bmc_PerformISearchOne( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fVerbose, Vec_Int_t * vLits )
371 {
372 int fUseOldCnf = 0;
373 Gia_Man_t * pMiter, * pTemp;
374 Cnf_Dat_t * pCnf;
375 sat_solver * pSat;
376 Vec_Int_t * vRegs = NULL;
377 // Vec_Int_t * vLits;
378 int i, Iter, status;
379 int nLitsUsed, RetValue = 0;
380 abctime clkStart = Abc_Clock();
381 assert( nFramesMax > 0 );
382 assert( Gia_ManRegNum(p) > 0 );
383
384 // create miter
385 pTemp = Gia_ManDup( p );
386 pMiter = Gia_ManMiter( p, pTemp, 0, 1, 1, 0, 0 );
387 Gia_ManStop( pTemp );
388 assert( Gia_ManPoNum(pMiter) == 2 * Gia_ManPoNum(p) );
389 assert( Gia_ManRegNum(pMiter) == 2 * Gia_ManRegNum(p) );
390 // derive CNF
391 if ( fUseOldCnf )
392 pCnf = Cnf_DeriveGiaRemapped( pMiter );
393 else
394 {
395 //pMiter = Jf_ManDeriveCnf( pTemp = pMiter, 0 );
396 //Gia_ManStop( pTemp );
397 //pCnf = (Cnf_Dat_t *)pMiter->pData; pMiter->pData = NULL;
398 pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pMiter, 8, 0, 0, 0, 0 );
399 }
400 /*
401 // collect positive literals
402 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
403 for ( i = 0; i < Gia_ManRegNum(p); i++ )
404 Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
405 */
406 // derive SAT solver
407 pSat = Bmc_DeriveSolver( p, pMiter, pCnf, nFramesMax, nTimeOut, fVerbose );
408 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
409 if ( status == l_True )
410 {
411 printf( "I = %4d : ", nFramesMax );
412 printf( "Problem is satisfiable.\n" );
413 sat_solver_delete( pSat );
414 Cnf_DataFree( pCnf );
415 Gia_ManStop( pMiter );
416 return 1;
417 }
418 if ( status == l_Undef )
419 {
420 printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
421 RetValue = 1;
422 goto cleanup;
423 }
424 assert( status == l_False );
425
426 // count the number of positive literals
427 nLitsUsed = 0;
428 for ( i = 0; i < Gia_ManRegNum(p); i++ )
429 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
430 nLitsUsed++;
431
432 // try removing variables
433 vRegs = Vec_IntStartNatural( Gia_ManRegNum(p) );
434 if ( fBackTopo )
435 Bmc_PerformFindFlopOrder( p, vRegs );
436 if ( fReverse )
437 Vec_IntReverseOrder( vRegs );
438 // for ( Iter = 0; Iter < Gia_ManRegNum(p); Iter++ )
439 Vec_IntForEachEntry( vRegs, i, Iter )
440 {
441 // i = fReverse ? Gia_ManRegNum(p) - 1 - Iter : Iter;
442 if ( Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
443 continue;
444 Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
445 status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
446 if ( status == l_Undef )
447 {
448 printf( "ICheck: Timeout reached after %d seconds. \n", nTimeOut );
449 RetValue = 1;
450 goto cleanup;
451 }
452 if ( status == l_True )
453 Vec_IntWriteEntry( vLits, i, Abc_LitNot(Vec_IntEntry(vLits, i)) );
454 else if ( status == l_False )
455 nLitsUsed--;
456 else assert( 0 );
457 // report the results
458 //printf( "Round %d: ", o );
459 if ( fVerbose )
460 {
461 printf( "I = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
462 i, (nFramesMax+1) * Gia_ManAndNum(pMiter),
463 Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
464 sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
465 ABC_PRTr( "Time", Abc_Clock() - clkStart );
466 fflush( stdout );
467 }
468 }
469 // report the results
470 //printf( "Round %d: ", o );
471 if ( fVerbose )
472 {
473 printf( "M = %4d : AIG =%8d. SAT vars =%8d. SAT conf =%8d. S =%6d. (%6.2f %%) ",
474 nFramesMax, (nFramesMax+1) * Gia_ManAndNum(pMiter),
475 Gia_ManRegNum(p) + Gia_ManCoNum(p) + sat_solver_nvars(pSat),
476 sat_solver_nconflicts(pSat), nLitsUsed, 100.0 * nLitsUsed / Gia_ManRegNum(p) );
477 Abc_PrintTime( 1, "Time", Abc_Clock() - clkStart );
478 fflush( stdout );
479 }
480 cleanup:
481 // cleanup
482 sat_solver_delete( pSat );
483 Cnf_DataFree( pCnf );
484 Gia_ManStop( pMiter );
485 Vec_IntFree( vRegs );
486 // Vec_IntFree( vLits );
487 return RetValue;
488 }
Bmc_PerformISearch(Gia_Man_t * p,int nFramesMax,int nTimeOut,int fReverse,int fBackTopo,int fDump,int fVerbose)489 Vec_Int_t * Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fBackTopo, int fDump, int fVerbose )
490 {
491 Vec_Int_t * vLits, * vFlops;
492 int i, f;
493 if ( fVerbose )
494 printf( "Solving M-inductiveness for design %s with %d AND nodes and %d flip-flops with %s %s flop order:\n",
495 Gia_ManName(p), Gia_ManAndNum(p), Gia_ManRegNum(p), fReverse ? "reverse":"direct", fBackTopo ? "backward":"natural" );
496 fflush( stdout );
497
498 // collect positive literals
499 vLits = Vec_IntAlloc( Gia_ManCoNum(p) );
500 for ( i = 0; i < Gia_ManRegNum(p); i++ )
501 Vec_IntPush( vLits, Abc_Var2Lit(i, 0) );
502
503 for ( f = 1; f <= nFramesMax; f++ )
504 if ( Bmc_PerformISearchOne( p, f, nTimeOut, fReverse, fBackTopo, fVerbose, vLits ) )
505 {
506 Vec_IntFree( vLits );
507 return NULL;
508 }
509
510 // dump the numbers of the flops
511 if ( fDump )
512 {
513 int nLitsUsed = 0;
514 for ( i = 0; i < Gia_ManRegNum(p); i++ )
515 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
516 nLitsUsed++;
517 printf( "The set contains %d (out of %d) next-state functions with 0-based numbers:\n", nLitsUsed, Gia_ManRegNum(p) );
518 for ( i = 0; i < Gia_ManRegNum(p); i++ )
519 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
520 printf( "%d ", i );
521 printf( "\n" );
522 }
523 // save flop indexes
524 vFlops = Vec_IntAlloc( Gia_ManRegNum(p) );
525 for ( i = 0; i < Gia_ManRegNum(p); i++ )
526 if ( !Abc_LitIsCompl(Vec_IntEntry(vLits, i)) )
527 Vec_IntPush( vFlops, 1 );
528 else
529 Vec_IntPush( vFlops, 0 );
530 Vec_IntFree( vLits );
531 return vFlops;
532 }
533
534 ////////////////////////////////////////////////////////////////////////
535 /// END OF FILE ///
536 ////////////////////////////////////////////////////////////////////////
537
538
539 ABC_NAMESPACE_IMPL_END
540
541