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 [Improved 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 #include "aig/gia/giaAig.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 struct Txs_Man_t_
31 {
32 Gia_Man_t * pGia; // user's AIG
33 Vec_Int_t * vPrio; // priority of each flop
34 Vec_Int_t * vCiObjs; // cone leaves (CI obj IDs)
35 Vec_Int_t * vCoObjs; // cone roots (CO obj IDs)
36 Vec_Int_t * vCiVals; // cone leaf values (0/1 CI values)
37 Vec_Int_t * vCoVals; // cone root values (0/1 CO values)
38 Vec_Int_t * vNodes; // cone nodes (node obj IDs)
39 Vec_Int_t * vTemp; // cone nodes (node obj IDs)
40 Vec_Int_t * vPiLits; // resulting array of PI literals
41 Vec_Int_t * vFfLits; // resulting array of flop literals
42 Pdr_Man_t * pMan; // calling manager
43 };
44
45 ////////////////////////////////////////////////////////////////////////
46 /// FUNCTION DEFINITIONS ///
47 ////////////////////////////////////////////////////////////////////////
48
49 /**Function*************************************************************
50
51 Synopsis [Start and stop the ternary simulation engine.]
52
53 Description []
54
55 SideEffects []
56
57 SeeAlso []
58
59 ***********************************************************************/
Txs_ManStart(Pdr_Man_t * pMan,Aig_Man_t * pAig,Vec_Int_t * vPrio)60 Txs_Man_t * Txs_ManStart( Pdr_Man_t * pMan, Aig_Man_t * pAig, Vec_Int_t * vPrio )
61 {
62 Txs_Man_t * p;
63 // Aig_Obj_t * pObj;
64 // int i;
65 assert( Vec_IntSize(vPrio) == Aig_ManRegNum(pAig) );
66 p = ABC_CALLOC( Txs_Man_t, 1 );
67 p->pGia = Gia_ManFromAigSimple(pAig); // user's AIG
68 // Aig_ManForEachObj( pAig, pObj, i )
69 // assert( i == 0 || pObj->iData == Abc_Var2Lit(i, 0) );
70 p->vPrio = vPrio; // priority of each flop
71 p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves (CI obj IDs)
72 p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots (CO obj IDs)
73 p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values (0/1 CI values)
74 p->vCoVals = Vec_IntAlloc( 100 ); // cone root values (0/1 CO values)
75 p->vNodes = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
76 p->vTemp = Vec_IntAlloc( 100 ); // cone nodes (node obj IDs)
77 p->vPiLits = Vec_IntAlloc( 100 ); // resulting array of PI literals
78 p->vFfLits = Vec_IntAlloc( 100 ); // resulting array of flop literals
79 p->pMan = pMan; // calling manager
80 return p;
81 }
Txs_ManStop(Txs_Man_t * p)82 void Txs_ManStop( Txs_Man_t * p )
83 {
84 Gia_ManStop( p->pGia );
85 Vec_IntFree( p->vCiObjs );
86 Vec_IntFree( p->vCoObjs );
87 Vec_IntFree( p->vCiVals );
88 Vec_IntFree( p->vCoVals );
89 Vec_IntFree( p->vNodes );
90 Vec_IntFree( p->vTemp );
91 Vec_IntFree( p->vPiLits );
92 Vec_IntFree( p->vFfLits );
93 ABC_FREE( p );
94 }
95
96 /**Function*************************************************************
97
98 Synopsis [Marks the TFI cone and collects CIs and nodes.]
99
100 Description [For this procedure to work Value should not be ~0
101 at the beginning.]
102
103 SideEffects []
104
105 SeeAlso []
106
107 ***********************************************************************/
Txs_ManCollectCone_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes)108 void Txs_ManCollectCone_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
109 {
110 if ( !~pObj->Value )
111 return;
112 pObj->Value = ~0;
113 if ( Gia_ObjIsCi(pObj) )
114 {
115 Vec_IntPush( vCiObjs, Gia_ObjId(p, pObj) );
116 return;
117 }
118 assert( Gia_ObjIsAnd(pObj) );
119 Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
120 Txs_ManCollectCone_rec( p, Gia_ObjFanin1(pObj), vCiObjs, vNodes );
121 Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
122 }
Txs_ManCollectCone(Gia_Man_t * p,Vec_Int_t * vCoObjs,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes)123 void Txs_ManCollectCone( Gia_Man_t * p, Vec_Int_t * vCoObjs, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes )
124 {
125 Gia_Obj_t * pObj; int i;
126 // printf( "Collecting cones for clause with %d literals.\n", Vec_IntSize(vCoObjs) );
127 Vec_IntClear( vCiObjs );
128 Vec_IntClear( vNodes );
129 Gia_ManConst0(p)->Value = ~0;
130 Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
131 Txs_ManCollectCone_rec( p, Gia_ObjFanin0(pObj), vCiObjs, vNodes );
132 }
133
134 /**Function*************************************************************
135
136 Synopsis [Propagate values and assign priority.]
137
138 Description []
139
140 SideEffects []
141
142 SeeAlso []
143
144 ***********************************************************************/
Txs_ManForwardPass(Gia_Man_t * p,Vec_Int_t * vPrio,Vec_Int_t * vCiObjs,Vec_Int_t * vCiVals,Vec_Int_t * vNodes,Vec_Int_t * vCoObjs,Vec_Int_t * vCoVals)145 void Txs_ManForwardPass( Gia_Man_t * p,
146 Vec_Int_t * vPrio, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals,
147 Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals )
148 {
149 Gia_Obj_t * pObj, * pFan0, * pFan1;
150 int i, value0, value1;
151 pObj = Gia_ManConst0(p);
152 pObj->fMark0 = 0;
153 pObj->fMark1 = 0;
154 Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
155 {
156 pObj->fMark0 = Vec_IntEntry(vCiVals, i);
157 pObj->fMark1 = 0;
158 pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Vec_IntEntry(vPrio, Gia_ObjCioId(pObj)-Gia_ManPiNum(p));
159 assert( ~pObj->Value );
160 }
161 Gia_ManForEachObjVec( vNodes, p, pObj, i )
162 {
163 pFan0 = Gia_ObjFanin0(pObj);
164 pFan1 = Gia_ObjFanin1(pObj);
165 value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
166 value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
167 pObj->fMark0 = value0 && value1;
168 pObj->fMark1 = 0;
169 if ( pObj->fMark0 )
170 pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
171 else if ( value0 )
172 pObj->Value = pFan1->Value;
173 else if ( value1 )
174 pObj->Value = pFan0->Value;
175 else // if ( value0 == 0 && value1 == 0 )
176 pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
177 assert( ~pObj->Value );
178 }
179 Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
180 {
181 pFan0 = Gia_ObjFanin0(pObj);
182 pObj->fMark0 = (pFan0->fMark0 ^ Gia_ObjFaninC0(pObj));
183 pFan0->fMark1 = 1;
184 assert( (int)pObj->fMark0 == Vec_IntEntry(vCoVals, i) );
185 }
186 }
187
188 /**Function*************************************************************
189
190 Synopsis [Propagate requirements and collect results.]
191
192 Description []
193
194 SideEffects []
195
196 SeeAlso []
197
198 ***********************************************************************/
Txs_ObjIsJust(Gia_Man_t * p,Gia_Obj_t * pObj)199 static inline int Txs_ObjIsJust( Gia_Man_t * p, Gia_Obj_t * pObj )
200 {
201 Gia_Obj_t * pFan0 = Gia_ObjFanin0(pObj);
202 Gia_Obj_t * pFan1 = Gia_ObjFanin1(pObj);
203 int value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
204 int value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
205 assert( Gia_ObjIsAnd(pObj) );
206 if ( pObj->fMark0 )
207 return pFan0->fMark1 && pFan1->fMark1;
208 assert( !pObj->fMark0 );
209 assert( !value0 || !value1 );
210 if ( value0 )
211 return pFan1->fMark1 || Gia_ObjIsPi(p, pFan1);
212 if ( value1 )
213 return pFan0->fMark1 || Gia_ObjIsPi(p, pFan0);
214 assert( !value0 && !value1 );
215 return pFan0->fMark1 || pFan1->fMark1 || Gia_ObjIsPi(p, pFan0) || Gia_ObjIsPi(p, pFan1);
216 }
Txs_ManBackwardPass(Gia_Man_t * p,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes,Vec_Int_t * vPiLits,Vec_Int_t * vFfLits)217 void Txs_ManBackwardPass( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_Int_t * vPiLits, Vec_Int_t * vFfLits )
218 {
219 Gia_Obj_t * pObj, * pFan0, * pFan1; int i, value0, value1;
220 Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
221 {
222 if ( !pObj->fMark1 )
223 continue;
224 pObj->fMark1 = 0;
225 pFan0 = Gia_ObjFanin0(pObj);
226 pFan1 = Gia_ObjFanin1(pObj);
227 if ( pObj->fMark0 )
228 {
229 pFan0->fMark1 = 1;
230 pFan1->fMark1 = 1;
231 continue;
232 }
233 value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
234 value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
235 assert( !value0 || !value1 );
236 if ( value0 )
237 pFan1->fMark1 = 1;
238 else if ( value1 )
239 pFan0->fMark1 = 1;
240 else // if ( !value0 && !value1 )
241 {
242 if ( pFan0->fMark1 || pFan1->fMark1 )
243 continue;
244 if ( Gia_ObjIsPi(p, pFan0) )
245 pFan0->fMark1 = 1;
246 else if ( Gia_ObjIsPi(p, pFan1) )
247 pFan1->fMark1 = 1;
248 else if ( Gia_ObjIsAnd(pFan0) && Txs_ObjIsJust(p, pFan0) )
249 pFan0->fMark1 = 1;
250 else if ( Gia_ObjIsAnd(pFan1) && Txs_ObjIsJust(p, pFan1) )
251 pFan1->fMark1 = 1;
252 else
253 {
254 if ( pFan0->Value >= pFan1->Value )
255 pFan0->fMark1 = 1;
256 else
257 pFan1->fMark1 = 1;
258 }
259 }
260 }
261 Vec_IntClear( vPiLits );
262 Vec_IntClear( vFfLits );
263 Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
264 {
265 if ( !pObj->fMark1 )
266 continue;
267 if ( Gia_ObjIsPi(p, pObj) )
268 Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj), !pObj->fMark0) );
269 else
270 Vec_IntPush( vFfLits, Abc_Var2Lit(Gia_ObjCioId(pObj)-Gia_ManPiNum(p), !pObj->fMark0) );
271 }
272 assert( Vec_IntSize(vFfLits) > 0 );
273 }
274
275 /**Function*************************************************************
276
277 Synopsis [Collects justification path.]
278
279 Description []
280
281 SideEffects []
282
283 SeeAlso []
284
285 ***********************************************************************/
Txs_ManSelectJustPath(Gia_Man_t * p,Vec_Int_t * vNodes,Vec_Int_t * vCoObjs,Vec_Int_t * vRes)286 void Txs_ManSelectJustPath( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Int_t * vCoObjs, Vec_Int_t * vRes )
287 {
288 Gia_Obj_t * pObj, * pFan0, * pFan1;
289 int i, value0, value1;
290 // mark CO drivers
291 Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
292 Gia_ObjFanin0(pObj)->fMark1 = 1;
293 // collect just paths
294 Vec_IntClear( vRes );
295 Gia_ManForEachObjVecReverse( vNodes, p, pObj, i )
296 {
297 if ( !pObj->fMark1 )
298 continue;
299 pObj->fMark1 = 0;
300 Vec_IntPush( vRes, Gia_ObjId(p, pObj) );
301 pFan0 = Gia_ObjFanin0(pObj);
302 pFan1 = Gia_ObjFanin1(pObj);
303 if ( pObj->fMark0 )
304 {
305 pFan0->fMark1 = 1;
306 pFan1->fMark1 = 1;
307 continue;
308 }
309 value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
310 value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
311 assert( !value0 || !value1 );
312 if ( value0 )
313 pFan1->fMark1 = 1;
314 else if ( value1 )
315 pFan0->fMark1 = 1;
316 else // if ( !value0 && !value1 )
317 {
318 pFan0->fMark1 = 1;
319 pFan1->fMark1 = 1;
320 }
321 }
322 Vec_IntReverseOrder( vRes );
323 }
Txs_ManCollectJustPis(Gia_Man_t * p,Vec_Int_t * vCiObjs,Vec_Int_t * vPiLits)324 void Txs_ManCollectJustPis( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vPiLits )
325 {
326 Gia_Obj_t * pObj; int i;
327 Vec_IntClear( vPiLits );
328 Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
329 if ( pObj->fMark1 && Gia_ObjIsPi(p, pObj) )
330 Vec_IntPush( vPiLits, Abc_Var2Lit(Gia_ObjCioId(pObj), !pObj->fMark0) );
331 }
Txs_ManInitPrio(Gia_Man_t * p,Vec_Int_t * vCiObjs)332 void Txs_ManInitPrio( Gia_Man_t * p, Vec_Int_t * vCiObjs )
333 {
334 Gia_Obj_t * pObj; int i;
335 Gia_ManConst0(p)->Value = 0x7FFFFFFF;
336 Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
337 pObj->Value = Gia_ObjIsPi(p, pObj) ? 0x7FFFFFFF : Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
338 }
Txs_ManPropagatePrio(Gia_Man_t * p,Vec_Int_t * vNodes,Vec_Int_t * vPrio)339 void Txs_ManPropagatePrio( Gia_Man_t * p, Vec_Int_t * vNodes, Vec_Int_t * vPrio )
340 {
341 Gia_Obj_t * pObj, * pFan0, * pFan1;
342 int i, value0, value1;
343 Gia_ManForEachObjVec( vNodes, p, pObj, i )
344 {
345 pFan0 = Gia_ObjFanin0(pObj);
346 pFan1 = Gia_ObjFanin1(pObj);
347 if ( pObj->fMark0 )
348 {
349 // pObj->Value = Abc_MinInt( pFan0->Value, pFan1->Value );
350 if ( pFan0->Value == 0x7FFFFFFF )
351 pObj->Value = pFan1->Value;
352 else if ( pFan1->Value == 0x7FFFFFFF )
353 pObj->Value = pFan0->Value;
354 else if ( Vec_IntEntry(vPrio, pFan0->Value) < Vec_IntEntry(vPrio, pFan1->Value) )
355 pObj->Value = pFan0->Value;
356 else
357 pObj->Value = pFan1->Value;
358 continue;
359 }
360 value0 = pFan0->fMark0 ^ Gia_ObjFaninC0(pObj);
361 value1 = pFan1->fMark0 ^ Gia_ObjFaninC1(pObj);
362 assert( !value0 || !value1 );
363 if ( value0 )
364 pObj->Value = pFan1->Value;
365 else if ( value1 )
366 pObj->Value = pFan0->Value;
367 else // if ( value0 == 0 && value1 == 0 )
368 {
369 // pObj->Value = Abc_MaxInt( pFan0->Value, pFan1->Value );
370 if ( pFan0->Value == 0x7FFFFFFF || pFan1->Value == 0x7FFFFFFF )
371 pObj->Value = 0x7FFFFFFF;
372 else if ( Vec_IntEntry(vPrio, pFan0->Value) >= Vec_IntEntry(vPrio, pFan1->Value) )
373 pObj->Value = pFan0->Value;
374 else
375 pObj->Value = pFan1->Value;
376 }
377 assert( ~pObj->Value );
378 }
379 }
Txs_ManFindMinId(Gia_Man_t * p,Vec_Int_t * vCoObjs,Vec_Int_t * vPrio)380 int Txs_ManFindMinId( Gia_Man_t * p, Vec_Int_t * vCoObjs, Vec_Int_t * vPrio )
381 {
382 Gia_Obj_t * pObj; int i, iMinId = -1;
383 Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
384 if ( Gia_ObjFanin0(pObj)->Value != 0x7FFFFFFF )
385 {
386 if ( iMinId == -1 || Vec_IntEntry(vPrio, iMinId) > Vec_IntEntry(vPrio, Gia_ObjFanin0(pObj)->Value) )
387 iMinId = Gia_ObjFanin0(pObj)->Value;
388 }
389 return iMinId;
390 }
Txs_ManFindCiReduction(Gia_Man_t * p,Vec_Int_t * vPrio,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes,Vec_Int_t * vCoObjs,Vec_Int_t * vPiLits,Vec_Int_t * vFfLits,Vec_Int_t * vTemp)391 void Txs_ManFindCiReduction( Gia_Man_t * p,
392 Vec_Int_t * vPrio, Vec_Int_t * vCiObjs,
393 Vec_Int_t * vNodes, Vec_Int_t * vCoObjs,
394 Vec_Int_t * vPiLits, Vec_Int_t * vFfLits, Vec_Int_t * vTemp )
395 {
396 Gia_Obj_t * pObj;
397 int iPrioCi;
398 // propagate PI influence
399 Txs_ManSelectJustPath( p, vNodes, vCoObjs, vTemp );
400 Txs_ManCollectJustPis( p, vCiObjs, vPiLits );
401 // printf( "%d -> %d ", Vec_IntSize(vNodes), Vec_IntSize(vTemp) );
402 // iteratively detect and remove smallest IDs
403 Vec_IntClear( vFfLits );
404 Txs_ManInitPrio( p, vCiObjs );
405 while ( 1 )
406 {
407 Txs_ManPropagatePrio( p, vTemp, vPrio );
408 iPrioCi = Txs_ManFindMinId( p, vCoObjs, vPrio );
409 if ( iPrioCi == -1 )
410 break;
411 pObj = Gia_ManCi( p, Gia_ManPiNum(p)+iPrioCi );
412 Vec_IntPush( vFfLits, Abc_Var2Lit(iPrioCi, !pObj->fMark0) );
413 pObj->Value = 0x7FFFFFFF;
414 }
415 }
Txs_ManPrintFlopLits(Vec_Int_t * vFfLits,Vec_Int_t * vPrio)416 void Txs_ManPrintFlopLits( Vec_Int_t * vFfLits, Vec_Int_t * vPrio )
417 {
418 int i, Entry;
419 printf( "%3d : ", Vec_IntSize(vFfLits) );
420 Vec_IntForEachEntry( vFfLits, Entry, i )
421 printf( "%s%d(%d) ", Abc_LitIsCompl(Entry)? "+":"-", Abc_Lit2Var(Entry), Vec_IntEntry(vPrio, Abc_Lit2Var(Entry)) );
422 printf( "\n" );
423 }
424
425 /**Function*************************************************************
426
427 Synopsis [Verify the result.]
428
429 Description []
430
431 SideEffects []
432
433 SeeAlso []
434
435 ***********************************************************************/
Txs_ManVerify(Gia_Man_t * p,Vec_Int_t * vCiObjs,Vec_Int_t * vNodes,Vec_Int_t * vPiLits,Vec_Int_t * vFfLits,Vec_Int_t * vCoObjs,Vec_Int_t * vCoVals)436 void Txs_ManVerify( Gia_Man_t * p, Vec_Int_t * vCiObjs, Vec_Int_t * vNodes, Vec_Int_t * vPiLits, Vec_Int_t * vFfLits, Vec_Int_t * vCoObjs, Vec_Int_t * vCoVals )
437 {
438 Gia_Obj_t * pObj;
439 int i, iLit;
440 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
441 Gia_ManForEachObjVec( vCiObjs, p, pObj, i )
442 Gia_ObjTerSimSetX( pObj );
443 Vec_IntForEachEntry( vPiLits, iLit, i )
444 {
445 pObj = Gia_ManPi( p, Abc_Lit2Var(iLit) );
446 assert( Gia_ObjTerSimGetX(pObj) );
447 if ( Abc_LitIsCompl(iLit) )
448 Gia_ObjTerSimSet0( pObj );
449 else
450 Gia_ObjTerSimSet1( pObj );
451 }
452 Vec_IntForEachEntry( vFfLits, iLit, i )
453 {
454 pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Abc_Lit2Var(iLit) );
455 assert( Gia_ObjTerSimGetX(pObj) );
456 if ( Abc_LitIsCompl(iLit) )
457 Gia_ObjTerSimSet0( pObj );
458 else
459 Gia_ObjTerSimSet1( pObj );
460 }
461 Gia_ManForEachObjVec( vNodes, p, pObj, i )
462 Gia_ObjTerSimAnd( pObj );
463 Gia_ManForEachObjVec( vCoObjs, p, pObj, i )
464 {
465 Gia_ObjTerSimCo( pObj );
466 if ( Vec_IntEntry(vCoVals, i) )
467 assert( Gia_ObjTerSimGet1(pObj) );
468 else
469 assert( Gia_ObjTerSimGet0(pObj) );
470 }
471 }
472
473 /**Function*************************************************************
474
475 Synopsis [Shrinks values using ternary simulation.]
476
477 Description [The cube contains the set of flop index literals which,
478 when converted into a clause and applied to the combinational outputs,
479 led to a satisfiable SAT run in frame k (values stored in the SAT solver).
480 If the cube is NULL, it is assumed that the first property output was
481 asserted and failed.
482 The resulting array is a set of flop index literals that asserts the COs.
483 Priority contains 0 for i-th entry if the i-th FF is desirable to remove.]
484
485 SideEffects []
486
487 SeeAlso []
488
489 ***********************************************************************/
Txs_ManTernarySim(Txs_Man_t * p,int k,Pdr_Set_t * pCube)490 Pdr_Set_t * Txs_ManTernarySim( Txs_Man_t * p, int k, Pdr_Set_t * pCube )
491 {
492 int fTryNew = 1;
493 Pdr_Set_t * pRes;
494 Gia_Obj_t * pObj;
495 // collect CO objects
496 Vec_IntClear( p->vCoObjs );
497 if ( pCube == NULL ) // the target is the property output
498 {
499 pObj = Gia_ManCo(p->pGia, p->pMan->iOutCur);
500 Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
501 }
502 else // the target is the cube
503 {
504 int i;
505 for ( i = 0; i < pCube->nLits; i++ )
506 {
507 if ( pCube->Lits[i] == -1 )
508 continue;
509 pObj = Gia_ManCo(p->pGia, Gia_ManPoNum(p->pGia) + Abc_Lit2Var(pCube->Lits[i]));
510 Vec_IntPush( p->vCoObjs, Gia_ObjId(p->pGia, pObj) );
511 }
512 }
513 if ( 0 )
514 {
515 Abc_Print( 1, "Trying to justify cube " );
516 if ( pCube )
517 Pdr_SetPrint( stdout, pCube, Gia_ManRegNum(p->pGia), NULL );
518 else
519 Abc_Print( 1, "<prop=fail>" );
520 Abc_Print( 1, " in frame %d.\n", k );
521 }
522
523 // collect CI objects
524 Txs_ManCollectCone( p->pGia, p->vCoObjs, p->vCiObjs, p->vNodes );
525 // collect values
526 Pdr_ManCollectValues( p->pMan, k, p->vCiObjs, p->vCiVals );
527 Pdr_ManCollectValues( p->pMan, k, p->vCoObjs, p->vCoVals );
528
529 // perform two passes
530 Txs_ManForwardPass( p->pGia, p->vPrio, p->vCiObjs, p->vCiVals, p->vNodes, p->vCoObjs, p->vCoVals );
531 if ( fTryNew )
532 Txs_ManFindCiReduction( p->pGia, p->vPrio, p->vCiObjs, p->vNodes, p->vCoObjs, p->vPiLits, p->vFfLits, p->vTemp );
533 else
534 Txs_ManBackwardPass( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits );
535 Txs_ManVerify( p->pGia, p->vCiObjs, p->vNodes, p->vPiLits, p->vFfLits, p->vCoObjs, p->vCoVals );
536
537 // derive the final set
538 pRes = Pdr_SetCreate( p->vFfLits, p->vPiLits );
539 //ZH: Disabled assertion because this invariant doesn't hold with down
540 //because of the join operation which can bring in initial states
541 //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
542 return pRes;
543 }
544
545 ////////////////////////////////////////////////////////////////////////
546 /// END OF FILE ///
547 ////////////////////////////////////////////////////////////////////////
548
549
550 ABC_NAMESPACE_IMPL_END
551