abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
bmcInse.c File Reference
#include "bmc.h"
#include "sat/cnf/cnf.h"
#include "sat/bsat/satStore.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 		Gia_ParTestAlloc (Gia_Man_t *p, int nWords)
 DECLARATIONS ///. More...
 
static void Gia_ParTestFree (Gia_Man_t *p)
 
static word * Gia_ParTestObj (Gia_Man_t *p, int Id)
 
void Gia_ManInseInit (Gia_Man_t *p, Vec_Int_t *vInit)
 FUNCTION DEFINITIONS ///. More...
 
void Gia_ManInseSimulateObj (Gia_Man_t *p, int Id)
 
int Gia_ManInseHighestScore (Gia_Man_t *p, int *pCost)
 
void Gia_ManInseFindStarting (Gia_Man_t *p, int iPat, Vec_Int_t *vInit, Vec_Int_t *vInputs)
 
Vec_Int_t * Gia_ManInseSimulate (Gia_Man_t *p, Vec_Int_t *vInit0, Vec_Int_t *vInputs, Vec_Int_t *vInit)
 
Vec_Int_t * Gia_ManInsePerform (Gia_Man_t *p, Vec_Int_t *vInit0, int nFrames, int nWords, int fVerbose)
 
Vec_Int_t * Gia_ManInseTest (Gia_Man_t *p, Vec_Int_t *vInit0, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose)
 

Function Documentation

void Gia_ManInseFindStarting ( Gia_Man_t *  p,
int  iPat,
Vec_Int_t *  vInit,
Vec_Int_t *  vInputs 
)

Definition at line 198 of file bmcInse.c.

199 {
200  Gia_Obj_t * pObj;
201  word * pData0, * pData1;
202  int i, k;
203  Vec_IntClear( vInit );
204  Gia_ManForEachRi( p, pObj, k )
205  {
206  pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
207  pData1 = pData0 + p->iData;
208  for ( i = 0; i < p->iData; i++ )
209  assert( (pData0[i] & pData1[i]) == 0 );
210  if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
211  Vec_IntPush( vInit, 0 );
212  else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
213  Vec_IntPush( vInit, 1 );
214  else
215  Vec_IntPush( vInit, 2 );
216  }
217  Gia_ManForEachPi( p, pObj, k )
218  {
219  pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
220  pData1 = pData0 + p->iData;
221  for ( i = 0; i < p->iData; i++ )
222  assert( (pData0[i] & pData1[i]) == 0 );
223  if ( Abc_InfoHasBit( (unsigned *)pData0, iPat ) )
224  Vec_IntPush( vInputs, 0 );
225  else if ( Abc_InfoHasBit( (unsigned *)pData1, iPat ) )
226  Vec_IntPush( vInputs, 1 );
227  else
228  Vec_IntPush( vInputs, 2 );
229  }
230 }
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Gia_ParTestObj
static word * Gia_ParTestObj(Gia_Man_t *p, int Id)
Definition: bmcInse.c:35
Gia_Obj_t_
Definition: gia.h:75
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_Man_t_::iData
int iData
Definition: gia.h:171
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
int Gia_ManInseHighestScore ( Gia_Man_t *  p,
int *  pCost 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file bmcInse.c.

174 {
175  Gia_Obj_t * pObj;
176  word * pData0, * pData1;
177  int * pCounts, CountBest;
178  int i, k, b, nPats, iPat;
179  nPats = 64 * p->iData;
180  pCounts = ABC_CALLOC( int, nPats );
181  Gia_ManForEachRi( p, pObj, k )
182  {
183  pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
184  pData1 = pData0 + p->iData;
185  for ( i = 0; i < p->iData; i++ )
186  for ( b = 0; b < 64; b++ )
187  pCounts[64*i+b] += (((pData0[i] >> b) & 1) || ((pData1[i] >> b) & 1)); // binary
188  }
189  iPat = 0;
190  CountBest = pCounts[0];
191  for ( k = 1; k < nPats; k++ )
192  if ( CountBest < pCounts[k] )
193  CountBest = pCounts[k], iPat = k;
194  *pCost = Gia_ManRegNum(p) - CountBest; // ternary
195  ABC_FREE( pCounts );
196  return iPat;
197 }
Gia_ParTestObj
static word * Gia_ParTestObj(Gia_Man_t *p, int Id)
Definition: bmcInse.c:35
Gia_Obj_t_
Definition: gia.h:75
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_Man_t_::iData
int iData
Definition: gia.h:171
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Gia_ManInseInit ( Gia_Man_t *  p,
Vec_Int_t *  vInit 
)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 52 of file bmcInse.c.

53 {
54  Gia_Obj_t * pObj;
55  word * pData1, * pData0;
56  int i, k;
57  Gia_ManForEachRi( p, pObj, k )
58  {
59  pData0 = Gia_ParTestObj( p, Gia_ObjId(p, pObj) );
60  pData1 = pData0 + p->iData;
61  if ( Vec_IntEntry(vInit, k) == 0 ) // 0
62  for ( i = 0; i < p->iData; i++ )
63  pData0[i] = ~(word)0, pData1[i] = 0;
64  else if ( Vec_IntEntry(vInit, k) == 1 ) // 1
65  for ( i = 0; i < p->iData; i++ )
66  pData0[i] = 0, pData1[i] = ~(word)0;
67  else // if ( Vec_IntEntry(vInit, k) > 1 ) // X
68  for ( i = 0; i < p->iData; i++ )
69  pData0[i] = pData1[i] = 0;
70  }
71 }
Gia_ParTestObj
static word * Gia_ParTestObj(Gia_Man_t *p, int Id)
Definition: bmcInse.c:35
Gia_Obj_t_
Definition: gia.h:75
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_Man_t_::iData
int iData
Definition: gia.h:171
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Vec_Int_t* Gia_ManInsePerform ( Gia_Man_t *  p,
Vec_Int_t *  vInit0,
int  nFrames,
int  nWords,
int  fVerbose 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 277 of file bmcInse.c.

278 {
279  Vec_Int_t * vRes, * vInit, * vInputs;
280  Gia_Obj_t * pObj;
281  int i, f, iPat, Cost, Cost0;
282  abctime clk, clkTotal = Abc_Clock();
283  Gia_ManRandomW( 1 );
284  if ( fVerbose )
285  printf( "Running with %d frames, %d words, and %sgiven init state.\n", nFrames, nWords, vInit0 ? "":"no " );
286  vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 2 );
287  vInputs = Vec_IntStart( Gia_ManPiNum(p) * nFrames );
288  Gia_ParTestAlloc( p, nWords );
289  Gia_ManInseInit( p, vInit );
290  Cost0 = 0;
291  Vec_IntForEachEntry( vInit, iPat, i )
292  Cost0 += ((iPat >> 1) & 1);
293  if ( fVerbose )
294  printf( "Frame =%6d : Values =%6d (out of %6d)\n", 0, Cost0, Cost0 );
295  for ( f = 0; f < nFrames; f++ )
296  {
297  clk = Abc_Clock();
298  Gia_ManForEachObj( p, pObj, i )
299  Gia_ManInseSimulateObj( p, i );
300  iPat = Gia_ManInseHighestScore( p, &Cost );
301  Gia_ManInseFindStarting( p, iPat, vInit, vInputs );
302  Gia_ManInseInit( p, vInit );
303  if ( fVerbose )
304  printf( "Frame =%6d : Values =%6d (out of %6d) ", f+1, Cost, Cost0 );
305  if ( fVerbose )
306  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
307  }
308  Gia_ParTestFree( p );
309  vRes = Gia_ManInseSimulate( p, vInit0, vInputs, vInit );
310  Vec_IntFreeP( &vInit );
311  Vec_IntFreeP( &vInputs );
312  printf( "After %d frames, found a sequence to produce %d x-values (out of %d). ", f, Cost, Gia_ManRegNum(p) );
313  Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
314  return vRes;
315 }
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_ManInseSimulate
Vec_Int_t * Gia_ManInseSimulate(Gia_Man_t *p, Vec_Int_t *vInit0, Vec_Int_t *vInputs, Vec_Int_t *vInit)
Definition: bmcInse.c:231
Gia_ParTestAlloc
static ABC_NAMESPACE_IMPL_START void Gia_ParTestAlloc(Gia_Man_t *p, int nWords)
DECLARATIONS ///.
Definition: bmcInse.c:33
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_ManInseFindStarting
void Gia_ManInseFindStarting(Gia_Man_t *p, int iPat, Vec_Int_t *vInit, Vec_Int_t *vInputs)
Definition: bmcInse.c:198
nWords
int nWords
Definition: abcNpn.c:127
for
for(p=first;p->value< newval;p=p->next)
Gia_Obj_t_
Definition: gia.h:75
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Gia_ManInseSimulateObj
void Gia_ManInseSimulateObj(Gia_Man_t *p, int Id)
Definition: bmcInse.c:72
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Gia_ManInseHighestScore
int Gia_ManInseHighestScore(Gia_Man_t *p, int *pCost)
Definition: bmcInse.c:173
if
if(last==0)
Definition: sparse_int.h:34
Gia_ManInseInit
void Gia_ManInseInit(Gia_Man_t *p, Vec_Int_t *vInit)
FUNCTION DEFINITIONS ///.
Definition: bmcInse.c:52
Gia_ParTestFree
static void Gia_ParTestFree(Gia_Man_t *p)
Definition: bmcInse.c:34
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition: giaUtil.c:62
runtime
runtime()
Definition: misc/espresso/main.c:568
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Vec_Int_t* Gia_ManInseSimulate ( Gia_Man_t *  p,
Vec_Int_t *  vInit0,
Vec_Int_t *  vInputs,
Vec_Int_t *  vInit 
)

Definition at line 231 of file bmcInse.c.

232 {
233  Vec_Int_t * vRes;
234  Gia_Obj_t * pObj, * pObjRo, * pObjRi;
235  int nFrames = Vec_IntSize(vInputs) / Gia_ManPiNum(p);
236  int i, f, iBit = 0;
237  assert( Vec_IntSize(vInputs) % Gia_ManPiNum(p) == 0 );
238  assert( Vec_IntSize(vInit0) == Gia_ManRegNum(p) );
239  assert( Vec_IntSize(vInit) == Gia_ManRegNum(p) );
240  Gia_ManConst0(p)->fMark0 = 0;
241  Gia_ManForEachRi( p, pObj, i )
242  pObj->fMark0 = Vec_IntEntry(vInit0, i);
243  for ( f = 0; f < nFrames; f++ )
244  {
245  Gia_ManForEachPi( p, pObj, i )
246  pObj->fMark0 = Vec_IntEntry(vInputs, iBit++);
247  Gia_ManForEachAnd( p, pObj, i )
248  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
249  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
250  Gia_ManForEachRi( p, pObj, i )
251  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
252  Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
253  pObjRo->fMark0 = pObjRi->fMark0;
254  }
255  assert( iBit == Vec_IntSize(vInputs) );
256  vRes = Vec_IntAlloc( Gia_ManRegNum(p) );
257  Gia_ManForEachRo( p, pObj, i )
258  assert( Vec_IntEntry(vInit, i) == 2 || Vec_IntEntry(vInit, i) == (int)pObj->fMark0 );
259  Gia_ManForEachRo( p, pObj, i )
260  Vec_IntPush( vRes, pObj->fMark0 | (Vec_IntEntry(vInit, i) != 2 ? 4 : 0) );
261  Gia_ManForEachObj( p, pObj, i )
262  pObj->fMark0 = 0;
263  return vRes;
264 }
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
for
for(p=first;p->value< newval;p=p->next)
Gia_Obj_t_
Definition: gia.h:75
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Gia_ManInseSimulateObj ( Gia_Man_t *  p,
int  Id 
)

Definition at line 72 of file bmcInse.c.

73 {
74  Gia_Obj_t * pObj = Gia_ManObj( p, Id );
75  word * pData0, * pDataA0, * pDataB0;
76  word * pData1, * pDataA1, * pDataB1;
77  int i;
78  if ( Gia_ObjIsAnd(pObj) )
79  {
80  pData0 = Gia_ParTestObj( p, Id );
81  pData1 = pData0 + p->iData;
82  if ( Gia_ObjFaninC0(pObj) )
83  {
84  pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
85  pDataA0 = pDataA1 + p->iData;
86  if ( Gia_ObjFaninC1(pObj) )
87  {
88  pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
89  pDataB0 = pDataB1 + p->iData;
90  }
91  else
92  {
93  pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
94  pDataB1 = pDataB0 + p->iData;
95  }
96  }
97  else
98  {
99  pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
100  pDataA1 = pDataA0 + p->iData;
101  if ( Gia_ObjFaninC1(pObj) )
102  {
103  pDataB1 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
104  pDataB0 = pDataB1 + p->iData;
105  }
106  else
107  {
108  pDataB0 = Gia_ParTestObj( p, Gia_ObjFaninId1(pObj, Id) );
109  pDataB1 = pDataB0 + p->iData;
110  }
111  }
112  for ( i = 0; i < p->iData; i++ )
113  pData0[i] = pDataA0[i] | pDataB0[i], pData1[i] = pDataA1[i] & pDataB1[i];
114  }
115  else if ( Gia_ObjIsCo(pObj) )
116  {
117  pData0 = Gia_ParTestObj( p, Id );
118  pData1 = pData0 + p->iData;
119  if ( Gia_ObjFaninC0(pObj) )
120  {
121  pDataA1 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
122  pDataA0 = pDataA1 + p->iData;
123  }
124  else
125  {
126  pDataA0 = Gia_ParTestObj( p, Gia_ObjFaninId0(pObj, Id) );
127  pDataA1 = pDataA0 + p->iData;
128  }
129  for ( i = 0; i < p->iData; i++ )
130  pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
131  }
132  else if ( Gia_ObjIsCi(pObj) )
133  {
134  if ( Gia_ObjIsPi(p, pObj) )
135  {
136  pData0 = Gia_ParTestObj( p, Id );
137  pData1 = pData0 + p->iData;
138  for ( i = 0; i < p->iData; i++ )
139  pData0[i] = Gia_ManRandomW(0), pData1[i] = ~pData0[i];
140  }
141  else
142  {
143  int Id2 = Gia_ObjId(p, Gia_ObjRoToRi(p, pObj));
144  pData0 = Gia_ParTestObj( p, Id );
145  pData1 = pData0 + p->iData;
146  pDataA0 = Gia_ParTestObj( p, Id2 );
147  pDataA1 = pDataA0 + p->iData;
148  for ( i = 0; i < p->iData; i++ )
149  pData0[i] = pDataA0[i], pData1[i] = pDataA1[i];
150  }
151  }
152  else if ( Gia_ObjIsConst0(pObj) )
153  {
154  pData0 = Gia_ParTestObj( p, Id );
155  pData1 = pData0 + p->iData;
156  for ( i = 0; i < p->iData; i++ )
157  pData0[i] = ~(word)0, pData1[i] = 0;
158  }
159  else assert( 0 );
160 }
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_ParTestObj
static word * Gia_ParTestObj(Gia_Man_t *p, int Id)
Definition: bmcInse.c:35
Gia_Obj_t_
Definition: gia.h:75
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Gia_ManRandomW
word Gia_ManRandomW(int fReset)
Definition: giaUtil.c:62
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
Gia_Man_t_::iData
int iData
Definition: gia.h:171
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Vec_Int_t* Gia_ManInseTest ( Gia_Man_t *  p,
Vec_Int_t *  vInit0,
int  nFrames,
int  nWords,
int  nTimeOut,
int  fSim,
int  fVerbose 
)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 328 of file bmcInse.c.

329 {
330  Vec_Int_t * vRes, * vInit;
331  vInit = Vec_IntAlloc(0); Vec_IntFill( vInit, Gia_ManRegNum(p), 0 );
332  vRes = Gia_ManInsePerform( p, vInit, nFrames, nWords, fVerbose );
333  if ( vInit != vInit0 )
334  Vec_IntFree( vInit );
335  return vRes;
336 }
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
nWords
int nWords
Definition: abcNpn.c:127
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Vec_IntFill
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
Gia_ManInsePerform
Vec_Int_t * Gia_ManInsePerform(Gia_Man_t *p, Vec_Int_t *vInit0, int nFrames, int nWords, int fVerbose)
Definition: bmcInse.c:277
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
static ABC_NAMESPACE_IMPL_START void Gia_ParTestAlloc ( Gia_Man_t *  p,
int  nWords 
)
inlinestatic

DECLARATIONS ///.

CFile****************************************************************

FileName [bmcInse.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
bmcInse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 33 of file bmcInse.c.

33 { assert( !p->pData ); p->pData = (unsigned *)ABC_ALLOC(word, 2*nWords*Gia_ManObjNum(p)); p->iData = nWords; }
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
nWords
int nWords
Definition: abcNpn.c:127
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_Man_t_::pData
void * pData
Definition: gia.h:169
Gia_Man_t_::iData
int iData
Definition: gia.h:171
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static void Gia_ParTestFree ( Gia_Man_t *  p)
inlinestatic

Definition at line 34 of file bmcInse.c.

34 { ABC_FREE( p->pData ); p->iData = 0; }
Gia_Man_t_::pData
void * pData
Definition: gia.h:169
Gia_Man_t_::iData
int iData
Definition: gia.h:171
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
static word* Gia_ParTestObj ( Gia_Man_t *  p,
int  Id 
)
inlinestatic

Definition at line 35 of file bmcInse.c.

35 { return (word *)p->pData + Id*(p->iData << 1); }
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
Gia_Man_t_::pData
void * pData
Definition: gia.h:169
Gia_Man_t_::iData
int iData
Definition: gia.h:171