1 /**CFile****************************************************************
2
3 FileName [fraCec.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [CEC engined based on fraiging.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22 #include "sat/cnf/cnf.h"
23 #include "sat/bsat/satSolver2.h"
24
25 ABC_NAMESPACE_IMPL_START
26
27
28 ////////////////////////////////////////////////////////////////////////
29 /// DECLARATIONS ///
30 ////////////////////////////////////////////////////////////////////////
31
32 ////////////////////////////////////////////////////////////////////////
33 /// FUNCTION DEFINITIONS ///
34 ////////////////////////////////////////////////////////////////////////
35
36 /**Function*************************************************************
37
38 Synopsis []
39
40 Description []
41
42 SideEffects []
43
44 SeeAlso []
45
46 ***********************************************************************/
Fra_FraigSat(Aig_Man_t * pMan,ABC_INT64_T nConfLimit,ABC_INT64_T nInsLimit,int nLearnedStart,int nLearnedDelta,int nLearnedPerce,int fFlipBits,int fAndOuts,int fNewSolver,int fVerbose)47 int Fra_FraigSat( Aig_Man_t * pMan, ABC_INT64_T nConfLimit, ABC_INT64_T nInsLimit, int nLearnedStart, int nLearnedDelta, int nLearnedPerce, int fFlipBits, int fAndOuts, int fNewSolver, int fVerbose )
48 {
49 if ( fNewSolver )
50 {
51 extern void * Cnf_DataWriteIntoSolver2( Cnf_Dat_t * p, int nFrames, int fInit );
52 extern int Cnf_DataWriteOrClause2( void * pSat, Cnf_Dat_t * pCnf );
53
54 sat_solver2 * pSat;
55 Cnf_Dat_t * pCnf;
56 int status, RetValue = 0;
57 abctime clk = Abc_Clock();
58 Vec_Int_t * vCiIds;
59
60 assert( Aig_ManRegNum(pMan) == 0 );
61 pMan->pData = NULL;
62
63 // derive CNF
64 pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
65 // pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
66
67 if ( fFlipBits )
68 Cnf_DataTranformPolarity( pCnf, 0 );
69
70 if ( fVerbose )
71 {
72 printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
73 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
74 }
75
76 // convert into SAT solver
77 pSat = (sat_solver2 *)Cnf_DataWriteIntoSolver2( pCnf, 1, 0 );
78 if ( pSat == NULL )
79 {
80 Cnf_DataFree( pCnf );
81 return 1;
82 }
83
84 if ( fAndOuts )
85 {
86 // assert each output independently
87 if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
88 {
89 sat_solver2_delete( pSat );
90 Cnf_DataFree( pCnf );
91 return 1;
92 }
93 }
94 else
95 {
96 // add the OR clause for the outputs
97 if ( !Cnf_DataWriteOrClause2( pSat, pCnf ) )
98 {
99 sat_solver2_delete( pSat );
100 Cnf_DataFree( pCnf );
101 return 1;
102 }
103 }
104 vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
105 Cnf_DataFree( pCnf );
106
107
108 printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
109 ABC_PRT( "Time", Abc_Clock() - clk );
110
111 // simplify the problem
112 clk = Abc_Clock();
113 status = sat_solver2_simplify(pSat);
114 // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver2_nvars(pSat), sat_solver2_nclauses(pSat) );
115 // ABC_PRT( "Time", Abc_Clock() - clk );
116 if ( status == 0 )
117 {
118 Vec_IntFree( vCiIds );
119 sat_solver2_delete( pSat );
120 // printf( "The problem is UNSATISFIABLE after simplification.\n" );
121 return 1;
122 }
123
124 // solve the miter
125 clk = Abc_Clock();
126 if ( fVerbose )
127 pSat->verbosity = 1;
128 status = sat_solver2_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
129 if ( status == l_Undef )
130 {
131 // printf( "The problem timed out.\n" );
132 RetValue = -1;
133 }
134 else if ( status == l_True )
135 {
136 // printf( "The problem is SATISFIABLE.\n" );
137 RetValue = 0;
138 }
139 else if ( status == l_False )
140 {
141 // printf( "The problem is UNSATISFIABLE.\n" );
142 RetValue = 1;
143 }
144 else
145 assert( 0 );
146
147 // Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts );
148 // Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
149
150 // if the problem is SAT, get the counterexample
151 if ( status == l_True )
152 {
153 pMan->pData = Sat_Solver2GetModel( pSat, vCiIds->pArray, vCiIds->nSize );
154 }
155 // free the sat_solver2
156 if ( fVerbose )
157 Sat_Solver2PrintStats( stdout, pSat );
158 //sat_solver2_store_write( pSat, "trace.cnf" );
159 //sat_solver2_store_free( pSat );
160 sat_solver2_delete( pSat );
161 Vec_IntFree( vCiIds );
162 return RetValue;
163 }
164 else
165 {
166 sat_solver * pSat;
167 Cnf_Dat_t * pCnf;
168 int status, RetValue = 0;
169 abctime clk = Abc_Clock();
170 Vec_Int_t * vCiIds;
171
172 assert( Aig_ManRegNum(pMan) == 0 );
173 pMan->pData = NULL;
174
175 // derive CNF
176 pCnf = Cnf_Derive( pMan, Aig_ManCoNum(pMan) );
177 // pCnf = Cnf_DeriveSimple( pMan, Aig_ManCoNum(pMan) );
178
179 if ( fFlipBits )
180 Cnf_DataTranformPolarity( pCnf, 0 );
181
182 if ( fVerbose )
183 {
184 printf( "CNF stats: Vars = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
185 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
186 }
187
188 // convert into SAT solver
189 pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
190 if ( pSat == NULL )
191 {
192 Cnf_DataFree( pCnf );
193 return 1;
194 }
195
196 if ( nLearnedStart )
197 pSat->nLearntStart = pSat->nLearntMax = nLearnedStart;
198 if ( nLearnedDelta )
199 pSat->nLearntDelta = nLearnedDelta;
200 if ( nLearnedPerce )
201 pSat->nLearntRatio = nLearnedPerce;
202 if ( fVerbose )
203 pSat->fVerbose = fVerbose;
204
205 if ( fAndOuts )
206 {
207 // assert each output independently
208 if ( !Cnf_DataWriteAndClauses( pSat, pCnf ) )
209 {
210 sat_solver_delete( pSat );
211 Cnf_DataFree( pCnf );
212 return 1;
213 }
214 }
215 else
216 {
217 // add the OR clause for the outputs
218 if ( !Cnf_DataWriteOrClause( pSat, pCnf ) )
219 {
220 sat_solver_delete( pSat );
221 Cnf_DataFree( pCnf );
222 return 1;
223 }
224 }
225 vCiIds = Cnf_DataCollectPiSatNums( pCnf, pMan );
226 Cnf_DataFree( pCnf );
227
228
229 // printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
230 // ABC_PRT( "Time", Abc_Clock() - clk );
231
232 // simplify the problem
233 clk = Abc_Clock();
234 status = sat_solver_simplify(pSat);
235 // printf( "Simplified the problem to %d variables and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
236 // ABC_PRT( "Time", Abc_Clock() - clk );
237 if ( status == 0 )
238 {
239 Vec_IntFree( vCiIds );
240 sat_solver_delete( pSat );
241 // printf( "The problem is UNSATISFIABLE after simplification.\n" );
242 return 1;
243 }
244
245 // solve the miter
246 clk = Abc_Clock();
247 // if ( fVerbose )
248 // pSat->verbosity = 1;
249 status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)nInsLimit, (ABC_INT64_T)0, (ABC_INT64_T)0 );
250 if ( status == l_Undef )
251 {
252 // printf( "The problem timed out.\n" );
253 RetValue = -1;
254 }
255 else if ( status == l_True )
256 {
257 // printf( "The problem is SATISFIABLE.\n" );
258 RetValue = 0;
259 }
260 else if ( status == l_False )
261 {
262 // printf( "The problem is UNSATISFIABLE.\n" );
263 RetValue = 1;
264 }
265 else
266 assert( 0 );
267
268 // Abc_Print( 1, "The number of conflicts = %6d. ", (int)pSat->stats.conflicts );
269 // Abc_PrintTime( 1, "Solving time", Abc_Clock() - clk );
270
271 // if the problem is SAT, get the counterexample
272 if ( status == l_True )
273 {
274 pMan->pData = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
275 }
276 // free the sat_solver
277 if ( fVerbose )
278 Sat_SolverPrintStats( stdout, pSat );
279 //sat_solver_store_write( pSat, "trace.cnf" );
280 //sat_solver_store_free( pSat );
281 sat_solver_delete( pSat );
282 Vec_IntFree( vCiIds );
283 return RetValue;
284 }
285 }
286
287 /**Function*************************************************************
288
289 Synopsis [Recognizes what nodes are inputs of the EXOR.]
290
291 Description []
292
293 SideEffects []
294
295 SeeAlso []
296
297 ***********************************************************************/
Aig_ManCountXors(Aig_Man_t * p)298 int Aig_ManCountXors( Aig_Man_t * p )
299 {
300 Aig_Obj_t * pObj, * pFan0, * pFan1;
301 int i, Counter = 0;
302 Aig_ManForEachNode( p, pObj, i )
303 if ( Aig_ObjIsMuxType(pObj) && Aig_ObjRecognizeExor(pObj, &pFan0, &pFan1) )
304 Counter++;
305 return Counter;
306
307 }
308
309 /**Function*************************************************************
310
311 Synopsis []
312
313 Description []
314
315 SideEffects []
316
317 SeeAlso []
318
319 ***********************************************************************/
Fra_FraigCec(Aig_Man_t ** ppAig,int nConfLimit,int fVerbose)320 int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose )
321 {
322 int nBTLimitStart = 300; // starting SAT run
323 int nBTLimitFirst = 2; // first fraiging iteration
324 int nBTLimitLast = nConfLimit; // the last-gasp SAT run
325
326 Fra_Par_t Params, * pParams = &Params;
327 Aig_Man_t * pAig = *ppAig, * pTemp;
328 int i, RetValue;
329 abctime clk;
330
331 // report the original miter
332 if ( fVerbose )
333 {
334 printf( "Original miter: Nodes = %6d.\n", Aig_ManNodeNum(pAig) );
335 }
336 RetValue = Fra_FraigMiterStatus( pAig );
337 // assert( RetValue == -1 );
338 if ( RetValue == 0 )
339 {
340 pAig->pData = ABC_ALLOC( int, Aig_ManCiNum(pAig) );
341 memset( pAig->pData, 0, sizeof(int) * Aig_ManCiNum(pAig) );
342 return RetValue;
343 }
344
345 // if SAT only, solve without iteration
346 clk = Abc_Clock();
347 RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)2*nBTLimitStart, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
348 if ( fVerbose )
349 {
350 printf( "Initial SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
351 ABC_PRT( "Time", Abc_Clock() - clk );
352 }
353 if ( RetValue >= 0 )
354 return RetValue;
355
356 // duplicate the AIG
357 clk = Abc_Clock();
358 pAig = Dar_ManRwsat( pTemp = pAig, 1, 0 );
359 Aig_ManStop( pTemp );
360 if ( fVerbose )
361 {
362 printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
363 ABC_PRT( "Time", Abc_Clock() - clk );
364 }
365
366 // perform the loop
367 Fra_ParamsDefault( pParams );
368 pParams->nBTLimitNode = nBTLimitFirst;
369 pParams->nBTLimitMiter = nBTLimitStart;
370 pParams->fDontShowBar = 1;
371 pParams->fProve = 1;
372 for ( i = 0; i < 6; i++ )
373 {
374 //printf( "Running fraiging with %d BTnode and %d BTmiter.\n", pParams->nBTLimitNode, pParams->nBTLimitMiter );
375 // try XOR balancing
376 if ( Aig_ManCountXors(pAig) * 30 > Aig_ManNodeNum(pAig) + 300 )
377 {
378 clk = Abc_Clock();
379 pAig = Dar_ManBalanceXor( pTemp = pAig, 1, 0, 0 );
380 Aig_ManStop( pTemp );
381 if ( fVerbose )
382 {
383 printf( "Balance-X: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
384 ABC_PRT( "Time", Abc_Clock() - clk );
385 }
386 }
387
388 // run fraiging
389 clk = Abc_Clock();
390 pAig = Fra_FraigPerform( pTemp = pAig, pParams );
391 Aig_ManStop( pTemp );
392 if ( fVerbose )
393 {
394 printf( "Fraiging (i=%d): Nodes = %6d. ", i+1, Aig_ManNodeNum(pAig) );
395 ABC_PRT( "Time", Abc_Clock() - clk );
396 }
397
398 // check the miter status
399 RetValue = Fra_FraigMiterStatus( pAig );
400 if ( RetValue >= 0 )
401 break;
402
403 // perform rewriting
404 clk = Abc_Clock();
405 pAig = Dar_ManRewriteDefault( pTemp = pAig );
406 Aig_ManStop( pTemp );
407 if ( fVerbose )
408 {
409 printf( "Rewriting: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
410 ABC_PRT( "Time", Abc_Clock() - clk );
411 }
412
413 // check the miter status
414 RetValue = Fra_FraigMiterStatus( pAig );
415 if ( RetValue >= 0 )
416 break;
417 // try simulation
418
419 // set the parameters for the next run
420 pParams->nBTLimitNode = 8 * pParams->nBTLimitNode;
421 pParams->nBTLimitMiter = 2 * pParams->nBTLimitMiter;
422 }
423
424 // if still unsolved try last gasp
425 if ( RetValue == -1 )
426 {
427 clk = Abc_Clock();
428 RetValue = Fra_FraigSat( pAig, (ABC_INT64_T)nBTLimitLast, (ABC_INT64_T)0, 0, 0, 0, 1, 0, 0, 0 );
429 if ( fVerbose )
430 {
431 printf( "Final SAT: Nodes = %6d. ", Aig_ManNodeNum(pAig) );
432 ABC_PRT( "Time", Abc_Clock() - clk );
433 }
434 }
435
436 *ppAig = pAig;
437 return RetValue;
438 }
439
440 /**Function*************************************************************
441
442 Synopsis []
443
444 Description []
445
446 SideEffects []
447
448 SeeAlso []
449
450 ***********************************************************************/
Fra_FraigCecPartitioned(Aig_Man_t * pMan1,Aig_Man_t * pMan2,int nConfLimit,int nPartSize,int fSmart,int fVerbose)451 int Fra_FraigCecPartitioned( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
452 {
453 Aig_Man_t * pAig;
454 Vec_Ptr_t * vParts;
455 int i, RetValue = 1, nOutputs;
456 // create partitions
457 vParts = Aig_ManMiterPartitioned( pMan1, pMan2, nPartSize, fSmart );
458 // solve the partitions
459 nOutputs = -1;
460 Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
461 {
462 nOutputs++;
463 if ( fVerbose )
464 {
465 printf( "Verifying part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r",
466 i+1, Vec_PtrSize(vParts), Aig_ManCiNum(pAig), Aig_ManCoNum(pAig),
467 Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
468 fflush( stdout );
469 }
470 RetValue = Fra_FraigMiterStatus( pAig );
471 if ( RetValue == 1 )
472 continue;
473 if ( RetValue == 0 )
474 break;
475 RetValue = Fra_FraigCec( &pAig, nConfLimit, 0 );
476 Vec_PtrWriteEntry( vParts, i, pAig );
477 if ( RetValue == 1 )
478 continue;
479 if ( RetValue == 0 )
480 break;
481 break;
482 }
483 // clear the result
484 if ( fVerbose )
485 {
486 printf( " \r" );
487 fflush( stdout );
488 }
489 // report the timeout
490 if ( RetValue == -1 )
491 {
492 printf( "Timed out after verifying %d partitions (out of %d).\n", nOutputs, Vec_PtrSize(vParts) );
493 fflush( stdout );
494 }
495 // free intermediate results
496 Vec_PtrForEachEntry( Aig_Man_t *, vParts, pAig, i )
497 Aig_ManStop( pAig );
498 Vec_PtrFree( vParts );
499 return RetValue;
500 }
501
502 /**Function*************************************************************
503
504 Synopsis []
505
506 Description []
507
508 SideEffects []
509
510 SeeAlso []
511
512 ***********************************************************************/
Fra_FraigCecTop(Aig_Man_t * pMan1,Aig_Man_t * pMan2,int nConfLimit,int nPartSize,int fSmart,int fVerbose)513 int Fra_FraigCecTop( Aig_Man_t * pMan1, Aig_Man_t * pMan2, int nConfLimit, int nPartSize, int fSmart, int fVerbose )
514 {
515 Aig_Man_t * pTemp;
516 //Abc_NtkDarCec( pNtk1, pNtk2, fPartition, fVerbose );
517 int RetValue;
518 abctime clkTotal = Abc_Clock();
519
520 if ( Aig_ManCiNum(pMan1) != Aig_ManCiNum(pMan1) )
521 {
522 printf( "Abc_CommandAbc8Cec(): Miters have different number of PIs.\n" );
523 return 0;
524 }
525 if ( Aig_ManCoNum(pMan1) != Aig_ManCoNum(pMan1) )
526 {
527 printf( "Abc_CommandAbc8Cec(): Miters have different number of POs.\n" );
528 return 0;
529 }
530 assert( Aig_ManCiNum(pMan1) == Aig_ManCiNum(pMan1) );
531 assert( Aig_ManCoNum(pMan1) == Aig_ManCoNum(pMan1) );
532
533 // make sure that the first miter has more nodes
534 if ( Aig_ManNodeNum(pMan1) < Aig_ManNodeNum(pMan2) )
535 {
536 pTemp = pMan1;
537 pMan1 = pMan2;
538 pMan2 = pTemp;
539 }
540 assert( Aig_ManNodeNum(pMan1) >= Aig_ManNodeNum(pMan2) );
541
542 if ( nPartSize )
543 RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, nPartSize, fSmart, fVerbose );
544 else // no partitioning
545 RetValue = Fra_FraigCecPartitioned( pMan1, pMan2, nConfLimit, Aig_ManCoNum(pMan1), 0, fVerbose );
546
547 // report the miter
548 if ( RetValue == 1 )
549 {
550 printf( "Networks are equivalent. " );
551 ABC_PRT( "Time", Abc_Clock() - clkTotal );
552 }
553 else if ( RetValue == 0 )
554 {
555 printf( "Networks are NOT EQUIVALENT. " );
556 ABC_PRT( "Time", Abc_Clock() - clkTotal );
557 }
558 else
559 {
560 printf( "Networks are UNDECIDED. " );
561 ABC_PRT( "Time", Abc_Clock() - clkTotal );
562 }
563 fflush( stdout );
564 return RetValue;
565 }
566
567
568 ////////////////////////////////////////////////////////////////////////
569 /// END OF FILE ///
570 ////////////////////////////////////////////////////////////////////////
571
572
573 ABC_NAMESPACE_IMPL_END
574
575