abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecSeq.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cecSeq.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Combinational equivalence checking.]
8 
9  Synopsis [Refinement of sequential equivalence classes.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cecSeq.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cecInt.h"
22 
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis [Sets register values from the counter-example.]
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
46 {
47  unsigned * pInfo;
48  int k, i, w, nWords;
49  assert( pCex->nBits == pCex->nRegs + pCex->nPis * (pCex->iFrame + 1) );
50  assert( pCex->nBits - pCex->nRegs + Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
51  nWords = Vec_PtrReadWordsSimInfo( vInfo );
52 /*
53  // user register values
54  assert( pCex->nRegs == Gia_ManRegNum(pAig) );
55  for ( k = 0; k < pCex->nRegs; k++ )
56  {
57  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
58  for ( w = 0; w < nWords; w++ )
59  pInfo[w] = Abc_InfoHasBit( pCex->pData, k )? ~0 : 0;
60  }
61 */
62  // print warning about register values
63  for ( k = 0; k < pCex->nRegs; k++ )
64  if ( Abc_InfoHasBit( pCex->pData, k ) )
65  break;
66  if ( k < pCex->nRegs )
67  Abc_Print( 0, "The CEX has flop values different from 0, but they are currently not used by \"resim\".\n" );
68 
69  // assign zero register values
70  for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
71  {
72  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
73  for ( w = 0; w < nWords; w++ )
74  pInfo[w] = 0;
75  }
76  for ( i = pCex->nRegs; i < pCex->nBits; i++ )
77  {
78  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k++ );
79  for ( w = 0; w < nWords; w++ )
80  pInfo[w] = Gia_ManRandom(0);
81  // set simulation pattern and make sure it is second (first will be erased during simulation)
82  pInfo[0] = (pInfo[0] << 1) | Abc_InfoHasBit( pCex->pData, i );
83  pInfo[0] <<= 1;
84  }
85  for ( ; k < Vec_PtrSize(vInfo); k++ )
86  {
87  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
88  for ( w = 0; w < nWords; w++ )
89  pInfo[w] = Gia_ManRandom(0);
90  }
91 }
92 
93 /**Function*************************************************************
94 
95  Synopsis [Sets register values from the counter-example.]
96 
97  Description []
98 
99  SideEffects []
100 
101  SeeAlso []
102 
103 ***********************************************************************/
105 {
106  unsigned * pInfo;
107  int k, w, nWords;
108  nWords = Vec_PtrReadWordsSimInfo( vInfo );
109  assert( pCex == NULL || Gia_ManRegNum(pAig) == pCex->nRegs );
110  assert( Gia_ManRegNum(pAig) <= Vec_PtrSize(vInfo) );
111  for ( k = 0; k < Gia_ManRegNum(pAig); k++ )
112  {
113  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
114  for ( w = 0; w < nWords; w++ )
115  pInfo[w] = (pCex && Abc_InfoHasBit(pCex->pData, k))? ~0 : 0;
116  }
117 
118  for ( ; k < Vec_PtrSize(vInfo); k++ )
119  {
120  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
121  for ( w = 0; w < nWords; w++ )
122  pInfo[w] = Gia_ManRandom( 0 );
123  }
124 }
125 
126 /**Function*************************************************************
127 
128  Synopsis [Resimulates the classes using sequential simulation info.]
129 
130  Description []
131 
132  SideEffects []
133 
134  SeeAlso []
135 
136 ***********************************************************************/
138 {
139  unsigned * pInfo0, * pInfo1;
140  int f, i, k, w;
141 // assert( Gia_ManRegNum(p->pAig) > 0 );
142  assert( Vec_PtrSize(vInfo) == Gia_ManRegNum(p->pAig) + Gia_ManPiNum(p->pAig) * p->pPars->nFrames );
143  for ( k = 0; k < Gia_ManRegNum(p->pAig); k++ )
144  {
145  pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k );
146  pInfo1 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + k );
147  for ( w = 0; w < p->nWords; w++ )
148  pInfo1[w] = pInfo0[w];
149  }
150  for ( f = 0; f < p->pPars->nFrames; f++ )
151  {
152  for ( i = 0; i < Gia_ManPiNum(p->pAig); i++ )
153  {
154  pInfo0 = (unsigned *)Vec_PtrEntry( vInfo, k++ );
155  pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, i );
156  for ( w = 0; w < p->nWords; w++ )
157  pInfo1[w] = pInfo0[w];
158  }
159  for ( i = 0; i < Gia_ManRegNum(p->pAig); i++ )
160  {
161  pInfo0 = (unsigned *)Vec_PtrEntry( p->vCoSimInfo, Gia_ManPoNum(p->pAig) + i );
162  pInfo1 = (unsigned *)Vec_PtrEntry( p->vCiSimInfo, Gia_ManPiNum(p->pAig) + i );
163  for ( w = 0; w < p->nWords; w++ )
164  pInfo1[w] = pInfo0[w];
165  }
166  if ( Cec_ManSimSimulateRound( p, p->vCiSimInfo, p->vCoSimInfo ) )
167  return 1;
168  }
169  assert( k == Vec_PtrSize(vInfo) );
170  return 0;
171 }
172 
173 /**Function*************************************************************
174 
175  Synopsis [Resimulates information to refine equivalence classes.]
176 
177  Description []
178 
179  SideEffects []
180 
181  SeeAlso []
182 
183 ***********************************************************************/
184 int Cec_ManSeqResimulateInfo( Gia_Man_t * pAig, Vec_Ptr_t * vSimInfo, Abc_Cex_t * pBestState, int fCheckMiter )
185 {
186  Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
187  Cec_ManSim_t * pSim;
188  int RetValue;//, clkTotal = Abc_Clock();
189  assert( (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) % Gia_ManPiNum(pAig) == 0 );
190  Cec_ManSimSetDefaultParams( pParsSim );
191  pParsSim->nFrames = (Vec_PtrSize(vSimInfo) - Gia_ManRegNum(pAig)) / Gia_ManPiNum(pAig);
192  pParsSim->nWords = Vec_PtrReadWordsSimInfo( vSimInfo );
193  pParsSim->fCheckMiter = fCheckMiter;
194  Gia_ManCreateValueRefs( pAig );
195  pSim = Cec_ManSimStart( pAig, pParsSim );
196  if ( pBestState )
197  pSim->pBestState = pBestState;
198  RetValue = Cec_ManSeqResimulate( pSim, vSimInfo );
199  pSim->pBestState = NULL;
200  Cec_ManSimStop( pSim );
201  return RetValue;
202 }
203 
204 /**Function*************************************************************
205 
206  Synopsis [Resimuates one counter-example to refine equivalence classes.]
207 
208  Description []
209 
210  SideEffects []
211 
212  SeeAlso []
213 
214 ***********************************************************************/
216 {
217  Vec_Ptr_t * vSimInfo;
218  int RetValue;
219  abctime clkTotal = Abc_Clock();
220  if ( pCex == NULL )
221  {
222  Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Counter-example is not available.\n" );
223  return -1;
224  }
225  if ( pAig->pReprs == NULL )
226  {
227  Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Equivalence classes are not available.\n" );
228  return -1;
229  }
230  if ( Gia_ManRegNum(pAig) == 0 )
231  {
232  Abc_Print( 1, "Cec_ManSeqResimulateCounter(): Not a sequential AIG.\n" );
233  return -1;
234  }
235 // if ( Gia_ManRegNum(pAig) != pCex->nRegs || Gia_ManPiNum(pAig) != pCex->nPis )
236  if ( Gia_ManPiNum(pAig) != pCex->nPis )
237  {
238  Abc_Print( 1, "Cec_ManSeqResimulateCounter(): The number of PIs in the AIG and the counter-example differ.\n" );
239  return -1;
240  }
241  if ( pPars->fVerbose )
242  Abc_Print( 1, "Resimulating %d timeframes.\n", pPars->nFrames + pCex->iFrame + 1 );
243  Gia_ManRandom( 1 );
244  vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
245  Gia_ManPiNum(pAig) * (pPars->nFrames + pCex->iFrame + 1), 1 );
246  Cec_ManSeqDeriveInfoFromCex( vSimInfo, pAig, pCex );
247  if ( pPars->fVerbose )
248  Gia_ManEquivPrintClasses( pAig, 0, 0 );
249  RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, NULL, pPars->fCheckMiter );
250  if ( pPars->fVerbose )
251  Gia_ManEquivPrintClasses( pAig, 0, 0 );
252  Vec_PtrFree( vSimInfo );
253  if ( pPars->fVerbose )
254  ABC_PRT( "Time", Abc_Clock() - clkTotal );
255 // if ( RetValue && pPars->fCheckMiter )
256 // Abc_Print( 1, "Cec_ManSeqResimulateCounter(): An output of the miter is asserted!\n" );
257  return RetValue;
258 }
259 
260 
261 /**Function*************************************************************
262 
263  Synopsis [Returns the number of POs that are not const0 cands.]
264 
265  Description []
266 
267  SideEffects []
268 
269  SeeAlso []
270 
271 ***********************************************************************/
273 {
274  Gia_Obj_t * pObj;
275  int i, Counter = 0;
276  if ( pAig->pReprs == NULL )
277  return -1;
278  Gia_ManForEachPo( pAig, pObj, i )
279  if ( !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, pObj) ) )
280  Counter++;
281  return Counter;
282 }
283 
284 /**Function*************************************************************
285 
286  Synopsis [Returns the number of POs that are not const0 cands.]
287 
288  Description []
289 
290  SideEffects []
291 
292  SeeAlso []
293 
294 ***********************************************************************/
296 {
297  Gia_Obj_t * pObj;
298  int i, RetValue = 0;
299  if ( pAig->pReprs == NULL )
300  return 0;
301  // label internal nodes driving POs
302  Gia_ManForEachPo( pAig, pObj, i )
303  Gia_ObjFanin0(pObj)->fMark0 = 1;
304  // check if there are non-labled equivs
305  Gia_ManForEachObj( pAig, pObj, i )
306  if ( Gia_ObjIsCand(pObj) && !pObj->fMark0 && Gia_ObjRepr(pAig, i) != GIA_VOID )
307  {
308  RetValue = 1;
309  break;
310  }
311  // clean internal nodes driving POs
312  Gia_ManForEachPo( pAig, pObj, i )
313  Gia_ObjFanin0(pObj)->fMark0 = 0;
314  return RetValue;
315 }
316 
317 /**Function*************************************************************
318 
319  Synopsis [Performs semiformal refinement of equivalence classes.]
320 
321  Description []
322 
323  SideEffects []
324 
325  SeeAlso []
326 
327 ***********************************************************************/
329 {
330  int nAddFrames = 16; // additional timeframes to simulate
331  int nCountNoRef = 0;
332  int nFramesReal;
333  Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
334  Vec_Ptr_t * vSimInfo;
335  Vec_Str_t * vStatus;
336  Abc_Cex_t * pState;
337  Gia_Man_t * pSrm, * pReduce, * pAux;
338  int r, nPats, RetValue = 0;
339  if ( pAig->pReprs == NULL )
340  {
341  Abc_Print( 1, "Cec_ManSeqSemiformal(): Equivalence classes are not available.\n" );
342  return -1;
343  }
344  if ( Gia_ManRegNum(pAig) == 0 )
345  {
346  Abc_Print( 1, "Cec_ManSeqSemiformal(): Not a sequential AIG.\n" );
347  return -1;
348  }
349  Gia_ManRandom( 1 );
350  // prepare starting pattern
351  pState = Abc_CexAlloc( Gia_ManRegNum(pAig), 0, 0 );
352  pState->iFrame = -1;
353  pState->iPo = -1;
354  // prepare SAT solving
355  Cec_ManSatSetDefaultParams( pParsSat );
356  pParsSat->nBTLimit = pPars->nBTLimit;
357  pParsSat->fVerbose = pPars->fVerbose;
358  if ( pParsSat->fVerbose )
359  {
360  Abc_Print( 1, "Starting: " );
361  Gia_ManEquivPrintClasses( pAig, 0, 0 );
362  }
363  // perform the given number of BMC rounds
364  Gia_ManCleanMark0( pAig );
365  for ( r = 0; r < pPars->nRounds; r++ )
366  {
367  if ( !Cec_ManCheckNonTrivialCands(pAig) )
368  {
369  Abc_Print( 1, "Cec_ManSeqSemiformal: There are only trivial equiv candidates left (PO drivers). Quitting.\n" );
370  break;
371  }
372 // Abc_CexPrint( pState );
373  // derive speculatively reduced model
374 // pSrm = Gia_ManSpecReduceInit( pAig, pState, pPars->nFrames, pPars->fDualOut );
375  pSrm = Gia_ManSpecReduceInitFrames( pAig, pState, pPars->nFrames, &nFramesReal, pPars->fDualOut, pPars->nMinOutputs );
376  if ( pSrm == NULL )
377  {
378  Abc_Print( 1, "Quitting refinement because miter could not be unrolled.\n" );
379  break;
380  }
381  assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == (Gia_ManPiNum(pAig) * nFramesReal) );
382  if ( pPars->fVerbose )
383  Abc_Print( 1, "Unrolled for %d frames.\n", nFramesReal );
384  // allocate room for simulation info
385  vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pAig) +
386  Gia_ManPiNum(pAig) * (nFramesReal + nAddFrames), pPars->nWords );
387  Cec_ManSeqDeriveInfoInitRandom( vSimInfo, pAig, pState );
388  // fill in simulation info with counter-examples
389  vStatus = Cec_ManSatSolveSeq( vSimInfo, pSrm, pParsSat, Gia_ManRegNum(pAig), &nPats );
390  Vec_StrFree( vStatus );
391  Gia_ManStop( pSrm );
392  // resimulate and refine the classes
393  RetValue = Cec_ManSeqResimulateInfo( pAig, vSimInfo, pState, pPars->fCheckMiter );
394  Vec_PtrFree( vSimInfo );
395  assert( pState->iPo >= 0 ); // hit counter
396  pState->iPo = -1;
397  if ( pPars->fVerbose )
398  {
399  Abc_Print( 1, "BMC = %3d ", nPats );
400  Gia_ManEquivPrintClasses( pAig, 0, 0 );
401  }
402 
403  // write equivalence classes
404  Gia_AigerWrite( pAig, "gore.aig", 0, 0 );
405  // reduce the model
406  pReduce = Gia_ManSpecReduce( pAig, 0, 0, 1, 0, 0 );
407  if ( pReduce )
408  {
409  pReduce = Gia_ManSeqStructSweep( pAux = pReduce, 1, 1, 0 );
410  Gia_ManStop( pAux );
411  Gia_AigerWrite( pReduce, "gsrm.aig", 0, 0 );
412 // Abc_Print( 1, "Speculatively reduced model was written into file \"%s\".\n", "gsrm.aig" );
413 // Gia_ManPrintStatsShort( pReduce );
414  Gia_ManStop( pReduce );
415  }
416 
417  if ( RetValue )
418  {
419  Abc_Print( 1, "Cec_ManSeqSemiformal(): An output of the miter is asserted. Refinement stopped.\n" );
420  break;
421  }
422  // decide when to stop
423  if ( nPats > 0 )
424  nCountNoRef = 0;
425  else if ( ++nCountNoRef == pPars->nNonRefines )
426  break;
427  }
428  ABC_FREE( pState );
429  if ( pPars->fCheckMiter )
430  {
431  int nNonConsts = Cec_ManCountNonConstOutputs( pAig );
432  if ( nNonConsts )
433  Abc_Print( 1, "The number of POs that are not const-0 candidates = %d.\n", nNonConsts );
434  }
435  return RetValue;
436 }
437 
438 //&r s13207.aig; &ps; &equiv; &ps; &semi -R 2 -vm
439 //&r bug/50/temp.aig; &ps; &equiv -smv; &semi -v
440 //r mentor/1_05c.blif; st; &get; &ps; &equiv -smv; &semi -mv
441 //&r bug/50/hdl1.aig; &ps; &equiv -smv; &semi -mv; &srm; &r gsrm.aig; &ps
442 
443 ////////////////////////////////////////////////////////////////////////
444 /// END OF FILE ///
445 ////////////////////////////////////////////////////////////////////////
446 
447 
449 
int fVerbose
Definition: cec.h:73
Gia_Man_t * Gia_ManSpecReduce(Gia_Man_t *p, int fDualOut, int fSynthesis, int fReduce, int fSkipSome, int fVerbose)
Definition: giaEquiv.c:848
int nFrames
Definition: cec.h:82
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
static int Gia_ObjIsCand(Gia_Obj_t *pObj)
Definition: gia.h:429
int nRounds
Definition: cec.h:81
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
int Cec_ManSimSimulateRound(Cec_ManSim_t *p, Vec_Ptr_t *vInfoCis, Vec_Ptr_t *vInfoCos)
Definition: cecClass.c:652
void Cec_ManSimStop(Cec_ManSim_t *p)
Definition: cecMan.c:232
Gia_Man_t * pAig
Definition: cecInt.h:115
ABC_NAMESPACE_IMPL_START void Cec_ManSeqDeriveInfoFromCex(Vec_Ptr_t *vInfo, Gia_Man_t *pAig, Abc_Cex_t *pCex)
DECLARATIONS ///.
Definition: cecSeq.c:45
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
int nWords
Definition: abcNpn.c:127
Definition: gia.h:75
int fCheckMiter
Definition: cec.h:67
void Gia_ManEquivPrintClasses(Gia_Man_t *p, int fVerbose, float Mem)
Definition: giaEquiv.c:304
Cec_ManSim_t * Cec_ManSimStart(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecMan.c:198
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
int Cec_ManSeqResimulateInfo(Gia_Man_t *pAig, Vec_Ptr_t *vSimInfo, Abc_Cex_t *pBestState, int fCheckMiter)
Definition: cecSeq.c:184
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition: cecCore.c:70
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
int Cec_ManSeqResimulate(Cec_ManSim_t *p, Vec_Ptr_t *vInfo)
Definition: cecSeq.c:137
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t * Gia_ManSpecReduceInitFrames(Gia_Man_t *p, Abc_Cex_t *pInit, int nFramesMax, int *pnFrames, int fDualOut, int nMinOutputs)
Definition: giaEquiv.c:1075
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
int nWords
Definition: cecInt.h:117
int nBTLimit
Definition: cec.h:85
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_Ptr_t * vCiSimInfo
Definition: cecInt.h:127
void Cec_ManSeqDeriveInfoInitRandom(Vec_Ptr_t *vInfo, Gia_Man_t *pAig, Abc_Cex_t *pCex)
Definition: cecSeq.c:104
Gia_Man_t * Gia_ManSeqStructSweep(Gia_Man_t *p, int fConst, int fEquiv, int fVerbose)
Definition: giaScl.c:258
static int Counter
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact)
Definition: giaAiger.c:1024
int fVerbose
Definition: cec.h:90
#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 int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
int fCheckMiter
Definition: cec.h:88
#define GIA_VOID
Definition: gia.h:45
int nWords
Definition: cec.h:80
int nFrames
Definition: cec.h:62
unsigned fMark0
Definition: gia.h:79
#define ABC_FREE(obj)
Definition: abc_global.h:232
Definition: gia.h:95
#define ABC_PRT(a, t)
Definition: abc_global.h:220
int fDualOut
Definition: cec.h:87
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Cec_ParSim_t * pPars
Definition: cecInt.h:116
int Cec_ManCheckNonTrivialCands(Gia_Man_t *pAig)
Definition: cecSeq.c:295
Vec_Str_t * Cec_ManSatSolveSeq(Vec_Ptr_t *vPatts, Gia_Man_t *pAig, Cec_ParSat_t *pPars, int nRegs, int *pnPats)
Definition: cecSolve.c:867
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
Vec_Ptr_t * vCoSimInfo
Definition: cecInt.h:128
int Cec_ManSeqResimulateCounter(Gia_Man_t *pAig, Cec_ParSim_t *pPars, Abc_Cex_t *pCex)
Definition: cecSeq.c:215
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
Gia_Rpr_t * pReprs
Definition: gia.h:121
int nMinOutputs
Definition: cec.h:84
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
int nNonRefines
Definition: cec.h:83
Abc_Cex_t * pBestState
Definition: cecInt.h:134
int nWords
Definition: cec.h:61
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
ABC_INT64_T abctime
Definition: abc_global.h:278
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
int Cec_ManSeqSemiformal(Gia_Man_t *pAig, Cec_ParSmf_t *pPars)
Definition: cecSeq.c:328
int Cec_ManCountNonConstOutputs(Gia_Man_t *pAig)
Definition: cecSeq.c:272
void Cec_ManSatSetDefaultParams(Cec_ParSat_t *p)
DECLARATIONS ///.
Definition: cecCore.c:45
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387