abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
absOldSim.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [saigSimExt2.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Sequential AIG package.]
8 
9  Synopsis [Extending simulation trace to contain ternary values.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: saigSimExt2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "abs.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 #define SAIG_ZER 1
31 #define SAIG_ONE 2
32 #define SAIG_UND 3
33 
34 static inline int Saig_ManSimInfoNot( int Value )
35 {
36  if ( Value == SAIG_ZER )
37  return SAIG_ONE;
38  if ( Value == SAIG_ONE )
39  return SAIG_ZER;
40  return SAIG_UND;
41 }
42 
43 static inline int Saig_ManSimInfoAnd( int Value0, int Value1 )
44 {
45  if ( Value0 == SAIG_ZER || Value1 == SAIG_ZER )
46  return SAIG_ZER;
47  if ( Value0 == SAIG_ONE && Value1 == SAIG_ONE )
48  return SAIG_ONE;
49  return SAIG_UND;
50 }
51 
52 static inline int Saig_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
53 {
54  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
55  return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
56 }
57 
58 static inline void Saig_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
59 {
60  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
61  assert( Value >= SAIG_ZER && Value <= SAIG_UND );
62  Value ^= Saig_ManSimInfoGet( vSimInfo, pObj, iFrame );
63  pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
64 }
65 
66 
67 
68 #define SAIG_ZER_NEW 0 // 0 not visited
69 #define SAIG_ONE_NEW 1 // 1 not visited
70 #define SAIG_ZER_OLD 2 // 0 visited
71 #define SAIG_ONE_OLD 3 // 1 visited
72 
73 static inline int Saig_ManSimInfo2IsOld( int Value )
74 {
75  return Value == SAIG_ZER_OLD || Value == SAIG_ONE_OLD;
76 }
77 
78 static inline int Saig_ManSimInfo2SetOld( int Value )
79 {
80  if ( Value == SAIG_ZER_NEW )
81  return SAIG_ZER_OLD;
82  if ( Value == SAIG_ONE_NEW )
83  return SAIG_ONE_OLD;
84  assert( 0 );
85  return 0;
86 }
87 
88 static inline int Saig_ManSimInfo2Not( int Value )
89 {
90  if ( Value == SAIG_ZER_NEW )
91  return SAIG_ONE_NEW;
92  if ( Value == SAIG_ONE_NEW )
93  return SAIG_ZER_NEW;
94  if ( Value == SAIG_ZER_OLD )
95  return SAIG_ONE_OLD;
96  if ( Value == SAIG_ONE_OLD )
97  return SAIG_ZER_OLD;
98  assert( 0 );
99  return 0;
100 }
101 
102 static inline int Saig_ManSimInfo2And( int Value0, int Value1 )
103 {
104  if ( Value0 == SAIG_ZER_NEW || Value1 == SAIG_ZER_NEW )
105  return SAIG_ZER_NEW;
106  if ( Value0 == SAIG_ONE_NEW && Value1 == SAIG_ONE_NEW )
107  return SAIG_ONE_NEW;
108  assert( 0 );
109  return 0;
110 }
111 
112 static inline int Saig_ManSimInfo2Get( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
113 {
114  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
115  return 3 & (pInfo[iFrame >> 4] >> ((iFrame & 15) << 1));
116 }
117 
118 static inline void Saig_ManSimInfo2Set( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
119 {
120  unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, Aig_ObjId(pObj) );
121  Value ^= Saig_ManSimInfo2Get( vSimInfo, pObj, iFrame );
122  pInfo[iFrame >> 4] ^= (Value << ((iFrame & 15) << 1));
123 }
124 
125 // performs ternary simulation
126 //extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes );
127 
128 ////////////////////////////////////////////////////////////////////////
129 /// FUNCTION DEFINITIONS ///
130 ////////////////////////////////////////////////////////////////////////
131 
132 /**Function*************************************************************
133 
134  Synopsis [Performs ternary simulation for one node.]
135 
136  Description []
137 
138  SideEffects []
139 
140  SeeAlso []
141 
142 ***********************************************************************/
143 int Saig_ManExtendOneEval( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
144 {
145  int Value0, Value1, Value;
146  Value0 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
147  if ( Aig_ObjFaninC0(pObj) )
148  Value0 = Saig_ManSimInfoNot( Value0 );
149  if ( Aig_ObjIsCo(pObj) )
150  {
151  Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
152  return Value0;
153  }
154  assert( Aig_ObjIsNode(pObj) );
155  Value1 = Saig_ManSimInfoGet( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
156  if ( Aig_ObjFaninC1(pObj) )
157  Value1 = Saig_ManSimInfoNot( Value1 );
158  Value = Saig_ManSimInfoAnd( Value0, Value1 );
159  Saig_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
160  return Value;
161 }
162 
163 /**Function*************************************************************
164 
165  Synopsis [Performs ternary simulation for one design.]
166 
167  Description []
168 
169  SideEffects []
170 
171  SeeAlso []
172 
173 ***********************************************************************/
174 int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes )
175 {
176  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
177  int i, f, Entry, iBit = 0;
178  Saig_ManForEachLo( p, pObj, i )
179  Saig_ManSimInfoSet( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
180  for ( f = 0; f <= pCex->iFrame; f++ )
181  {
182  Saig_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE );
183  Saig_ManForEachPi( p, pObj, i )
184  Saig_ManSimInfoSet( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE:SAIG_ZER );
185  if ( vRes )
186  Vec_IntForEachEntry( vRes, Entry, i )
187  Saig_ManSimInfoSet( vSimInfo, Aig_ManCi(p, Entry), f, SAIG_UND );
188  Aig_ManForEachNode( p, pObj, i )
189  Saig_ManExtendOneEval( vSimInfo, pObj, f );
190  Aig_ManForEachCo( p, pObj, i )
191  Saig_ManExtendOneEval( vSimInfo, pObj, f );
192  if ( f == pCex->iFrame )
193  break;
194  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
195  Saig_ManSimInfoSet( vSimInfo, pObjLo, f+1, Saig_ManSimInfoGet(vSimInfo, pObjLi, f) );
196  }
197  // make sure the output of the property failed
198  pObj = Aig_ManCo( p, pCex->iPo );
199  return Saig_ManSimInfoGet( vSimInfo, pObj, pCex->iFrame );
200 }
201 
202 /**Function*************************************************************
203 
204  Synopsis [Performs ternary simulation for one node.]
205 
206  Description []
207 
208  SideEffects []
209 
210  SeeAlso []
211 
212 ***********************************************************************/
213 int Saig_ManExtendOneEval2( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
214 {
215  int Value0, Value1, Value;
216  Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pObj), iFrame );
217  if ( Aig_ObjFaninC0(pObj) )
218  Value0 = Saig_ManSimInfo2Not( Value0 );
219  if ( Aig_ObjIsCo(pObj) )
220  {
221  Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value0 );
222  return Value0;
223  }
224  assert( Aig_ObjIsNode(pObj) );
225  Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pObj), iFrame );
226  if ( Aig_ObjFaninC1(pObj) )
227  Value1 = Saig_ManSimInfo2Not( Value1 );
228  Value = Saig_ManSimInfo2And( Value0, Value1 );
229  Saig_ManSimInfo2Set( vSimInfo, pObj, iFrame, Value );
230  return Value;
231 }
232 
233 /**Function*************************************************************
234 
235  Synopsis [Performs sensitization analysis for one design.]
236 
237  Description []
238 
239  SideEffects []
240 
241  SeeAlso []
242 
243 ***********************************************************************/
244 int Saig_ManSimDataInit2( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo )
245 {
246  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
247  int i, f, iBit = 0;
248  Saig_ManForEachLo( p, pObj, i )
249  Saig_ManSimInfo2Set( vSimInfo, pObj, 0, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW );
250  for ( f = 0; f <= pCex->iFrame; f++ )
251  {
252  Saig_ManSimInfo2Set( vSimInfo, Aig_ManConst1(p), f, SAIG_ONE_NEW );
253  Saig_ManForEachPi( p, pObj, i )
254  Saig_ManSimInfo2Set( vSimInfo, pObj, f, Abc_InfoHasBit(pCex->pData, iBit++)?SAIG_ONE_NEW:SAIG_ZER_NEW );
255  Aig_ManForEachNode( p, pObj, i )
256  Saig_ManExtendOneEval2( vSimInfo, pObj, f );
257  Aig_ManForEachCo( p, pObj, i )
258  Saig_ManExtendOneEval2( vSimInfo, pObj, f );
259  if ( f == pCex->iFrame )
260  break;
261  Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
262  Saig_ManSimInfo2Set( vSimInfo, pObjLo, f+1, Saig_ManSimInfo2Get(vSimInfo, pObjLi, f) );
263  }
264  // make sure the output of the property failed
265  pObj = Aig_ManCo( p, pCex->iPo );
266  return Saig_ManSimInfo2Get( vSimInfo, pObj, pCex->iFrame );
267 }
268 
269 /**Function*************************************************************
270 
271  Synopsis [Drive implications of the given node towards primary outputs.]
272 
273  Description []
274 
275  SideEffects []
276 
277  SeeAlso []
278 
279 ***********************************************************************/
280 void Saig_ManSetAndDriveImplications_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Vec_Ptr_t * vSimInfo )
281 {
282  Aig_Obj_t * pFanout;
283  int k, iFanout = -1, Value0, Value1;
284  int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f );
285  assert( !Saig_ManSimInfo2IsOld( Value ) );
286  Saig_ManSimInfo2Set( vSimInfo, pObj, f, Saig_ManSimInfo2SetOld(Value) );
287  if ( (Aig_ObjIsCo(pObj) && f == fMax) || Saig_ObjIsPo(p, pObj) )
288  return;
289  if ( Saig_ObjIsLi( p, pObj ) )
290  {
291  assert( f < fMax );
292  pFanout = Saig_ObjLiToLo(p, pObj);
293  Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f+1 );
294  if ( !Saig_ManSimInfo2IsOld( Value ) )
295  Saig_ManSetAndDriveImplications_rec( p, pFanout, f+1, fMax, vSimInfo );
296  return;
297  }
298  assert( Aig_ObjIsCi(pObj) || Aig_ObjIsNode(pObj) || Aig_ObjIsConst1(pObj) );
299  Aig_ObjForEachFanout( p, pObj, pFanout, iFanout, k )
300  {
301  Value = Saig_ManSimInfo2Get( vSimInfo, pFanout, f );
302  if ( Saig_ManSimInfo2IsOld( Value ) )
303  continue;
304  if ( Aig_ObjIsCo(pFanout) )
305  {
306  Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo );
307  continue;
308  }
309  assert( Aig_ObjIsNode(pFanout) );
310  Value0 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin0(pFanout), f );
311  Value1 = Saig_ManSimInfo2Get( vSimInfo, Aig_ObjFanin1(pFanout), f );
312  if ( Aig_ObjFaninC0(pFanout) )
313  Value0 = Saig_ManSimInfo2Not( Value0 );
314  if ( Aig_ObjFaninC1(pFanout) )
315  Value1 = Saig_ManSimInfo2Not( Value1 );
316  if ( Value0 == SAIG_ZER_OLD || Value1 == SAIG_ZER_OLD ||
317  (Value0 == SAIG_ONE_OLD && Value1 == SAIG_ONE_OLD) )
318  Saig_ManSetAndDriveImplications_rec( p, pFanout, f, fMax, vSimInfo );
319  }
320 }
321 
322 /**Function*************************************************************
323 
324  Synopsis [Performs recursive sensetization analysis.]
325 
326  Description []
327 
328  SideEffects []
329 
330  SeeAlso []
331 
332 ***********************************************************************/
333 void Saig_ManExplorePaths_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int f, int fMax, Vec_Ptr_t * vSimInfo )
334 {
335  int Value = Saig_ManSimInfo2Get( vSimInfo, pObj, f );
336  if ( Saig_ManSimInfo2IsOld( Value ) )
337  return;
338  Saig_ManSetAndDriveImplications_rec( p, pObj, f, fMax, vSimInfo );
339  assert( !Aig_ObjIsConst1(pObj) );
340  if ( Saig_ObjIsLo(p, pObj) && f == 0 )
341  return;
342  if ( Saig_ObjIsPi(p, pObj) )
343  {
344  // propagate implications of this assignment
345  int i, iPiNum = Aig_ObjCioId(pObj);
346  for ( i = fMax; i >= 0; i-- )
347  if ( i != f )
348  Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, iPiNum), i, fMax, vSimInfo );
349  return;
350  }
351  if ( Saig_ObjIsLo( p, pObj ) )
352  {
353  assert( f > 0 );
354  Saig_ManExplorePaths_rec( p, Saig_ObjLoToLi(p, pObj), f-1, fMax, vSimInfo );
355  return;
356  }
357  if ( Aig_ObjIsCo(pObj) )
358  {
359  Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo );
360  return;
361  }
362  assert( Aig_ObjIsNode(pObj) );
363  if ( Value == SAIG_ZER_OLD )
364  {
365 // if ( (Aig_ObjId(pObj) & 1) == 0 )
366  Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo );
367 // else
368 // Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, fMax, vSimInfo );
369  }
370  else
371  {
372  Saig_ManExplorePaths_rec( p, Aig_ObjFanin0(pObj), f, fMax, vSimInfo );
373  Saig_ManExplorePaths_rec( p, Aig_ObjFanin1(pObj), f, fMax, vSimInfo );
374  }
375 }
376 
377 /**Function*************************************************************
378 
379  Synopsis [Returns the array of PIs for flops that should not be absracted.]
380 
381  Description []
382 
383  SideEffects []
384 
385  SeeAlso []
386 
387 ***********************************************************************/
388 Vec_Int_t * Saig_ManProcessCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
389 {
390  Aig_Obj_t * pObj;
391  Vec_Int_t * vRes, * vResInv;
392  int i, f, Value;
393 // assert( Aig_ManRegNum(p) > 0 );
394  assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Abc_BitWordNum(2*(pCex->iFrame+1)) );
395  // start simulation data
396  Value = Saig_ManSimDataInit2( p, pCex, vSimInfo );
397  assert( Value == SAIG_ONE_NEW );
398  // derive implications of constants and primary inputs
399  Saig_ManForEachLo( p, pObj, i )
400  Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo );
401  for ( f = pCex->iFrame; f >= 0; f-- )
402  {
403  Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo );
404  for ( i = 0; i < iFirstFlopPi; i++ )
405  Saig_ManSetAndDriveImplications_rec( p, Aig_ManCi(p, i), f, pCex->iFrame, vSimInfo );
406  }
407  // recursively compute justification
408  Saig_ManExplorePaths_rec( p, Aig_ManCo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo );
409  // select the result
410  vRes = Vec_IntAlloc( 1000 );
411  vResInv = Vec_IntAlloc( 1000 );
412  for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
413  {
414  for ( f = pCex->iFrame; f >= 0; f-- )
415  {
416  Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManCi(p, i), f );
417  if ( Saig_ManSimInfo2IsOld( Value ) )
418  break;
419  }
420  if ( f >= 0 )
421  Vec_IntPush( vRes, i );
422  else
423  Vec_IntPush( vResInv, i );
424  }
425  // resimulate to make sure it is valid
426  Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
427  assert( Value == SAIG_ONE );
428  Vec_IntFree( vResInv );
429  return vRes;
430 }
431 
432 /**Function*************************************************************
433 
434  Synopsis [Returns the array of PIs for flops that should not be absracted.]
435 
436  Description []
437 
438  SideEffects []
439 
440  SeeAlso []
441 
442 ***********************************************************************/
443 Vec_Int_t * Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
444 {
445  Vec_Int_t * vRes;
446  Vec_Ptr_t * vSimInfo;
447  abctime clk;
448  if ( Saig_ManPiNum(p) != pCex->nPis )
449  {
450  printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n",
451  Aig_ManCiNum(p), pCex->nPis );
452  return NULL;
453  }
454  Aig_ManFanoutStart( p );
455  vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Abc_BitWordNum(2*(pCex->iFrame+1)) );
456  Vec_PtrCleanSimInfo( vSimInfo, 0, Abc_BitWordNum(2*(pCex->iFrame+1)) );
457 
458 clk = Abc_Clock();
459  vRes = Saig_ManProcessCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
460  if ( fVerbose )
461  {
462  printf( "Total new PIs = %3d. Non-removable PIs = %3d. ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
463 ABC_PRT( "Time", Abc_Clock() - clk );
464  }
465  Vec_PtrFree( vSimInfo );
466  Aig_ManFanoutStop( p );
467  return vRes;
468 }
469 
470 
471 ////////////////////////////////////////////////////////////////////////
472 /// END OF FILE ///
473 ////////////////////////////////////////////////////////////////////////
474 
475 
477 
#define Aig_ObjForEachFanout(p, pObj, pFanout, iFan, i)
Definition: aig.h:427
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Saig_ManExtendOneEval(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
FUNCTION DEFINITIONS ///.
Definition: absOldSim.c:143
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
static int Saig_ManSimInfo2And(int Value0, int Value1)
Definition: absOldSim.c:102
#define SAIG_ONE
Definition: absOldSim.c:31
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
#define SAIG_ONE_OLD
Definition: absOldSim.c:71
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static abctime Abc_Clock()
Definition: abc_global.h:279
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
#define SAIG_ONE_NEW
Definition: absOldSim.c:69
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Vec_Int_t * Saig_ManProcessCex(Aig_Man_t *p, int iFirstFlopPi, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo, int fVerbose)
Definition: absOldSim.c:388
void Aig_ManFanoutStart(Aig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: aigFanout.c:56
void Aig_ManFanoutStop(Aig_Man_t *p)
Definition: aigFanout.c:89
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
int Saig_ManExtendOneEval2(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
Definition: absOldSim.c:213
void Saig_ManSetAndDriveImplications_rec(Aig_Man_t *p, Aig_Obj_t *pObj, int f, int fMax, Vec_Ptr_t *vSimInfo)
Definition: absOldSim.c:280
#define SAIG_UND
Definition: absOldSim.c:32
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static void Saig_ManSimInfo2Set(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame, int Value)
Definition: absOldSim.c:118
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
static int Saig_ObjIsPo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:83
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
int Saig_ManSimDataInit(Aig_Man_t *p, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo, Vec_Int_t *vRes)
Definition: absOldSim.c:174
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Vec_Int_t * Saig_ManExtendCounterExampleTest2(Aig_Man_t *p, int iFirstFlopPi, Abc_Cex_t *pCex, int fVerbose)
Definition: absOldSim.c:443
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Saig_ManSimInfoAnd(int Value0, int Value1)
Definition: absOldSim.c:43
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define SAIG_ZER_OLD
Definition: absOldSim.c:70
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
#define SAIG_ZER
DECLARATIONS ///.
Definition: absOldSim.c:30
#define ABC_PRT(a, t)
Definition: abc_global.h:220
int Saig_ManSimDataInit2(Aig_Man_t *p, Abc_Cex_t *pCex, Vec_Ptr_t *vSimInfo)
Definition: absOldSim.c:244
static int Saig_ManSimInfoNot(int Value)
Definition: absOldSim.c:34
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
static void Saig_ManSimInfoSet(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame, int Value)
Definition: absOldSim.c:58
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
#define assert(ex)
Definition: util_old.h:213
void Saig_ManExplorePaths_rec(Aig_Man_t *p, Aig_Obj_t *pObj, int f, int fMax, Vec_Ptr_t *vSimInfo)
Definition: absOldSim.c:333
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
static int Saig_ManSimInfo2Not(int Value)
Definition: absOldSim.c:88
static int Saig_ManSimInfo2SetOld(int Value)
Definition: absOldSim.c:78
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
#define SAIG_ZER_NEW
Definition: absOldSim.c:68
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Saig_ManSimInfo2Get(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
Definition: absOldSim.c:112
static int Saig_ManSimInfo2IsOld(int Value)
Definition: absOldSim.c:73
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
static int Saig_ManSimInfoGet(Vec_Ptr_t *vSimInfo, Aig_Obj_t *pObj, int iFrame)
Definition: absOldSim.c:52
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91