1 /**CFile****************************************************************
2
3 FileName [pdrTsim.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Property driven reachability.]
8
9 Synopsis [Ternary simulation.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 20, 2010.]
16
17 Revision [$Id: pdrTsim.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "pdrInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25 ////////////////////////////////////////////////////////////////////////
26 /// DECLARATIONS ///
27 ////////////////////////////////////////////////////////////////////////
28
29 #define PDR_ZER 1
30 #define PDR_ONE 2
31 #define PDR_UND 3
32
Pdr_ManSimInfoNot(int Value)33 static inline int Pdr_ManSimInfoNot( int Value )
34 {
35 if ( Value == PDR_ZER )
36 return PDR_ONE;
37 if ( Value == PDR_ONE )
38 return PDR_ZER;
39 return PDR_UND;
40 }
41
Pdr_ManSimInfoAnd(int Value0,int Value1)42 static inline int Pdr_ManSimInfoAnd( int Value0, int Value1 )
43 {
44 if ( Value0 == PDR_ZER || Value1 == PDR_ZER )
45 return PDR_ZER;
46 if ( Value0 == PDR_ONE && Value1 == PDR_ONE )
47 return PDR_ONE;
48 return PDR_UND;
49 }
50
Pdr_ManSimInfoGet(Aig_Man_t * p,Aig_Obj_t * pObj)51 static inline int Pdr_ManSimInfoGet( Aig_Man_t * p, Aig_Obj_t * pObj )
52 {
53 return 3 & (p->pTerSimData[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
54 }
55
Pdr_ManSimInfoSet(Aig_Man_t * p,Aig_Obj_t * pObj,int Value)56 static inline void Pdr_ManSimInfoSet( Aig_Man_t * p, Aig_Obj_t * pObj, int Value )
57 {
58 assert( Value >= PDR_ZER && Value <= PDR_UND );
59 Value ^= Pdr_ManSimInfoGet( p, pObj );
60 p->pTerSimData[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
61 }
62
63 ////////////////////////////////////////////////////////////////////////
64 /// FUNCTION DEFINITIONS ///
65 ////////////////////////////////////////////////////////////////////////
66
67 /**Function*************************************************************
68
69 Synopsis [Marks the TFI cone and collects CIs and nodes.]
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ***********************************************************************/
Pdr_ManCollectCone_rec(Aig_Man_t * pAig,Aig_Obj_t * pObj,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes)78 void Pdr_ManCollectCone_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
79 {
80 assert( !Aig_IsComplement(pObj) );
81 if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
82 return;
83 Aig_ObjSetTravIdCurrent(pAig, pObj);
84 if ( Aig_ObjIsCi(pObj) )
85 {
86 Vec_IntPush( vCiObjs, Aig_ObjId(pObj) );
87 return;
88 }
89 Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin0(pObj), vCiObjs, vNodes );
90 if ( Aig_ObjIsCo(pObj) )
91 return;
92 Pdr_ManCollectCone_rec( pAig, Aig_ObjFanin1(pObj), vCiObjs, vNodes );
93 Vec_IntPush( vNodes, Aig_ObjId(pObj) );
94 }
95
96 /**Function*************************************************************
97
98 Synopsis [Marks the TFI cone and collects CIs and nodes.]
99
100 Description []
101
102 SideEffects []
103
104 SeeAlso []
105
106 ***********************************************************************/
Pdr_ManCollectCone(Aig_Man_t * pAig,Vec_Int_t * vCoObjs,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes)107 void Pdr_ManCollectCone( Aig_Man_t * pAig, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
108 {
109 Aig_Obj_t * pObj;
110 int i;
111 Vec_IntClear( vCiObjs );
112 Vec_IntClear( vNodes );
113 Aig_ManIncrementTravId( pAig );
114 Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
115 Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
116 Pdr_ManCollectCone_rec( pAig, pObj, vCiObjs, vNodes );
117 }
118
119 /**Function*************************************************************
120
121 Synopsis [Performs ternary simulation for one node.]
122
123 Description []
124
125 SideEffects []
126
127 SeeAlso []
128
129 ***********************************************************************/
Pdr_ManExtendOneEval(Aig_Man_t * pAig,Aig_Obj_t * pObj)130 int Pdr_ManExtendOneEval( Aig_Man_t * pAig, Aig_Obj_t * pObj )
131 {
132 int Value0, Value1, Value;
133 Value0 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin0(pObj) );
134 if ( Aig_ObjFaninC0(pObj) )
135 Value0 = Pdr_ManSimInfoNot( Value0 );
136 if ( Aig_ObjIsCo(pObj) )
137 {
138 Pdr_ManSimInfoSet( pAig, pObj, Value0 );
139 return Value0;
140 }
141 assert( Aig_ObjIsNode(pObj) );
142 Value1 = Pdr_ManSimInfoGet( pAig, Aig_ObjFanin1(pObj) );
143 if ( Aig_ObjFaninC1(pObj) )
144 Value1 = Pdr_ManSimInfoNot( Value1 );
145 Value = Pdr_ManSimInfoAnd( Value0, Value1 );
146 Pdr_ManSimInfoSet( pAig, pObj, Value );
147 return Value;
148 }
149
150 /**Function*************************************************************
151
152 Synopsis [Performs ternary simulation for one design.]
153
154 Description []
155
156 SideEffects []
157
158 SeeAlso []
159
160 ***********************************************************************/
Pdr_ManSimDataInit(Aig_Man_t * pAig,Vec_Int_t * vCiObjs,Vec_Int_t * vCiVals,Vec_Int_t * vNodes,Vec_Int_t * vCoObjs,Vec_Int_t * vCoVals,Vec_Int_t * vCi2Rem)161 int Pdr_ManSimDataInit( Aig_Man_t * pAig,
162 Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vNodes,
163 Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals, Vec_Int_t * vCi2Rem )
164 {
165 Aig_Obj_t * pObj;
166 int i;
167 // set the CI values
168 Pdr_ManSimInfoSet( pAig, Aig_ManConst1(pAig), PDR_ONE );
169 Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
170 Pdr_ManSimInfoSet( pAig, pObj, (Vec_IntEntry(vCiVals, i)?PDR_ONE:PDR_ZER) );
171 // set the FOs to remove
172 if ( vCi2Rem != NULL )
173 Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
174 Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
175 // perform ternary simulation
176 Aig_ManForEachObjVec( vNodes, pAig, pObj, i )
177 Pdr_ManExtendOneEval( pAig, pObj );
178 // transfer results to the output
179 Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
180 Pdr_ManExtendOneEval( pAig, pObj );
181 // check the results
182 Aig_ManForEachObjVec( vCoObjs, pAig, pObj, i )
183 if ( Pdr_ManSimInfoGet( pAig, pObj ) != (Vec_IntEntry(vCoVals, i)?PDR_ONE:PDR_ZER) )
184 return 0;
185 return 1;
186 }
187
188 /**Function*************************************************************
189
190 Synopsis [Tries to assign ternary value to one of the CIs.]
191
192 Description []
193
194 SideEffects []
195
196 SeeAlso []
197
198 ***********************************************************************/
Pdr_ManExtendOne(Aig_Man_t * pAig,Aig_Obj_t * pObj,Vec_Int_t * vUndo,Vec_Int_t * vVis)199 int Pdr_ManExtendOne( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vUndo, Vec_Int_t * vVis )
200 {
201 Aig_Obj_t * pFanout;
202 int i, k, iFanout = -1, Value, Value2;
203 assert( Saig_ObjIsLo(pAig, pObj) );
204 assert( Aig_ObjIsTravIdCurrent(pAig, pObj) );
205 // save original value
206 Value = Pdr_ManSimInfoGet( pAig, pObj );
207 assert( Value == PDR_ZER || Value == PDR_ONE );
208 Vec_IntPush( vUndo, Aig_ObjId(pObj) );
209 Vec_IntPush( vUndo, Value );
210 // update original value
211 Pdr_ManSimInfoSet( pAig, pObj, PDR_UND );
212 // traverse
213 Vec_IntClear( vVis );
214 Vec_IntPush( vVis, Aig_ObjId(pObj) );
215 Aig_ManForEachObjVec( vVis, pAig, pObj, i )
216 {
217 Aig_ObjForEachFanout( pAig, pObj, pFanout, iFanout, k )
218 {
219 if ( !Aig_ObjIsTravIdCurrent(pAig, pFanout) )
220 continue;
221 assert( Aig_ObjId(pObj) < Aig_ObjId(pFanout) );
222 Value = Pdr_ManSimInfoGet( pAig, pFanout );
223 if ( Value == PDR_UND )
224 continue;
225 Value2 = Pdr_ManExtendOneEval( pAig, pFanout );
226 if ( Value2 == Value )
227 continue;
228 assert( Value2 == PDR_UND );
229 Vec_IntPush( vUndo, Aig_ObjId(pFanout) );
230 Vec_IntPush( vUndo, Value );
231 if ( Aig_ObjIsCo(pFanout) )
232 return 0;
233 assert( Aig_ObjIsNode(pFanout) );
234 Vec_IntPushOrder( vVis, Aig_ObjId(pFanout) );
235 }
236 }
237 return 1;
238 }
239
240 /**Function*************************************************************
241
242 Synopsis [Undoes the partial results of ternary simulation.]
243
244 Description []
245
246 SideEffects []
247
248 SeeAlso []
249
250 ***********************************************************************/
Pdr_ManExtendUndo(Aig_Man_t * pAig,Vec_Int_t * vUndo)251 void Pdr_ManExtendUndo( Aig_Man_t * pAig, Vec_Int_t * vUndo )
252 {
253 Aig_Obj_t * pObj;
254 int i, Value;
255 Aig_ManForEachObjVec( vUndo, pAig, pObj, i )
256 {
257 Value = Vec_IntEntry(vUndo, ++i);
258 assert( Pdr_ManSimInfoGet(pAig, pObj) == PDR_UND );
259 Pdr_ManSimInfoSet( pAig, pObj, Value );
260 }
261 }
262
263 /**Function*************************************************************
264
265 Synopsis [Derives the resulting cube.]
266
267 Description []
268
269 SideEffects []
270
271 SeeAlso []
272
273 ***********************************************************************/
Pdr_ManDeriveResult(Aig_Man_t * pAig,Vec_Int_t * vCiObjs,Vec_Int_t * vCiVals,Vec_Int_t * vCi2Rem,Vec_Int_t * vRes,Vec_Int_t * vPiLits)274 void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem, Vec_Int_t * vRes, Vec_Int_t * vPiLits )
275 {
276 Aig_Obj_t * pObj;
277 int i, Lit;
278 // mark removed flop outputs
279 Aig_ManIncrementTravId( pAig );
280 Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
281 {
282 assert( Saig_ObjIsLo( pAig, pObj ) );
283 Aig_ObjSetTravIdCurrent(pAig, pObj);
284 }
285 // collect flop outputs that are not marked
286 Vec_IntClear( vRes );
287 Vec_IntClear( vPiLits );
288 Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
289 {
290 if ( Saig_ObjIsPi(pAig, pObj) )
291 {
292 Lit = Abc_Var2Lit( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) );
293 Vec_IntPush( vPiLits, Lit );
294 continue;
295 }
296 assert( Saig_ObjIsLo(pAig, pObj) );
297 if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
298 continue;
299 Lit = Abc_Var2Lit( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) );
300 Vec_IntPush( vRes, Lit );
301 }
302 if ( Vec_IntSize(vRes) == 0 )
303 Vec_IntPush(vRes, 0);
304 }
305
306 /**Function*************************************************************
307
308 Synopsis [Derives the resulting cube.]
309
310 Description []
311
312 SideEffects []
313
314 SeeAlso []
315
316 ***********************************************************************/
Pdr_ManPrintCex(Aig_Man_t * pAig,Vec_Int_t * vCiObjs,Vec_Int_t * vCiVals,Vec_Int_t * vCi2Rem)317 void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals, Vec_Int_t * vCi2Rem )
318 {
319 Aig_Obj_t * pObj;
320 int i;
321 char * pBuff = ABC_ALLOC( char, Aig_ManCiNum(pAig)+1 );
322 for ( i = 0; i < Aig_ManCiNum(pAig); i++ )
323 pBuff[i] = '-';
324 pBuff[i] = 0;
325 Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i )
326 pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0');
327 if ( vCi2Rem )
328 Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i )
329 pBuff[Aig_ObjCioId(pObj)] = 'x';
330 Abc_Print( 1, "%s\n", pBuff );
331 ABC_FREE( pBuff );
332 }
333
334 /**Function*************************************************************
335
336 Synopsis [Shrinks values using ternary simulation.]
337
338 Description [The cube contains the set of flop index literals which,
339 when converted into a clause and applied to the combinational outputs,
340 led to a satisfiable SAT run in frame k (values stored in the SAT solver).
341 If the cube is NULL, it is assumed that the first property output was
342 asserted and failed.
343 The resulting array is a set of flop index literals that asserts the COs.
344 Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
345
346 SideEffects []
347
348 SeeAlso []
349
350 ***********************************************************************/
Pdr_ManTernarySim(Pdr_Man_t * p,int k,Pdr_Set_t * pCube)351 Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
352 {
353 Pdr_Set_t * pRes;
354 Vec_Int_t * vPrio = p->vPrio; // priority flops (flop indices)
355 Vec_Int_t * vPiLits = p->vLits; // array of literals (0/1 PI values)
356 Vec_Int_t * vCiObjs = p->vCiObjs; // cone leaves (CI obj IDs)
357 Vec_Int_t * vCoObjs = p->vCoObjs; // cone roots (CO obj IDs)
358 Vec_Int_t * vCiVals = p->vCiVals; // cone leaf values (0/1 CI values)
359 Vec_Int_t * vCoVals = p->vCoVals; // cone root values (0/1 CO values)
360 Vec_Int_t * vNodes = p->vNodes; // cone nodes (node obj IDs)
361 Vec_Int_t * vUndo = p->vUndo; // cone undos (node obj IDs)
362 Vec_Int_t * vVisits = p->vVisits; // intermediate (obj IDs)
363 Vec_Int_t * vCi2Rem = p->vCi2Rem; // CIs to be removed (CI obj IDs)
364 Vec_Int_t * vRes = p->vRes; // final result (flop literals)
365 Aig_Obj_t * pObj;
366 int i, Entry, RetValue;
367 //abctime clk = Abc_Clock();
368
369 // collect CO objects
370 Vec_IntClear( vCoObjs );
371 if ( pCube == NULL ) // the target is the property output
372 {
373 // Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
374 Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) );
375 }
376 else // the target is the cube
377 {
378 for ( i = 0; i < pCube->nLits; i++ )
379 {
380 if ( pCube->Lits[i] == -1 )
381 continue;
382 pObj = Saig_ManLi(p->pAig, (pCube->Lits[i] >> 1));
383 Vec_IntPush( vCoObjs, Aig_ObjId(pObj) );
384 }
385 }
386 if ( p->pPars->fVeryVerbose )
387 {
388 Abc_Print( 1, "Trying to justify cube " );
389 if ( pCube )
390 Pdr_SetPrint( stdout, pCube, Aig_ManRegNum(p->pAig), NULL );
391 else
392 Abc_Print( 1, "<prop=fail>" );
393 Abc_Print( 1, " in frame %d.\n", k );
394 }
395
396 // collect CI objects
397 Pdr_ManCollectCone( p->pAig, vCoObjs, vCiObjs, vNodes );
398 // collect values
399 Pdr_ManCollectValues( p, k, vCiObjs, vCiVals );
400 Pdr_ManCollectValues( p, k, vCoObjs, vCoVals );
401 // simulate for the first time
402 if ( p->pPars->fVeryVerbose )
403 Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
404 RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, NULL );
405 assert( RetValue );
406
407 // iteratively remove flops
408 if ( p->pPars->fFlopPrio )
409 {
410 // collect flops and sort them by priority
411 Vec_IntClear( vRes );
412 Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
413 {
414 if ( !Saig_ObjIsLo( p->pAig, pObj ) )
415 continue;
416 Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
417 Vec_IntPush( vRes, Entry );
418 }
419 Vec_IntSelectSortCost( Vec_IntArray(vRes), Vec_IntSize(vRes), vPrio );
420
421 // try removing flops starting from low-priority to high-priority
422 Vec_IntClear( vCi2Rem );
423 Vec_IntForEachEntry( vRes, Entry, i )
424 {
425 pObj = Aig_ManCi( p->pAig, Saig_ManPiNum(p->pAig) + Entry );
426 assert( Saig_ObjIsLo( p->pAig, pObj ) );
427 Vec_IntClear( vUndo );
428 if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
429 Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
430 else
431 Pdr_ManExtendUndo( p->pAig, vUndo );
432 }
433 }
434 else
435 {
436 // try removing low-priority flops first
437 Vec_IntClear( vCi2Rem );
438 Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
439 {
440 if ( !Saig_ObjIsLo( p->pAig, pObj ) )
441 continue;
442 Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
443 if ( Vec_IntEntry(vPrio, Entry) )
444 continue;
445 Vec_IntClear( vUndo );
446 if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
447 Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
448 else
449 Pdr_ManExtendUndo( p->pAig, vUndo );
450 }
451 // try removing high-priority flops next
452 Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
453 {
454 if ( !Saig_ObjIsLo( p->pAig, pObj ) )
455 continue;
456 Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
457 if ( !Vec_IntEntry(vPrio, Entry) )
458 continue;
459 Vec_IntClear( vUndo );
460 if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
461 Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
462 else
463 Pdr_ManExtendUndo( p->pAig, vUndo );
464 }
465 }
466
467 if ( p->pPars->fVeryVerbose )
468 Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
469 RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
470 assert( RetValue );
471
472 // derive the set of resulting registers
473 Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
474 assert( Vec_IntSize(vRes) > 0 );
475 //p->tTsim += Abc_Clock() - clk;
476
477 // move abstracted literals from flops to inputs
478 if ( p->pPars->fUseAbs && p->vAbsFlops )
479 {
480 int i, iLit, k = 0;
481 Vec_IntForEachEntry( vRes, iLit, i )
482 {
483 if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
484 Vec_IntWriteEntry( vRes, k++, iLit );
485 else
486 Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
487 }
488 Vec_IntShrink( vRes, k );
489 }
490 pRes = Pdr_SetCreate( vRes, vPiLits );
491 //ZH: Disabled assertion because this invariant doesn't hold with down
492 //because of the join operation which can bring in initial states
493 //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
494 return pRes;
495 }
496
497 ////////////////////////////////////////////////////////////////////////
498 /// END OF FILE ///
499 ////////////////////////////////////////////////////////////////////////
500
501
502 ABC_NAMESPACE_IMPL_END
503