abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
pdrTsim.c
Go to the documentation of this file.
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 
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 
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 
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 
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 ***********************************************************************/
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 = toLitCond( 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 = toLitCond( 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 ***********************************************************************/
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 ***********************************************************************/
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 #if 1
408  // try removing high-priority flops
409  Vec_IntClear( vCi2Rem );
410  Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
411  {
412  if ( !Saig_ObjIsLo( p->pAig, pObj ) )
413  continue;
414  Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
415  if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
416  continue;
417  Vec_IntClear( vUndo );
418  if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
419  Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
420  else
421  Pdr_ManExtendUndo( p->pAig, vUndo );
422  }
423  // try removing low-priority flops
424  Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
425  {
426  if ( !Saig_ObjIsLo( p->pAig, pObj ) )
427  continue;
428  Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
429  if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
430  continue;
431  Vec_IntClear( vUndo );
432  if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
433  Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
434  else
435  Pdr_ManExtendUndo( p->pAig, vUndo );
436  }
437 #else
438  // try removing low-priority flops
439  Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
440  {
441  if ( !Saig_ObjIsLo( p->pAig, pObj ) )
442  continue;
443  Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
444  if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
445  continue;
446  Vec_IntClear( vUndo );
447  if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
448  Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
449  else
450  Pdr_ManExtendUndo( p->pAig, vUndo );
451  }
452  // try removing high-priority flops
453  Vec_IntClear( vCi2Rem );
454  Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
455  {
456  if ( !Saig_ObjIsLo( p->pAig, pObj ) )
457  continue;
458  Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
459  if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
460  continue;
461  Vec_IntClear( vUndo );
462  if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
463  Vec_IntPush( vCi2Rem, Aig_ObjId(pObj) );
464  else
465  Pdr_ManExtendUndo( p->pAig, vUndo );
466  }
467 #endif
468 
469 if ( p->pPars->fVeryVerbose )
470 Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
471  RetValue = Pdr_ManSimDataInit( p->pAig, vCiObjs, vCiVals, vNodes, vCoObjs, vCoVals, vCi2Rem );
472  assert( RetValue );
473 
474  // derive the set of resulting registers
475  Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
476  assert( Vec_IntSize(vRes) > 0 );
477  p->tTsim += Abc_Clock() - clk;
478  pRes = Pdr_SetCreate( vRes, vPiLits );
479  assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
480  return pRes;
481 }
482 
483 ////////////////////////////////////////////////////////////////////////
484 /// END OF FILE ///
485 ////////////////////////////////////////////////////////////////////////
486 
487 
488 ABC_NAMESPACE_IMPL_END
Aig_ObjForEachFanout
#define Aig_ObjForEachFanout(p, pObj, pFanout, iFan, i)
Definition: aig.h:427
PDR_ZER
#define PDR_ZER
DECLARATIONS ///.
Definition: pdrTsim.c:29
Pdr_Man_t_::pAig
Aig_Man_t * pAig
Definition: pdrInt.h:70
Vec_IntPushOrder
static void Vec_IntPushOrder(Vec_Int_t *p, int Entry)
Definition: vecInt.h:751
Pdr_ManExtendUndo
void Pdr_ManExtendUndo(Aig_Man_t *pAig, Vec_Int_t *vUndo)
Definition: pdrTsim.c:251
Pdr_SetCreate
Pdr_Set_t * Pdr_SetCreate(Vec_Int_t *vLits, Vec_Int_t *vPiLits)
Definition: pdrUtil.c:65
Pdr_Man_t_::vPrio
Vec_Int_t * vPrio
Definition: pdrInt.h:90
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ObjIsTravIdCurrent
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
Pdr_Man_t_::iOutCur
int iOutCur
Definition: pdrInt.h:81
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Pdr_ManCollectCone
void Pdr_ManCollectCone(Aig_Man_t *pAig, Vec_Int_t *vCoObjs, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes)
Definition: pdrTsim.c:107
Pdr_Man_t_::vRes
Vec_Int_t * vRes
Definition: pdrInt.h:100
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Pdr_Man_t_::vCiVals
Vec_Int_t * vCiVals
Definition: pdrInt.h:94
Pdr_Man_t_
Definition: pdrInt.h:66
Pdr_SetPrint
void Pdr_SetPrint(FILE *pFile, Pdr_Set_t *p, int nRegs, Vec_Int_t *vFlopCounts)
Definition: pdrUtil.c:225
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Pdr_ManSimInfoAnd
static int Pdr_ManSimInfoAnd(int Value0, int Value1)
Definition: pdrTsim.c:42
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ObjSetTravIdCurrent
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Pdr_Man_t_::vCi2Rem
Vec_Int_t * vCi2Rem
Definition: pdrInt.h:99
Pdr_Man_t_::vCoVals
Vec_Int_t * vCoVals
Definition: pdrInt.h:95
PDR_UND
#define PDR_UND
Definition: pdrTsim.c:31
Pdr_ManSimInfoNot
static int Pdr_ManSimInfoNot(int Value)
Definition: pdrTsim.c:33
toLitCond
static lit toLitCond(int v, int c)
Definition: satVec.h:143
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Pdr_Man_t_::pPars
Pdr_Par_t * pPars
Definition: pdrInt.h:69
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Pdr_Man_t_::vNodes
Vec_Int_t * vNodes
Definition: pdrInt.h:96
PDR_ONE
#define PDR_ONE
Definition: pdrTsim.c:30
Saig_ManLi
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
Pdr_Set_t
typedefABC_NAMESPACE_HEADER_START struct Pdr_Set_t_ Pdr_Set_t
INCLUDES ///.
Definition: pdrInt.h:44
Pdr_ManSimDataInit
int 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)
Definition: pdrTsim.c:161
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Pdr_ManExtendOneEval
int Pdr_ManExtendOneEval(Aig_Man_t *pAig, Aig_Obj_t *pObj)
Definition: pdrTsim.c:130
Pdr_Man_t_::tTsim
abctime tTsim
Definition: pdrInt.h:129
Pdr_Man_t_::vVisits
Vec_Int_t * vVisits
Definition: pdrInt.h:98
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Pdr_ManCollectCone_rec
void Pdr_ManCollectCone_rec(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vCiObjs, Vec_Int_t *vNodes)
FUNCTION DEFINITIONS ///.
Definition: pdrTsim.c:78
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Pdr_Man_t_::vLits
Vec_Int_t * vLits
Definition: pdrInt.h:91
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Pdr_ManSimInfoSet
static void Pdr_ManSimInfoSet(Aig_Man_t *p, Aig_Obj_t *pObj, int Value)
Definition: pdrTsim.c:56
Aig_ObjFaninC1
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
Pdr_ManCollectValues
void Pdr_ManCollectValues(Pdr_Man_t *p, int k, Vec_Int_t *vObjIds, Vec_Int_t *vValues)
Definition: pdrSat.c:232
Aig_ObjId
static int Aig_ObjId(Aig_Obj_t *pObj)
Definition: aig.h:286
Pdr_ManSimInfoGet
static int Pdr_ManSimInfoGet(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: pdrTsim.c:51
assert
#define assert(ex)
Definition: util_old.h:213
Pdr_Man_t_::vCiObjs
Vec_Int_t * vCiObjs
Definition: pdrInt.h:92
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Pdr_ManDeriveResult
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)
Definition: pdrTsim.c:274
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
Pdr_SetIsInit
int Pdr_SetIsInit(Pdr_Set_t *p, int iRemove)
Definition: pdrUtil.c:341
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
Pdr_Man_t_::vUndo
Vec_Int_t * vUndo
Definition: pdrInt.h:97
Pdr_ManTernarySim
Pdr_Set_t * Pdr_ManTernarySim(Pdr_Man_t *p, int k, Pdr_Set_t *pCube)
Definition: pdrTsim.c:351
Pdr_Man_t_::vCoObjs
Vec_Int_t * vCoObjs
Definition: pdrInt.h:93
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Pdr_ManExtendOne
int Pdr_ManExtendOne(Aig_Man_t *pAig, Aig_Obj_t *pObj, Vec_Int_t *vUndo, Vec_Int_t *vVis)
Definition: pdrTsim.c:199
Pdr_ManPrintCex
void Pdr_ManPrintCex(Aig_Man_t *pAig, Vec_Int_t *vCiObjs, Vec_Int_t *vCiVals, Vec_Int_t *vCi2Rem)
Definition: pdrTsim.c:317