1 /**CFile****************************************************************
2
3 FileName [fraInd.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Inductive prover.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraInd.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 "opt/dar/dar.h"
24 #include "aig/saig/saig.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 [Performs AIG rewriting on the constraint manager.]
40
41 Description []
42
43 SideEffects []
44
45 SeeAlso []
46
47 ***********************************************************************/
Fra_FraigInductionRewrite(Fra_Man_t * p)48 void Fra_FraigInductionRewrite( Fra_Man_t * p )
49 {
50 Aig_Man_t * pTemp;
51 Aig_Obj_t * pObj, * pObjPo;
52 int nTruePis, k, i;
53 abctime clk = Abc_Clock();
54 // perform AIG rewriting on the speculated frames
55 // pTemp = Dar_ManRwsat( pTemp, 1, 0 );
56 pTemp = Dar_ManRewriteDefault( p->pManFraig );
57 // printf( "Before = %6d. After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) );
58 //Aig_ManDumpBlif( p->pManFraig, "1.blif", NULL, NULL );
59 //Aig_ManDumpBlif( pTemp, "2.blif", NULL, NULL );
60 // Fra_FramesWriteCone( pTemp );
61 // Aig_ManStop( pTemp );
62 // transfer PI/register pointers
63 assert( p->pManFraig->nRegs == pTemp->nRegs );
64 assert( p->pManFraig->nAsserts == pTemp->nAsserts );
65 nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
66 memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
67 Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
68 Aig_ManForEachPiSeq( p->pManAig, pObj, i )
69 Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManCi(pTemp,nTruePis*p->pPars->nFramesK+i) );
70 k = 0;
71 assert( Aig_ManRegNum(p->pManAig) == Aig_ManCoNum(pTemp) - pTemp->nAsserts );
72 Aig_ManForEachLoSeq( p->pManAig, pObj, i )
73 {
74 pObjPo = Aig_ManCo(pTemp, pTemp->nAsserts + k++);
75 Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
76 }
77 // exchange
78 Aig_ManStop( p->pManFraig );
79 p->pManFraig = pTemp;
80 p->timeRwr += Abc_Clock() - clk;
81 }
82
83 /**Function*************************************************************
84
85 Synopsis [Performs speculative reduction for one node.]
86
87 Description []
88
89 SideEffects []
90
91 SeeAlso []
92
93 ***********************************************************************/
Fra_FramesConstrainNode(Aig_Man_t * pManFraig,Aig_Obj_t * pObj,int iFrame)94 static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
95 {
96 Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
97 // skip nodes without representative
98 if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
99 return;
100 assert( pObjRepr->Id < pObj->Id );
101 // get the new node
102 pObjNew = Fra_ObjFraig( pObj, iFrame );
103 // get the new node of the representative
104 pObjReprNew = Fra_ObjFraig( pObjRepr, iFrame );
105 // if this is the same node, no need to add constraints
106 if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
107 return;
108 // these are different nodes - perform speculative reduction
109 pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
110 // set the new node
111 Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
112 // add the constraint
113 pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
114 pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
115 assert( Aig_ObjPhaseReal(pMiter) == 1 );
116 Aig_ObjCreateCo( pManFraig, pMiter );
117 }
118
119 /**Function*************************************************************
120
121 Synopsis [Prepares the inductive case with speculative reduction.]
122
123 Description []
124
125 SideEffects []
126
127 SeeAlso []
128
129 ***********************************************************************/
Fra_FramesWithClasses(Fra_Man_t * p)130 Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
131 {
132 Aig_Man_t * pManFraig;
133 Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
134 int i, k, f;
135 assert( p->pManFraig == NULL );
136 assert( Aig_ManRegNum(p->pManAig) > 0 );
137 assert( Aig_ManRegNum(p->pManAig) < Aig_ManCiNum(p->pManAig) );
138
139 // start the fraig package
140 pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
141 pManFraig->pName = Abc_UtilStrsav( p->pManAig->pName );
142 pManFraig->pSpec = Abc_UtilStrsav( p->pManAig->pSpec );
143 pManFraig->nRegs = p->pManAig->nRegs;
144 // create PI nodes for the frames
145 for ( f = 0; f < p->nFramesAll; f++ )
146 Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
147 for ( f = 0; f < p->nFramesAll; f++ )
148 Aig_ManForEachPiSeq( p->pManAig, pObj, i )
149 Fra_ObjSetFraig( pObj, f, Aig_ObjCreateCi(pManFraig) );
150 // create latches for the first frame
151 Aig_ManForEachLoSeq( p->pManAig, pObj, i )
152 Fra_ObjSetFraig( pObj, 0, Aig_ObjCreateCi(pManFraig) );
153
154 // add timeframes
155 // pManFraig->fAddStrash = 1;
156 for ( f = 0; f < p->nFramesAll - 1; f++ )
157 {
158 // set the constraints on the latch outputs
159 Aig_ManForEachLoSeq( p->pManAig, pObj, i )
160 Fra_FramesConstrainNode( pManFraig, pObj, f );
161 // add internal nodes of this frame
162 Aig_ManForEachNode( p->pManAig, pObj, i )
163 {
164 pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
165 Fra_ObjSetFraig( pObj, f, pObjNew );
166 Fra_FramesConstrainNode( pManFraig, pObj, f );
167 }
168 // transfer latch input to the latch outputs
169 Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
170 Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
171 }
172 // pManFraig->fAddStrash = 0;
173 // mark the asserts
174 pManFraig->nAsserts = Aig_ManCoNum(pManFraig);
175 // add the POs for the latch outputs of the last frame
176 Aig_ManForEachLoSeq( p->pManAig, pObj, i )
177 Aig_ObjCreateCo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
178
179 // remove dangling nodes
180 Aig_ManCleanup( pManFraig );
181 // make sure the satisfying assignment is node assigned
182 assert( pManFraig->pData == NULL );
183 return pManFraig;
184 }
185
186 /**Function*************************************************************
187
188 Synopsis [Prepares the inductive case with speculative reduction.]
189
190 Description []
191
192 SideEffects []
193
194 SeeAlso []
195
196 ***********************************************************************/
Fra_FramesAddMore(Aig_Man_t * p,int nFrames)197 void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
198 {
199 Aig_Obj_t * pObj, ** pLatches;
200 int i, k, f, nNodesOld;
201 // set copy pointer of each object to point to itself
202 Aig_ManForEachObj( p, pObj, i )
203 pObj->pData = pObj;
204 // iterate and add objects
205 nNodesOld = Aig_ManObjNumMax(p);
206 pLatches = ABC_ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
207 for ( f = 0; f < nFrames; f++ )
208 {
209 // clean latch inputs and outputs
210 Aig_ManForEachLiSeq( p, pObj, i )
211 pObj->pData = NULL;
212 Aig_ManForEachLoSeq( p, pObj, i )
213 pObj->pData = NULL;
214 // save the latch input values
215 k = 0;
216 Aig_ManForEachLiSeq( p, pObj, i )
217 {
218 if ( Aig_ObjFanin0(pObj)->pData )
219 pLatches[k++] = Aig_ObjChild0Copy(pObj);
220 else
221 pLatches[k++] = NULL;
222 }
223 // insert them as the latch output values
224 k = 0;
225 Aig_ManForEachLoSeq( p, pObj, i )
226 pObj->pData = pLatches[k++];
227 // create the next time frame of nodes
228 Aig_ManForEachNode( p, pObj, i )
229 {
230 if ( i > nNodesOld )
231 break;
232 if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
233 pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
234 else
235 pObj->pData = NULL;
236 }
237 }
238 ABC_FREE( pLatches );
239 }
240
241
242 /**Function*************************************************************
243
244 Synopsis [Performs partitioned sequential SAT sweepingG.]
245
246 Description []
247
248 SideEffects []
249
250 SeeAlso []
251
252 ***********************************************************************/
Fra_FraigInductionPart(Aig_Man_t * pAig,Fra_Ssw_t * pPars)253 Aig_Man_t * Fra_FraigInductionPart( Aig_Man_t * pAig, Fra_Ssw_t * pPars )
254 {
255 int fPrintParts = 0;
256 char Buffer[100];
257 Aig_Man_t * pTemp, * pNew;
258 Vec_Ptr_t * vResult;
259 Vec_Int_t * vPart;
260 int * pMapBack;
261 int i, nCountPis, nCountRegs;
262 int nClasses, nPartSize, fVerbose;
263 abctime clk = Abc_Clock();
264
265 // save parameters
266 nPartSize = pPars->nPartSize; pPars->nPartSize = 0;
267 fVerbose = pPars->fVerbose; pPars->fVerbose = 0;
268 // generate partitions
269 if ( pAig->vClockDoms )
270 {
271 // divide large clock domains into separate partitions
272 vResult = Vec_PtrAlloc( 100 );
273 Vec_PtrForEachEntry( Vec_Int_t *, (Vec_Ptr_t *)pAig->vClockDoms, vPart, i )
274 {
275 if ( nPartSize && Vec_IntSize(vPart) > nPartSize )
276 Aig_ManPartDivide( vResult, vPart, nPartSize, pPars->nOverSize );
277 else
278 Vec_PtrPush( vResult, Vec_IntDup(vPart) );
279 }
280 }
281 else
282 vResult = Aig_ManRegPartitionSimple( pAig, nPartSize, pPars->nOverSize );
283 // vResult = Aig_ManPartitionSmartRegisters( pAig, nPartSize, 0 );
284 // vResult = Aig_ManRegPartitionSmart( pAig, nPartSize );
285 if ( fPrintParts )
286 {
287 // print partitions
288 printf( "Simple partitioning. %d partitions are saved:\n", Vec_PtrSize(vResult) );
289 Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
290 {
291 sprintf( Buffer, "part%03d.aig", i );
292 pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, NULL );
293 Ioa_WriteAiger( pTemp, Buffer, 0, 0 );
294 printf( "part%03d.aig : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d.\n",
295 i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp) );
296 Aig_ManStop( pTemp );
297 }
298 }
299
300 // perform SSW with partitions
301 Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) );
302 Vec_PtrForEachEntry( Vec_Int_t *, vResult, vPart, i )
303 {
304 pTemp = Aig_ManRegCreatePart( pAig, vPart, &nCountPis, &nCountRegs, &pMapBack );
305 // create the projection of 1-hot registers
306 if ( pAig->vOnehots )
307 pTemp->vOnehots = Aig_ManRegProjectOnehots( pAig, pTemp, pAig->vOnehots, fVerbose );
308 // run SSW
309 pNew = Fra_FraigInduction( pTemp, pPars );
310 nClasses = Aig_TransferMappedClasses( pAig, pTemp, pMapBack );
311 if ( fVerbose )
312 printf( "%3d : Reg = %4d. PI = %4d. (True = %4d. Regs = %4d.) And = %5d. It = %3d. Cl = %5d.\n",
313 i, Vec_IntSize(vPart), Aig_ManCiNum(pTemp)-Vec_IntSize(vPart), nCountPis, nCountRegs, Aig_ManNodeNum(pTemp), pPars->nIters, nClasses );
314 Aig_ManStop( pNew );
315 Aig_ManStop( pTemp );
316 ABC_FREE( pMapBack );
317 }
318 // remap the AIG
319 pNew = Aig_ManDupRepr( pAig, 0 );
320 Aig_ManSeqCleanup( pNew );
321 // Aig_ManPrintStats( pAig );
322 // Aig_ManPrintStats( pNew );
323 Vec_VecFree( (Vec_Vec_t *)vResult );
324 pPars->nPartSize = nPartSize;
325 pPars->fVerbose = fVerbose;
326 if ( fVerbose )
327 {
328 ABC_PRT( "Total time", Abc_Clock() - clk );
329 }
330 return pNew;
331 }
332
333 /**Function*************************************************************
334
335 Synopsis [Performs sequential SAT sweeping.]
336
337 Description []
338
339 SideEffects []
340
341 SeeAlso []
342
343 ***********************************************************************/
Fra_FraigInduction(Aig_Man_t * pManAig,Fra_Ssw_t * pParams)344 Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, Fra_Ssw_t * pParams )
345 {
346 int fUseSimpleCnf = 0;
347 int fUseOldSimulation = 0;
348 // other paramaters affecting performance
349 // - presence of FRAIGing in Abc_NtkDarSeqSweep()
350 // - using distance-1 patterns in Fra_SmlAssignDist1()
351 // - the number of simulation patterns
352 // - the number of BMC frames
353
354 Fra_Man_t * p;
355 Fra_Par_t Pars, * pPars = &Pars;
356 Aig_Obj_t * pObj;
357 Cnf_Dat_t * pCnf;
358 Aig_Man_t * pManAigNew = NULL;
359 int nNodesBeg, nRegsBeg;
360 int nIter = -1; // Suppress "might be used uninitialized"
361 int i;
362 abctime clk = Abc_Clock(), clk2;
363 abctime TimeToStop = pParams->TimeLimit ? pParams->TimeLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
364
365 if ( Aig_ManNodeNum(pManAig) == 0 )
366 {
367 pParams->nIters = 0;
368 // Ntl_ManFinalize() needs the following to satisfy an assertion
369 Aig_ManReprStart(pManAig,Aig_ManObjNumMax(pManAig));
370 return Aig_ManDupOrdered(pManAig);
371 }
372 assert( Aig_ManRegNum(pManAig) > 0 );
373 assert( pParams->nFramesK > 0 );
374 //Aig_ManShow( pManAig, 0, NULL );
375
376 if ( pParams->fWriteImps && pParams->nPartSize > 0 )
377 {
378 pParams->nPartSize = 0;
379 printf( "Partitioning was disabled to allow implication writing.\n" );
380 }
381 // perform partitioning
382 if ( (pParams->nPartSize > 0 && pParams->nPartSize < Aig_ManRegNum(pManAig))
383 || (pManAig->vClockDoms && Vec_VecSize(pManAig->vClockDoms) > 0) )
384 return Fra_FraigInductionPart( pManAig, pParams );
385
386 nNodesBeg = Aig_ManNodeNum(pManAig);
387 nRegsBeg = Aig_ManRegNum(pManAig);
388
389 // enhance the AIG by adding timeframes
390 // Fra_FramesAddMore( pManAig, 3 );
391
392 // get parameters
393 Fra_ParamsDefaultSeq( pPars );
394 pPars->nFramesP = pParams->nFramesP;
395 pPars->nFramesK = pParams->nFramesK;
396 pPars->nMaxImps = pParams->nMaxImps;
397 pPars->nMaxLevs = pParams->nMaxLevs;
398 pPars->fVerbose = pParams->fVerbose;
399 pPars->fRewrite = pParams->fRewrite;
400 pPars->fLatchCorr = pParams->fLatchCorr;
401 pPars->fUseImps = pParams->fUseImps;
402 pPars->fWriteImps = pParams->fWriteImps;
403 pPars->fUse1Hot = pParams->fUse1Hot;
404
405 assert( !(pPars->nFramesP > 0 && pPars->fUse1Hot) );
406 assert( !(pPars->nFramesK > 1 && pPars->fUse1Hot) );
407
408 // start the fraig manager for this run
409 p = Fra_ManStart( pManAig, pPars );
410 p->pPars->nBTLimitNode = 0;
411 // derive and refine e-classes using K initialized frames
412 if ( fUseOldSimulation )
413 {
414 if ( pPars->nFramesP > 0 )
415 {
416 pPars->nFramesP = 0;
417 printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
418 }
419 p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
420 Fra_SmlSimulate( p, 1 );
421 }
422 else
423 {
424 // bug: r iscas/blif/s5378.blif ; st; ssw -v
425 // bug: r iscas/blif/s1238.blif ; st; ssw -v
426 // refine the classes with more simulation rounds
427 if ( pPars->fVerbose )
428 printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
429 p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1, 1 ); //pPars->nFramesK + 1, 1 );
430 if ( pPars->fVerbose )
431 {
432 ABC_PRT( "Time", Abc_Clock() - clk );
433 }
434 Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, p->pPars->nMaxLevs );
435 // Fra_ClassesPostprocess( p->pCla );
436 // compute one-hotness conditions
437 if ( p->pPars->fUse1Hot )
438 p->vOneHots = Fra_OneHotCompute( p, p->pSml );
439 // allocate new simulation manager for simulating counter-examples
440 Fra_SmlStop( p->pSml );
441 p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
442 }
443
444 // select the most expressive implications
445 if ( pPars->fUseImps )
446 p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
447
448 if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
449 {
450 if ( !pParams->fSilent )
451 printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
452 goto finish;
453 }
454
455 // perform BMC (for the min number of frames)
456 Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
457 //Fra_ClassesPrint( p->pCla, 1 );
458 // if ( p->vCex == NULL )
459 // p->vCex = Vec_IntAlloc( 1000 );
460
461 p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
462 p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
463 p->nRegsBeg = nRegsBeg; // Aig_ManRegNum(pManAig);
464
465 // dump AIG of the timeframes
466 // pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
467 // Aig_ManDumpBlif( pManAigNew, "frame_aig.blif", NULL, NULL );
468 // Fra_ManPartitionTest2( pManAigNew );
469 // Aig_ManStop( pManAigNew );
470
471 // iterate the inductive case
472 p->pCla->fRefinement = 1;
473 for ( nIter = 0; p->pCla->fRefinement; nIter++ )
474 {
475 int nLitsOld = Fra_ClassesCountLits(p->pCla);
476 int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
477 int nHotsOld = p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0;
478 abctime clk3 = Abc_Clock();
479
480 if ( pParams->TimeLimit != 0.0 && Abc_Clock() > TimeToStop )
481 {
482 if ( !pParams->fSilent )
483 printf( "Fra_FraigInduction(): Runtime limit exceeded.\n" );
484 goto finish;
485 }
486
487 // mark the classes as non-refined
488 p->pCla->fRefinement = 0;
489 // derive non-init K-timeframes while implementing e-classes
490 clk2 = Abc_Clock();
491 p->pManFraig = Fra_FramesWithClasses( p );
492 p->timeTrav += Abc_Clock() - clk2;
493 //Aig_ManDumpBlif( p->pManFraig, "testaig.blif", NULL, NULL );
494
495 // perform AIG rewriting
496 if ( p->pPars->fRewrite )
497 Fra_FraigInductionRewrite( p );
498
499 // convert the manager to SAT solver (the last nLatches outputs are inputs)
500 if ( fUseSimpleCnf || pPars->fUseImps )
501 pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
502 else
503 pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
504 // Cnf_DataTranformPolarity( pCnf, 0 );
505 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
506
507 p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
508 p->nSatVars = pCnf->nVars;
509 assert( p->pSat != NULL );
510 if ( p->pSat == NULL )
511 printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
512 if ( pPars->fUseImps )
513 {
514 Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
515 if ( p->pSat == NULL )
516 printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
517 }
518
519 // set the pointers to the manager
520 Aig_ManForEachObj( p->pManFraig, pObj, i )
521 pObj->pData = p;
522
523 // prepare solver for fraiging the last timeframe
524 Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
525
526 // transfer PI/LO variable numbers
527 Aig_ManForEachObj( p->pManFraig, pObj, i )
528 {
529 if ( pCnf->pVarNums[pObj->Id] == -1 )
530 continue;
531 Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
532 Fra_ObjSetFaninVec( pObj, (Vec_Ptr_t *)1 );
533 }
534 Cnf_DataFree( pCnf );
535
536 // add one-hotness clauses
537 if ( p->pPars->fUse1Hot )
538 Fra_OneHotAssume( p, p->vOneHots );
539 // if ( p->pManAig->vOnehots )
540 // Fra_OneHotAddKnownConstraint( p, p->pManAig->vOnehots );
541
542 // report the intermediate results
543 if ( pPars->fVerbose )
544 {
545 printf( "%3d : C = %6d. Cl = %6d. L = %6d. LR = %6d. ",
546 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses),
547 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
548 if ( p->pCla->vImps )
549 printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
550 if ( p->pPars->fUse1Hot )
551 printf( "1h = %6d. ", Fra_OneHotCount(p, p->vOneHots) );
552 printf( "NR = %6d. ", Aig_ManNodeNum(p->pManFraig) );
553 // printf( "\n" );
554 }
555
556 // perform sweeping
557 p->nSatCallsRecent = 0;
558 p->nSatCallsSkipped = 0;
559 clk2 = Abc_Clock();
560 if ( p->pPars->fUse1Hot )
561 Fra_OneHotCheck( p, p->vOneHots );
562 Fra_FraigSweep( p );
563 if ( pPars->fVerbose )
564 {
565 ABC_PRT( "T", Abc_Clock() - clk3 );
566 }
567
568 // Sat_SolverPrintStats( stdout, p->pSat );
569 // remove FRAIG and SAT solver
570 Aig_ManStop( p->pManFraig ); p->pManFraig = NULL;
571 // printf( "Vars = %d. Clauses = %d. Learnts = %d.\n", p->pSat->size, p->pSat->clauses.size, p->pSat->learnts.size );
572 sat_solver_delete( p->pSat ); p->pSat = NULL;
573 memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
574 // printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
575 assert( p->vTimeouts == NULL );
576 if ( p->vTimeouts )
577 printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
578 // check if refinement has happened
579 // p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
580 if ( p->pCla->fRefinement &&
581 nLitsOld == Fra_ClassesCountLits(p->pCla) &&
582 nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) &&
583 nHotsOld == (p->vOneHots? Fra_OneHotCount(p, p->vOneHots) : 0) )
584 {
585 printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
586 break;
587 }
588 }
589 /*
590 // verify implications using simulation
591 if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
592 {
593 int Temp;
594 abctime clk = Abc_Clock();
595 if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
596 printf( "Implications failing the simulation test = %d (out of %d). ", Temp, Vec_IntSize(p->pCla->vImps) );
597 else
598 printf( "All %d implications have passed the simulation test. ", Vec_IntSize(p->pCla->vImps) );
599 ABC_PRT( "Time", Abc_Clock() - clk );
600 }
601 */
602
603 // move the classes into representatives and reduce AIG
604 clk2 = Abc_Clock();
605 if ( p->pPars->fWriteImps && p->vOneHots && Fra_OneHotCount(p, p->vOneHots) )
606 {
607 extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols, int fCompact );
608 Aig_Man_t * pNew;
609 char * pFileName = Ioa_FileNameGenericAppend( p->pManAig->pName, "_care.aig" );
610 printf( "Care one-hotness clauses will be written into file \"%s\".\n", pFileName );
611 pManAigNew = Aig_ManDupOrdered( pManAig );
612 pNew = Fra_OneHotCreateExdc( p, p->vOneHots );
613 Ioa_WriteAiger( pNew, pFileName, 0, 1 );
614 Aig_ManStop( pNew );
615 }
616 else
617 {
618 // Fra_ClassesPrint( p->pCla, 1 );
619 Fra_ClassesSelectRepr( p->pCla );
620 Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
621 pManAigNew = Aig_ManDupRepr( pManAig, 0 );
622 }
623 // add implications to the manager
624 // if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
625 // Fra_ImpRecordInManager( p, pManAigNew );
626 // cleanup the new manager
627 Aig_ManSeqCleanup( pManAigNew );
628 // remove pointers to the dead nodes
629 // Aig_ManForEachObj( pManAig, pObj, i )
630 // if ( pObj->pData && Aig_ObjIsNone(pObj->pData) )
631 // pObj->pData = NULL;
632 // Aig_ManCountMergeRegs( pManAigNew );
633 p->timeTrav += Abc_Clock() - clk2;
634 p->timeTotal = Abc_Clock() - clk;
635 // get the final stats
636 p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
637 p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
638 p->nRegsEnd = Aig_ManRegNum(pManAigNew);
639 // free the manager
640 finish:
641 Fra_ManStop( p );
642 // check the output
643 // if ( Aig_ManCoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
644 // if ( Aig_ObjChild0( Aig_ManCo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
645 // printf( "Proved output constant 0.\n" );
646 pParams->nIters = nIter;
647 return pManAigNew;
648 }
649
650 /**Function*************************************************************
651
652 Synopsis [Outputs a set of pairs of equivalent nodes.]
653
654 Description []
655
656 SideEffects []
657
658 SeeAlso []
659
660 ***********************************************************************/
Fra_FraigInductionTest(char * pFileName,Fra_Ssw_t * pParams)661 int Fra_FraigInductionTest( char * pFileName, Fra_Ssw_t * pParams )
662 {
663 FILE * pFile;
664 char * pFilePairs;
665 Aig_Man_t * pMan, * pNew;
666 Aig_Obj_t * pObj, * pRepr;
667 int * pNum2Id;
668 int i, Counter = 0;
669 pMan = Saig_ManReadBlif( pFileName );
670 if ( pMan == NULL )
671 return 0;
672 // perform seq SAT sweeping
673 pNew = Fra_FraigInduction( pMan, pParams );
674 if ( pNew == NULL )
675 {
676 Aig_ManStop( pMan );
677 return 0;
678 }
679 if ( pParams->fVerbose )
680 {
681 printf( "Original AIG: " );
682 Aig_ManPrintStats( pMan );
683 printf( "Reduced AIG: " );
684 Aig_ManPrintStats( pNew );
685 }
686 Aig_ManStop( pNew );
687 pNum2Id = (int *)pMan->pData;
688 // write the output file
689 pFilePairs = Aig_FileNameGenericAppend( pFileName, ".pairs" );
690 pFile = fopen( pFilePairs, "w" );
691 Aig_ManForEachObj( pMan, pObj, i )
692 if ( (pRepr = pMan->pReprs[pObj->Id]) )
693 {
694 fprintf( pFile, "%d %d %c\n", pNum2Id[pObj->Id], pNum2Id[pRepr->Id], (Aig_ObjPhase(pObj) ^ Aig_ObjPhase(pRepr))? '-' : '+' );
695 Counter++;
696 }
697 fclose( pFile );
698 if ( pParams->fVerbose )
699 {
700 printf( "Result: %d pairs of seq equiv nodes are written into file \"%s\".\n", Counter, pFilePairs );
701 }
702 Aig_ManStop( pMan );
703 return 1;
704 }
705
706 ////////////////////////////////////////////////////////////////////////
707 /// END OF FILE ///
708 ////////////////////////////////////////////////////////////////////////
709
710
711 ABC_NAMESPACE_IMPL_END
712
713