1 /**CFile****************************************************************
2
3 FileName [fraImp.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [New FRAIG package.]
8
9 Synopsis [Detecting and proving implications.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 30, 2007.]
16
17 Revision [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "fra.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Counts the number of 1s in each siminfo of each node.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Fra_SmlCountOnesOne(Fra_Sml_t * p,int Node)45 static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
46 {
47 unsigned * pSim;
48 int k, Counter = 0;
49 pSim = Fra_ObjSim( p, Node );
50 for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
51 Counter += Aig_WordCountOnes( pSim[k] );
52 return Counter;
53 }
54
55 /**Function*************************************************************
56
57 Synopsis [Counts the number of 1s in each siminfo of each node.]
58
59 Description []
60
61 SideEffects []
62
63 SeeAlso []
64
65 ***********************************************************************/
Fra_SmlCountOnes(Fra_Sml_t * p)66 static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
67 {
68 Aig_Obj_t * pObj;
69 int i, * pnBits;
70 pnBits = ABC_ALLOC( int, Aig_ManObjNumMax(p->pAig) );
71 memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
72 Aig_ManForEachObj( p->pAig, pObj, i )
73 pnBits[i] = Fra_SmlCountOnesOne( p, i );
74 return pnBits;
75 }
76
77 /**Function*************************************************************
78
79 Synopsis [Returns 1 if implications holds.]
80
81 Description []
82
83 SideEffects []
84
85 SeeAlso []
86
87 ***********************************************************************/
Sml_NodeCheckImp(Fra_Sml_t * p,int Left,int Right)88 static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
89 {
90 unsigned * pSimL, * pSimR;
91 int k;
92 pSimL = Fra_ObjSim( p, Left );
93 pSimR = Fra_ObjSim( p, Right );
94 for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
95 if ( pSimL[k] & ~pSimR[k] )
96 return 0;
97 return 1;
98 }
99
100 /**Function*************************************************************
101
102 Synopsis [Counts the number of 1s in the complement of the implication.]
103
104 Description []
105
106 SideEffects []
107
108 SeeAlso []
109
110 ***********************************************************************/
Sml_NodeNotImpWeight(Fra_Sml_t * p,int Left,int Right)111 static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
112 {
113 unsigned * pSimL, * pSimR;
114 int k, Counter = 0;
115 pSimL = Fra_ObjSim( p, Left );
116 pSimR = Fra_ObjSim( p, Right );
117 for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
118 Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
119 return Counter;
120 }
121
122 /**Function*************************************************************
123
124 Synopsis [Computes the complement of the implication.]
125
126 Description []
127
128 SideEffects []
129
130 SeeAlso []
131
132 ***********************************************************************/
Sml_NodeSaveNotImpPatterns(Fra_Sml_t * p,int Left,int Right,unsigned * pResult)133 static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
134 {
135 unsigned * pSimL, * pSimR;
136 int k;
137 pSimL = Fra_ObjSim( p, Left );
138 pSimR = Fra_ObjSim( p, Right );
139 for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
140 pResult[k] |= pSimL[k] & ~pSimR[k];
141 }
142
143 /**Function*************************************************************
144
145 Synopsis [Returns the array of nodes sorted by the number of 1s.]
146
147 Description []
148
149 SideEffects []
150
151 SeeAlso []
152
153 ***********************************************************************/
Fra_SmlSortUsingOnes(Fra_Sml_t * p,int fLatchCorr)154 Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
155 {
156 Aig_Obj_t * pObj;
157 Vec_Ptr_t * vNodes;
158 int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
159 assert( p->nWordsTotal > 0 );
160 // count 1s in each node's siminfo
161 pnBits = Fra_SmlCountOnes( p );
162 // count number of nodes having that many 1s
163 nNodes = 0;
164 nBits = p->nWordsTotal * 32;
165 pnNodes = ABC_ALLOC( int, nBits + 1 );
166 memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
167 Aig_ManForEachObj( p->pAig, pObj, i )
168 {
169 if ( i == 0 ) continue;
170 // skip non-PI and non-internal nodes
171 if ( fLatchCorr )
172 {
173 if ( !Aig_ObjIsCi(pObj) )
174 continue;
175 }
176 else
177 {
178 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
179 continue;
180 }
181 // skip nodes participating in the classes
182 // if ( Fra_ClassObjRepr(pObj) )
183 // continue;
184 assert( pnBits[i] <= nBits ); // "<" because of normalized info
185 pnNodes[pnBits[i]]++;
186 nNodes++;
187 }
188 // allocate memory for all the nodes
189 pMemory = ABC_ALLOC( int, nNodes + nBits + 1 );
190 // markup the memory for each node
191 vNodes = Vec_PtrAlloc( nBits + 1 );
192 Vec_PtrPush( vNodes, pMemory );
193 for ( i = 1; i <= nBits; i++ )
194 {
195 pMemory += pnNodes[i-1] + 1;
196 Vec_PtrPush( vNodes, pMemory );
197 }
198 // add the nodes
199 memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
200 Aig_ManForEachObj( p->pAig, pObj, i )
201 {
202 if ( i == 0 ) continue;
203 // skip non-PI and non-internal nodes
204 if ( fLatchCorr )
205 {
206 if ( !Aig_ObjIsCi(pObj) )
207 continue;
208 }
209 else
210 {
211 if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsCi(pObj) )
212 continue;
213 }
214 // skip nodes participating in the classes
215 // if ( Fra_ClassObjRepr(pObj) )
216 // continue;
217 pMemory = (int *)Vec_PtrEntry( vNodes, pnBits[i] );
218 pMemory[ pnNodes[pnBits[i]]++ ] = i;
219 }
220 // add 0s in the end
221 nTotal = 0;
222 Vec_PtrForEachEntry( int *, vNodes, pMemory, i )
223 {
224 pMemory[ pnNodes[i]++ ] = 0;
225 nTotal += pnNodes[i];
226 }
227 assert( nTotal == nNodes + nBits + 1 );
228 ABC_FREE( pnNodes );
229 ABC_FREE( pnBits );
230 return vNodes;
231 }
232
233 /**Function*************************************************************
234
235 Synopsis [Returns the array of implications with the highest cost.]
236
237 Description []
238
239 SideEffects []
240
241 SeeAlso []
242
243 ***********************************************************************/
Fra_SmlSelectMaxCost(Vec_Int_t * vImps,int * pCosts,int nCostMax,int nImpLimit,int * pCostRange)244 Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
245 {
246 Vec_Int_t * vImpsNew;
247 int * pCostCount, nImpCount, Imp, i, c;
248 assert( Vec_IntSize(vImps) >= nImpLimit );
249 // count how many implications have each cost
250 pCostCount = ABC_ALLOC( int, nCostMax + 1 );
251 memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
252 for ( i = 0; i < Vec_IntSize(vImps); i++ )
253 {
254 assert( pCosts[i] <= nCostMax );
255 pCostCount[ pCosts[i] ]++;
256 }
257 assert( pCostCount[0] == 0 );
258 // select the bound on the cost (above this bound, implication will be included)
259 nImpCount = 0;
260 for ( c = nCostMax; c > 0; c-- )
261 {
262 nImpCount += pCostCount[c];
263 if ( nImpCount >= nImpLimit )
264 break;
265 }
266 // printf( "Cost range >= %d.\n", c );
267 // collect implications with the given costs
268 vImpsNew = Vec_IntAlloc( nImpLimit );
269 Vec_IntForEachEntry( vImps, Imp, i )
270 {
271 if ( pCosts[i] < c )
272 continue;
273 Vec_IntPush( vImpsNew, Imp );
274 if ( Vec_IntSize( vImpsNew ) == nImpLimit )
275 break;
276 }
277 ABC_FREE( pCostCount );
278 if ( pCostRange )
279 *pCostRange = c;
280 return vImpsNew;
281 }
282
283 /**Function*************************************************************
284
285 Synopsis [Compares two implications using their largest ID.]
286
287 Description []
288
289 SideEffects []
290
291 SeeAlso []
292
293 ***********************************************************************/
Sml_CompareMaxId(unsigned short * pImp1,unsigned short * pImp2)294 int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
295 {
296 int Max1 = Abc_MaxInt( pImp1[0], pImp1[1] );
297 int Max2 = Abc_MaxInt( pImp2[0], pImp2[1] );
298 if ( Max1 < Max2 )
299 return -1;
300 if ( Max1 > Max2 )
301 return 1;
302 return 0;
303 }
304
305 /**Function*************************************************************
306
307 Synopsis [Derives implication candidates.]
308
309 Description [Implication candidates have the property that
310 (1) they hold using sequential simulation information
311 (2) they do not hold using combinational simulation information
312 (3) they have as high expressive power as possible (heuristically)
313 that is, they are easy to disprove combinationally
314 meaning they cover relatively larger sequential subspace.]
315
316 SideEffects []
317
318 SeeAlso []
319
320 ***********************************************************************/
Fra_ImpDerive(Fra_Man_t * p,int nImpMaxLimit,int nImpUseLimit,int fLatchCorr)321 Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
322 {
323 int nSimWords = 64;
324 Fra_Sml_t * pSeq, * pComb;
325 Vec_Int_t * vImps, * vTemp;
326 Vec_Ptr_t * vNodes;
327 int * pImpCosts, * pNodesI, * pNodesK;
328 int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
329 int CostMin = ABC_INFINITY, CostMax = 0;
330 int i, k, Imp, CostRange;
331 abctime clk = Abc_Clock();
332 assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
333 assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
334 // normalize both managers
335 pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
336 pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1, 1 );
337 // get the nodes sorted by the number of 1s
338 vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
339 // count the total number of implications
340 for ( k = nSimWords * 32; k > 0; k-- )
341 for ( i = k - 1; i > 0; i-- )
342 for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
343 for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
344 nImpsTotal++;
345
346 // compute implications and their costs
347 pImpCosts = ABC_ALLOC( int, nImpMaxLimit );
348 vImps = Vec_IntAlloc( nImpMaxLimit );
349 for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
350 for ( i = k - 1; i > 0; i-- )
351 {
352 // HERE WE ARE MISSING SOME POTENTIAL IMPLICATIONS (with complement!)
353
354 for ( pNodesI = (int *)Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
355 for ( pNodesK = (int *)Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
356 {
357 nImpsTried++;
358 if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
359 {
360 nImpsNonSeq++;
361 continue;
362 }
363 if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
364 {
365 nImpsComb++;
366 continue;
367 }
368 nImpsCollected++;
369 Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
370 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
371 CostMin = Abc_MinInt( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
372 CostMax = Abc_MaxInt( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
373 Vec_IntPush( vImps, Imp );
374 if ( Vec_IntSize(vImps) == nImpMaxLimit )
375 goto finish;
376 }
377 }
378 finish:
379 Fra_SmlStop( pComb );
380 Fra_SmlStop( pSeq );
381
382 // select implications with the highest cost
383 CostRange = CostMin;
384 if ( Vec_IntSize(vImps) > nImpUseLimit )
385 {
386 vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
387 Vec_IntFree( vTemp );
388 }
389
390 // dealloc
391 ABC_FREE( pImpCosts );
392 {
393 void * pTemp = Vec_PtrEntry(vNodes, 0);
394 ABC_FREE( pTemp );
395 }
396 Vec_PtrFree( vNodes );
397 // reorder implications topologically
398 qsort( (void *)Vec_IntArray(vImps), (size_t)Vec_IntSize(vImps), sizeof(int),
399 (int (*)(const void *, const void *)) Sml_CompareMaxId );
400 if ( p->pPars->fVerbose )
401 {
402 printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n",
403 nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
404 printf( "Implication weight: Min = %d. Pivot = %d. Max = %d. ",
405 CostMin, CostRange, CostMax );
406 ABC_PRT( "Time", Abc_Clock() - clk );
407 }
408 return vImps;
409 }
410
411
412 // the following three procedures are called to
413 // - add implications to the SAT solver
414 // - check implications using the SAT solver
415 // - refine implications using after a cex is generated
416
417 /**Function*************************************************************
418
419 Synopsis [Add implication clauses to the SAT solver.]
420
421 Description [Note that implications should be checked in the first frame!]
422
423 SideEffects []
424
425 SeeAlso []
426
427 ***********************************************************************/
Fra_ImpAddToSolver(Fra_Man_t * p,Vec_Int_t * vImps,int * pSatVarNums)428 void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
429 {
430 sat_solver * pSat = p->pSat;
431 Aig_Obj_t * pLeft, * pRight;
432 Aig_Obj_t * pLeftF, * pRightF;
433 int pLits[2], Imp, Left, Right, i, f, status;
434 int fComplL, fComplR;
435 Vec_IntForEachEntry( vImps, Imp, i )
436 {
437 // get the corresponding nodes
438 pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
439 pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
440 // check if all the nodes are present
441 for ( f = 0; f < p->pPars->nFramesK; f++ )
442 {
443 // map these info fraig
444 pLeftF = Fra_ObjFraig( pLeft, f );
445 pRightF = Fra_ObjFraig( pRight, f );
446 if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
447 {
448 Vec_IntWriteEntry( vImps, i, 0 );
449 break;
450 }
451 }
452 if ( f < p->pPars->nFramesK )
453 continue;
454 // add constraints in each timeframe
455 for ( f = 0; f < p->pPars->nFramesK; f++ )
456 {
457 // map these info fraig
458 pLeftF = Fra_ObjFraig( pLeft, f );
459 pRightF = Fra_ObjFraig( pRight, f );
460 // get the corresponding SAT numbers
461 Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
462 Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
463 assert( Left > 0 && Left < p->nSatVars );
464 assert( Right > 0 && Right < p->nSatVars );
465 // get the complemented attributes
466 fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
467 fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
468 // get the constraint
469 // L => R L' v R (complement = L & R')
470 pLits[0] = 2 * Left + !fComplL;
471 pLits[1] = 2 * Right + fComplR;
472 // add constraint to solver
473 if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
474 {
475 sat_solver_delete( pSat );
476 p->pSat = NULL;
477 return;
478 }
479 }
480 }
481 status = sat_solver_simplify(pSat);
482 if ( status == 0 )
483 {
484 sat_solver_delete( pSat );
485 p->pSat = NULL;
486 }
487 // printf( "Total imps = %d. ", Vec_IntSize(vImps) );
488 Fra_ImpCompactArray( vImps );
489 // printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
490 }
491
492 /**Function*************************************************************
493
494 Synopsis [Check implications for the node (if they are present).]
495
496 Description [Returns the new position in the array.]
497
498 SideEffects []
499
500 SeeAlso []
501
502 ***********************************************************************/
Fra_ImpCheckForNode(Fra_Man_t * p,Vec_Int_t * vImps,Aig_Obj_t * pNode,int Pos)503 int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
504 {
505 Aig_Obj_t * pLeft, * pRight;
506 Aig_Obj_t * pLeftF, * pRightF;
507 int i, Imp, Left, Right, Max, RetValue;
508 int fComplL, fComplR;
509 Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
510 {
511 if ( Imp == 0 )
512 continue;
513 Left = Fra_ImpLeft(Imp);
514 Right = Fra_ImpRight(Imp);
515 Max = Abc_MaxInt( Left, Right );
516 assert( Max >= pNode->Id );
517 if ( Max > pNode->Id )
518 return i;
519 // get the corresponding nodes
520 pLeft = Aig_ManObj( p->pManAig, Left );
521 pRight = Aig_ManObj( p->pManAig, Right );
522 // get the corresponding FRAIG nodes
523 pLeftF = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
524 pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
525 // get the complemented attributes
526 fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
527 fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
528 // check equality
529 if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
530 {
531 if ( fComplL == fComplR ) // x => x - always true
532 continue;
533 assert( fComplL != fComplR );
534 // consider 4 possibilities:
535 // NOT(1) => 1 or 0 => 1 - always true
536 // 1 => NOT(1) or 1 => 0 - never true
537 // NOT(x) => x or x - not always true
538 // x => NOT(x) or NOT(x) - not always true
539 if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
540 continue;
541 // disproved implication
542 p->pCla->fRefinement = 1;
543 Vec_IntWriteEntry( vImps, i, 0 );
544 continue;
545 }
546 // check the implication
547 // - if true, a clause is added
548 // - if false, a cex is simulated
549 // make sure the implication is refined
550 RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
551 if ( RetValue != 1 )
552 {
553 p->pCla->fRefinement = 1;
554 if ( RetValue == 0 )
555 Fra_SmlResimulate( p );
556 if ( Vec_IntEntry(vImps, i) != 0 )
557 printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
558 assert( Vec_IntEntry(vImps, i) == 0 );
559 }
560 }
561 return i;
562 }
563
564 /**Function*************************************************************
565
566 Synopsis [Removes those implications that no longer hold.]
567
568 Description [Returns 1 if refinement has happened.]
569
570 SideEffects []
571
572 SeeAlso []
573
574 ***********************************************************************/
Fra_ImpRefineUsingCex(Fra_Man_t * p,Vec_Int_t * vImps)575 int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
576 {
577 Aig_Obj_t * pLeft, * pRight;
578 int Imp, i, RetValue = 0;
579 Vec_IntForEachEntry( vImps, Imp, i )
580 {
581 if ( Imp == 0 )
582 continue;
583 // get the corresponding nodes
584 pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
585 pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
586 // check if implication holds using this simulation info
587 if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
588 {
589 Vec_IntWriteEntry( vImps, i, 0 );
590 RetValue = 1;
591 }
592 }
593 return RetValue;
594 }
595
596 /**Function*************************************************************
597
598 Synopsis [Removes empty implications.]
599
600 Description []
601
602 SideEffects []
603
604 SeeAlso []
605
606 ***********************************************************************/
Fra_ImpCompactArray(Vec_Int_t * vImps)607 void Fra_ImpCompactArray( Vec_Int_t * vImps )
608 {
609 int i, k, Imp;
610 k = 0;
611 Vec_IntForEachEntry( vImps, Imp, i )
612 if ( Imp )
613 Vec_IntWriteEntry( vImps, k++, Imp );
614 Vec_IntShrink( vImps, k );
615 }
616
617 /**Function*************************************************************
618
619 Synopsis [Determines the ratio of the state space by computed implications.]
620
621 Description []
622
623 SideEffects []
624
625 SeeAlso []
626
627 ***********************************************************************/
Fra_ImpComputeStateSpaceRatio(Fra_Man_t * p)628 double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
629 {
630 int nSimWords = 64;
631 Fra_Sml_t * pComb;
632 unsigned * pResult;
633 double Ratio = 0.0;
634 int Left, Right, Imp, i;
635 if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
636 return Ratio;
637 // simulate the AIG manager with combinational patterns
638 pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords, 0 );
639 // go through the implications and collect where they do not hold
640 pResult = Fra_ObjSim( pComb, 0 );
641 assert( pResult[0] == 0 );
642 Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
643 {
644 Left = Fra_ImpLeft(Imp);
645 Right = Fra_ImpRight(Imp);
646 Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
647 }
648 // count the number of ones in this area
649 Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
650 Fra_SmlStop( pComb );
651 return Ratio;
652 }
653
654 /**Function*************************************************************
655
656 Synopsis [Returns the number of failed implications.]
657
658 Description []
659
660 SideEffects []
661
662 SeeAlso []
663
664 ***********************************************************************/
Fra_ImpVerifyUsingSimulation(Fra_Man_t * p)665 int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
666 {
667 int nFrames = 2000;
668 int nSimWords = 8;
669 Fra_Sml_t * pSeq;
670 char * pfFails;
671 int Left, Right, Imp, i, Counter;
672 if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
673 return 0;
674 // simulate the AIG manager with combinational patterns
675 pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords, 1 );
676 // go through the implications and check how many of them do not hold
677 pfFails = ABC_ALLOC( char, Vec_IntSize(p->pCla->vImps) );
678 memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
679 Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
680 {
681 Left = Fra_ImpLeft(Imp);
682 Right = Fra_ImpRight(Imp);
683 pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
684 }
685 // count how many has failed
686 Counter = 0;
687 for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
688 Counter += pfFails[i];
689 ABC_FREE( pfFails );
690 Fra_SmlStop( pSeq );
691 return Counter;
692 }
693
694 /**Function*************************************************************
695
696 Synopsis [Record proven implications in the AIG manager.]
697
698 Description []
699
700 SideEffects []
701
702 SeeAlso []
703
704 ***********************************************************************/
Fra_ImpRecordInManager(Fra_Man_t * p,Aig_Man_t * pNew)705 void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
706 {
707 Aig_Obj_t * pLeft, * pRight, * pMiter;
708 int nPosOld, Imp, i;
709 if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
710 return;
711 // go through the implication
712 nPosOld = Aig_ManCoNum(pNew);
713 Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
714 {
715 pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
716 pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
717 // record the implication: L' + R
718 pMiter = Aig_Or( pNew,
719 Aig_NotCond((Aig_Obj_t *)pLeft->pData, !pLeft->fPhase),
720 Aig_NotCond((Aig_Obj_t *)pRight->pData, pRight->fPhase) );
721 Aig_ObjCreateCo( pNew, pMiter );
722 }
723 pNew->nAsserts = Aig_ManCoNum(pNew) - nPosOld;
724 }
725
726 ////////////////////////////////////////////////////////////////////////
727 /// END OF FILE ///
728 ////////////////////////////////////////////////////////////////////////
729
730
731 ABC_NAMESPACE_IMPL_END
732
733