source: vis_dev/vis-2.3/src/puresat/puresatTFrame.c @ 82

Last change on this file since 82 was 14, checked in by cecile, 14 years ago

vis2.3
File size: 39.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [puresatTFrame.c]
4
5  PackageName [puresat]
6
7  Synopsis    [Abstraction refinement for large scale invariant checking.]
8
9  Description [This file contains the functions to check invariant properties
10  by the PureSAT abstraction refinement algorithm, which is entirely based on
11  SAT solver, the input of which could be either CNF or AIG. It has several
12  parts:
13
14  * Localization-reduction base Abstraction
15  * K-induction or interpolation to prove the truth of a property
16  * Bounded Model Checking to find bugs
17  * Incremental concretization based methods to verify abstract bugs
18  * Incremental SAT solver to improve efficiency
19  * UNSAT proof based method to obtain refinement
20  * AROSAT to bring in only necessary latches into unsat proofs
21  * Bridge abstraction to get compact coarse refinement
22  * Refinement minization to guarrantee minimal refinements
23  * Unsat proof-based refinement minimization to eliminate multiple candidate
24    by on SAT test
25  * Refinement prediction to decrease the number of refinement iterations
26  * Dynamic switching to redistribute computional resources to improve
27    efficiency
28
29  For more information, please check the BMC'03, ICCAD'04, STTT'05 and TACAS'05
30  paper of Li et al., "A satisfiability-based appraoch to abstraction
31  refinement in model checking", " Abstraction in symbolic model checking
32  using satisfiability as the only decision procedure", "Efficient computation
33  of small abstraction refinements", and "Efficient abstraction refinement in
34  interpolation-based unbounded model checking"]
35
36  Author      [Bing Li]
37
38  Copyright   [Copyright (c) 2004 The Regents of the Univ. of Colorado.
39  All rights reserved.
40
41  Permission is hereby granted, without written agreement and without
42  license or royalty fees, to use, copy, modify, and distribute this
43  software and its documentation for any purpose, provided that the
44  above copyright notice and the following two paragraphs appear in
45  all copies of this software.]
46
47******************************************************************************/
48#include "puresatInt.h"
49
50
51/*---------------------------------------------------------------------------*/
52/* Constant declarations                                                     */
53/*---------------------------------------------------------------------------*/
54
55/*---------------------------------------------------------------------------*/
56/* Structure declarations                                                    */
57/*---------------------------------------------------------------------------*/
58
59/*---------------------------------------------------------------------------*/
60/* Type declarations                                                         */
61/*---------------------------------------------------------------------------*/
62
63/*---------------------------------------------------------------------------*/
64/* Variable declarations                                                     */
65/*---------------------------------------------------------------------------*/
66
67/*---------------------------------------------------------------------------*/
68/* Macro declarations                                                        */
69/*---------------------------------------------------------------------------*/
70
71/**AutomaticStart*************************************************************/
72
73/*---------------------------------------------------------------------------*/
74/* Static function prototypes                                                */
75/*---------------------------------------------------------------------------*/
76
77static int nameCompare(const void * node1, const void * node2);
78static int NoOfBitEncode( int n);
79
80
81/**AutomaticEnd***************************************************************/
82
83/*---------------------------------------------------------------------------*/
84/* Definition of exported functions                                          */
85/*---------------------------------------------------------------------------*/
86
87/**Function********************************************************************
88
89  Synopsis    [build conncetion between binary variables and
90               multi-valued variables]
91
92  Description []
93
94  SideEffects []
95
96  SeeAlso     []
97
98******************************************************************************/
99
100bAigEdge_t
101PureSat_CaseNew(mAig_Manager_t *manager,
102  bAigEdge_t      *arr,
103  array_t *       encodeList,
104  int             index)
105{
106  int encodeLen;
107  int i, count;
108  bAigEdge_t v;
109  bAigEdge_t    andResult1, andResult2, orResult, result;
110  bAigEdge_t    node1, node2;
111  array_t *newEncodeList;
112
113  encodeLen = array_n(encodeList);
114  if (encodeLen == 1)
115    return array_fetch(bAigEdge_t, encodeList, 0);
116  newEncodeList =  array_alloc(bAigEdge_t, 0);
117
118  v = arr[index];
119  count = 0;
120  for (i=0; i< (encodeLen/2); i++){
121    node1 = array_fetch(bAigEdge_t, encodeList, count++);
122    node2 = array_fetch(bAigEdge_t, encodeList, count++);
123
124     /*  performs ITE operator */
125    andResult1 = PureSat_And(manager, v,           node2);
126    andResult2 = PureSat_And(manager, bAig_Not(v), node1);
127    orResult   = PureSat_Or (manager, andResult1,  andResult2);
128    flags(andResult1) |= IsSystemMask;
129    flags(andResult2) |= IsSystemMask;
130    flags(orResult) |= IsSystemMask;
131
132    array_insert_last(bAigEdge_t, newEncodeList, orResult);
133  }
134
135  if(encodeLen%2){
136    node1 = array_fetch(bAigEdge_t, encodeList, count);
137    array_insert_last(bAigEdge_t, newEncodeList, node1);
138  }
139
140  result = PureSat_CaseNew(manager, arr, newEncodeList, index-1);
141  array_free(newEncodeList);
142  return(result);
143}
144
145/**Function********************************************************************
146
147  Synopsis    [Create new aig node in expanding timeframes with initial states]
148
149  Description []
150
151  SideEffects []
152
153  SeeAlso     []
154
155******************************************************************************/
156
157
158void PureSat_CreateNewNode(
159        mAig_Manager_t *manager,
160        st_table *node2MvfAigTable,
161        Ntk_Node_t *node,
162        bAigEdge_t *bli,
163        bAigEdge_t *li,
164        int *bindex,
165        int *index,
166        int withInitialState)
167{
168  int i, j, value, noBits;
169  bAigEdge_t *arr, v, tv;
170  MvfAig_Function_t  *mvfAig;
171  array_t *encodeList;
172  bAigEdge_t *ManagerNodesArray;
173  bAigTimeFrame_t *timeframe;
174
175
176  if(withInitialState)
177    timeframe = manager->timeframe;
178  else
179    timeframe = manager->timeframeWOI;
180
181  value = Var_VariableReadNumValues(Ntk_NodeReadVariable(node));
182  noBits = NoOfBitEncode(value);
183  arr = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*noBits);
184  mvfAig = 0;
185  st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
186  for(i=0; i<noBits; i++) {
187    arr[i] = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
188    bli[(*bindex)++] = arr[i];
189
190    flags(arr[i]) |= IsSystemMask;
191  }
192
193  for(i=0; i<value; i++) {
194    v = MvfAig_FunctionReadComponent(mvfAig, i);
195
196    encodeList = array_alloc(bAigEdge_t, 0);
197    for(j=0; j<value; j++) {
198      if(j == i)array_insert_last(bAigEdge_t, encodeList, mAig_One);
199      else      array_insert_last(bAigEdge_t, encodeList, mAig_Zero);
200    }
201    tv = PureSat_CaseNew(manager, arr, encodeList, noBits-1);
202    li[(*index)++] = tv;
203
204    ManagerNodesArray = manager->NodesArray;
205
206    array_free(encodeList);
207    if(v == bAig_Zero){
208      flags(tv) |= StaticLearnMask;
209      if(timeframe->assertedArray == 0)
210        timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
211      array_insert_last(bAigEdge_t, timeframe->assertedArray, bAig_Not(tv));
212    }
213    else if(v == bAig_One){
214      flags(tv) |= StaticLearnMask;
215      if(timeframe->assertedArray == 0)
216        timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
217      array_insert_last(bAigEdge_t, timeframe->assertedArray, tv);
218    }
219  }
220  free(arr);
221}
222
223/**Function********************************************************************
224
225  Synopsis    [Build timeframed coi for each variable]
226
227  Description []
228
229  SideEffects []
230
231  SeeAlso     []
232
233******************************************************************************/
234
235
236bAigEdge_t
237PureSat_ExpandForEachCone(
238        mAig_Manager_t *manager,
239        bAigEdge_t v,
240        st_table *old2new)
241{
242  bAigEdge_t left, right, nv;
243
244  v = bAig_GetCanonical(manager, v);
245  if(v == bAig_One || v == bAig_Zero)   return(v);
246  if(v == bAig_NULL)    {
247      fprintf(vis_stdout, "current error\n");
248      return(v);
249  }
250
251
252  if(st_lookup(old2new, (char *)v, &nv))
253    return(nv);
254  if(st_lookup(old2new, (char *)bAig_Not(v), &nv))
255    return(bAig_Not(nv));
256
257  left = PureSat_ExpandForEachCone(manager, leftChild(v), old2new);
258  right = PureSat_ExpandForEachCone(manager, rightChild(v), old2new);
259
260  nv = PureSat_And(manager, left, right);
261
262  flags(nv) |= IsSystemMask;
263
264  if(bAig_IsInverted(v))        nv = bAig_Not(nv);
265  st_insert(old2new, (char *)v, (char *)nv);
266
267
268  return(nv);
269
270}
271
272/**Function********************************************************************
273
274  Synopsis    [Initialize aig timeframes]
275
276  Description []
277
278  SideEffects []
279
280  SeeAlso     []
281
282******************************************************************************/
283
284bAigTimeFrame_t *
285bAig_PureSat_InitTimeFrame(
286        Ntk_Network_t *network,
287        mAig_Manager_t *manager,
288        PureSat_Manager_t *pm,
289        int withInitialState)
290{
291bAigTimeFrame_t *timeframe;
292array_t *latchArr, *inputArr, *outputArr;
293array_t *iindexArray;
294st_table   *li2index, *o2index, *i2index, *pi2index;
295st_table   *bli2index, *bpi2index;
296Ntk_Node_t *node, *latch;
297st_table   *node2MvfAigTable, *old2new;
298lsGen gen;
299int nLatches, nInputs, nOutputs, nInternals;
300int nbLatches, nbInputs;
301int i;
302int index, index1, mvfSize, lmvfSize;
303int bindex, tindex, tindex1;
304MvfAig_Function_t  *mvfAig, *tmpMvfAig, *lmvfAig;
305bAigEdge_t *li, *pre_li, *ori_li;
306bAigEdge_t *bli, *ori_bli;
307bAigEdge_t v, nv;
308mAigMvar_t mVar;
309mAigBvar_t bVar;
310array_t   *bVarList, *mVarList;
311int mAigId;
312int lmAigId;
313mAigMvar_t lmVar;
314mAigBvar_t lbVar;
315
316bAigEdge_t vi, tmpv1, tmpv2,tmpv3;
317char * name, *name1;
318int imvfSize;
319st_table *idx2name,*MultiLatchTable,*table;
320
321  manager->class_ = 1;
322
323  node2MvfAigTable =
324        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
325
326  timeframe = ALLOC(bAigTimeFrame_t, 1);
327  memset(timeframe, 0, sizeof(bAigTimeFrame_t));
328  if(withInitialState) manager->timeframe = timeframe;
329  else                 manager->timeframeWOI = timeframe;
330
331  latchArr = array_alloc(Ntk_Node_t *, 0);
332  inputArr = array_alloc(Ntk_Node_t *, 0);
333  outputArr = array_alloc(Ntk_Node_t *, 0);
334  timeframe->latchArr = latchArr;
335  timeframe->inputArr = inputArr;
336  timeframe->outputArr = outputArr;
337
338  li2index = st_init_table(st_ptrcmp, st_ptrhash);
339  o2index = st_init_table(st_ptrcmp, st_ptrhash);
340  i2index = st_init_table(st_ptrcmp, st_ptrhash);
341  pi2index = st_init_table(st_ptrcmp, st_ptrhash);
342
343  bli2index = st_init_table(st_ptrcmp, st_ptrhash);
344  bpi2index = st_init_table(st_ptrcmp, st_ptrhash);
345
346  idx2name = st_init_table(st_ptrcmp,st_ptrhash);
347  timeframe->idx2name = idx2name;
348  MultiLatchTable = st_init_table(st_ptrcmp,st_ptrhash);
349  timeframe->MultiLatchTable = MultiLatchTable;
350
351  timeframe->li2index = li2index;
352  timeframe->o2index = o2index;
353  timeframe->pi2index = pi2index;
354  timeframe->i2index = i2index;
355
356  timeframe->bli2index = bli2index;
357  timeframe->bpi2index = bpi2index;
358  /**
359   * count total number,
360   * insert into node array
361   * and make table for bAigEdge_t to index
362   **/
363
364  bVarList = mAigReadBinVarList(manager);
365  mVarList = mAigReadMulVarList(manager);
366
367  nLatches = 0;
368  nbLatches = 0;
369  Ntk_NetworkForEachLatch(network, gen, latch) {
370
371    name = Ntk_NodeReadName(latch);
372    array_insert_last(Ntk_Node_t *, latchArr, latch);
373    st_lookup(node2MvfAigTable, (char *)latch, &mvfAig);
374    mvfSize = array_n(mvfAig);
375    for(i=0; i< mvfSize; i++){
376      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
377      st_insert(li2index, (char *)v, (char *)(long)nLatches++);
378
379#ifdef TIMEFRAME_VERIFY_
380      fprintf(vis_stdout,"Latch:%s v-->idx:%d-->%d\n",name,v,nLatches-1);
381#endif
382    }
383
384
385    mAigId = Ntk_NodeReadMAigId(latch);
386    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
387    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
388      bVar = array_fetch(mAigBvar_t, bVarList, index1);
389      st_insert(bli2index, (char *)bVar.node, (char *)(long)nbLatches++);
390      index1++;
391    }
392  }
393  timeframe->nLatches = nLatches;
394  timeframe->nbLatches = nbLatches;
395
396  nOutputs = 0;
397  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
398    array_insert_last(Ntk_Node_t *, outputArr, node);
399    st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
400    mvfSize = array_n(mvfAig);
401    for(i=0; i< mvfSize; i++){
402      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
403      st_insert(o2index, (char *)v, (char *)(long)nOutputs++);
404    }
405  }
406  timeframe->nOutputs = nOutputs;
407
408  timeframe->iindexArray = iindexArray = array_alloc(bAigEdge_t, 0);
409  nInternals = 0;
410  Ntk_NetworkForEachNode(network, gen, node) {
411    if(Ntk_NodeTestIsShadow(node))      continue;
412    if(Ntk_NodeTestIsCombInput(node))   continue;
413    if(Ntk_NodeTestIsCombOutput(node))continue;
414    if(!st_lookup(node2MvfAigTable, (char *)node, &mvfAig)) {
415      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
416      array_free(tmpMvfAig);
417      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
418    }
419    mvfSize = array_n(mvfAig);
420    for(i=0; i< mvfSize; i++){
421      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
422      if(!st_lookup(i2index, (char *)v, &index1)) {
423        array_insert_last(bAigEdge_t, iindexArray, v);
424        st_insert(i2index, (char *)v, (char *)(long)nInternals++);
425      }
426    }
427  }
428  timeframe->nInternals = nInternals;
429
430  nInputs = 0;
431  nbInputs = 0;
432  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
433    array_insert_last(Ntk_Node_t *, inputArr, node);
434    if(!st_lookup(node2MvfAigTable, (char *)node, &mvfAig)) {
435      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
436      array_free(tmpMvfAig);
437      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
438    }
439    mvfSize = array_n(mvfAig);
440    for(i=0; i< mvfSize; i++){
441      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
442        st_insert(pi2index, (char *)v, (char *)(long)nInputs++);
443    }
444
445    mAigId = Ntk_NodeReadMAigId(node);
446    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
447    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
448      bVar = array_fetch(mAigBvar_t, bVarList, index1);
449      st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
450      index1++;
451    }
452  }
453  Ntk_NetworkForEachPseudoInput(network, gen, node)  {
454    array_insert_last(Ntk_Node_t *, inputArr, node);
455    if(!st_lookup(node2MvfAigTable, (char *)node, &mvfAig)) {
456      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
457      array_free(tmpMvfAig);
458      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
459    }
460    mvfSize = array_n(mvfAig);
461    for(i=0; i< mvfSize; i++){
462      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
463        st_insert(pi2index, (char *)v, (char *)(long)nInputs++);
464    }
465
466    mAigId = Ntk_NodeReadMAigId(node);
467    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
468    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
469      bVar = array_fetch(mAigBvar_t, bVarList, index1);
470      st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
471      index1++;
472    }
473  }
474  timeframe->nInputs = nInputs;
475  timeframe->nbInputs = nbInputs;
476
477  array_sort(inputArr, nameCompare);
478  array_sort(latchArr, nameCompare);
479  array_sort(outputArr, nameCompare);
480
481    /** make 0 index bAigEdge_t **/
482  manager->SymbolTableArray[0] = st_init_table(strcmp,st_strhash);
483  manager->HashTableArray[0] = ALLOC(bAigEdge_t, bAig_HashTableSize);
484  for (i=0; i<bAig_HashTableSize; i++)
485       manager->HashTableArray[0][i]= bAig_NULL;
486  manager->SymbolTableArray[1] = st_init_table(strcmp,st_strhash);
487  manager->HashTableArray[1] = ALLOC(bAigEdge_t, bAig_HashTableSize);
488  for (i=0; i<bAig_HashTableSize; i++)
489       manager->HashTableArray[1][i]= bAig_NULL;
490
491  old2new = st_init_table(st_ptrcmp, st_ptrhash);
492  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
493  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
494  index1 = index = 0;
495  bindex = 0;
496  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
497
498    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
499
500    st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
501    mvfSize = array_n(mvfAig);
502    for(i=0; i< mvfSize; i++){
503      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
504#ifdef TIMEFRAME_VERIFY_
505      fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
506#endif
507      st_insert(old2new, (char *)v, (char *)(li[index1++]));
508    }
509  }
510  Ntk_NetworkForEachPseudoInput(network, gen, node) {
511
512    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
513
514    st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
515    mvfSize = array_n(mvfAig);
516    for(i=0; i< mvfSize; i++){
517      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
518#ifdef TIMEFRAME_VERIFY_
519      fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
520#endif
521      st_insert(old2new, (char *)v, (char *)(li[index1++]));
522    }
523  }
524
525  timeframe->blatchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
526  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
527  timeframe->blatchInputs[0] = bli;
528
529  timeframe->latchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
530  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
531  timeframe->latchInputs[0] = li;
532
533  ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
534  ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
535  timeframe->oriLatchInputs = ori_li;
536  timeframe->oribLatchInputs = ori_bli;
537
538  index1 = index = 0;
539  bindex = tindex = tindex1 = 0;
540
541  if(withInitialState == 0) {
542    manager->InitState = bAig_One;
543    Ntk_NetworkForEachLatch(network, gen, latch) {
544
545      manager->class_ = 0;
546
547      PureSat_CreateNewNode(manager, node2MvfAigTable, latch, bli, li, &bindex, &index,withInitialState);
548      node =  Ntk_LatchReadInitialInput(latch);
549      st_lookup(node2MvfAigTable,(char*)node,&tmpMvfAig);
550
551      st_lookup(node2MvfAigTable, (char *) latch, &mvfAig);
552      mvfSize = array_n(mvfAig);
553      imvfSize = array_n(tmpMvfAig);
554      if(mvfSize!=imvfSize){
555        fprintf(vis_stdout,"mvfSize:%d!=imvSize:%d, exit\n",mvfSize, imvfSize);
556        exit(0);
557      }
558      tmpv3=0;
559      for(i=0; i< mvfSize; i++){
560        bAigEdge_t tmpvvv;
561        tmpvvv = manager->InitState;
562        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
563        st_insert(old2new, (char *)v, (char *)(li[index1]));
564        flags(li[index1]) |= StateBitMask;
565#ifdef TIMEFRAME_VERIFY_
566        fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
567#endif
568        ori_li[index1++] = v;
569        if(tmpv3!=SATnormalNode(li[index1-1])){
570
571          vi = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(tmpMvfAig,i));
572
573          if(vi == bAig_One){
574            manager->InitState =
575              PureSat_And(manager,manager->InitState,li[index1-1]);
576#ifdef TIMEFRAME_VERIFY_
577            fprintf(vis_stdout,"%d AND %d = %d\n",li[index1-1],tmpvvv,manager->InitState);
578#endif
579          }
580          else if(vi == bAig_Zero){
581            manager->InitState =
582              PureSat_And(manager,manager->InitState,bAig_Not(li[index1-1]));
583#ifdef TIMEFRAME_VERIFY_
584            fprintf(vis_stdout,"%d AND %d = %d\n",bAig_Not(li[index1-1]),tmpvvv,manager->InitState);
585#endif
586          }
587          else{
588            tmpv1 = PureSat_ExpandForEachCone(manager,vi,old2new);
589            tmpv2 = PureSat_Eq(manager,li[index1-1],tmpv1);
590            manager->InitState = PureSat_And(manager,manager->InitState,tmpv2);
591#ifdef TIMEFRAME_VERIFY_
592
593            fprintf(vis_stdout,"%d AND %d = %d, %d is EQ node for funct node %d<-->%d\n",
594                   tmpvvv,tmpv2,manager->InitState,tmpv2,tmpv1,li[index1-1] );
595#endif
596          }
597        }
598        tmpv3 = SATnormalNode(li[index1-1]);
599      }
600
601      lmAigId = Ntk_NodeReadMAigId(latch);
602      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
603      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
604        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
605        tindex1++;
606        v = bAig_GetCanonical(manager, lbVar.node);
607        flags(bli[tindex])|=StateBitMask;
608        ori_bli[tindex++] = v;
609      }
610
611    }
612
613#if DBG
614    assert(tindex==bindex&&index1==index);
615#endif
616  }
617
618  st_free_table(old2new);
619
620  manager->class_ = 1;
621
622  timeframe->binputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
623  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
624  timeframe->binputs[0] = bli;
625
626  timeframe->inputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
627  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
628  ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
629  ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
630  timeframe->inputs[0] = li;
631  timeframe->oriInputs = ori_li;
632  timeframe->oribInputs = ori_bli;
633  index1 = index = 0;
634  tindex = bindex = tindex1 = 0;
635  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
636
637    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
638
639    st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
640    mvfSize = array_n(mvfAig);
641    for(i=0; i< mvfSize; i++){
642      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
643#ifdef TIMEFRAME_VERIFY_
644        fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
645#endif
646        ori_li[index1++] = v;
647    }
648    lmAigId = Ntk_NodeReadMAigId(node);
649    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
650    for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
651      lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
652      tindex1++;
653      v = bAig_GetCanonical(manager, lbVar.node);
654      ori_bli[tindex++] = v;
655    }
656  }
657  Ntk_NetworkForEachPseudoInput(network, gen, node) {
658
659    PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
660
661    st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
662    mvfSize = array_n(mvfAig);
663    for(i=0; i< mvfSize; i++){
664      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
665#ifdef TIMEFRAME_VERIFY_
666        fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
667#endif
668        ori_li[index1++] = v;
669    }
670    lmAigId = Ntk_NodeReadMAigId(node);
671    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
672    for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
673      lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
674      tindex1++;
675      v = bAig_GetCanonical(manager, lbVar.node);
676      ori_bli[tindex++] = v;
677    }
678  }
679
680    /** map node of previous timeframe into current timeframe **/
681  old2new = st_init_table(st_ptrcmp, st_ptrhash);
682
683  pre_li = timeframe->inputs[0];
684  ori_li = timeframe->oriInputs;
685
686  for(i=0; i<nInputs; i++){
687    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
688
689    }
690  pre_li = timeframe->latchInputs[0];
691  ori_li = timeframe->oriLatchInputs;
692
693    for(i=0; i<nLatches; i++){
694    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
695
696    }
697
698  pre_li = timeframe->binputs[0];
699  ori_li = timeframe->oribInputs;
700  for(i=0; i<nbInputs; i++){
701    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
702
703  }
704  pre_li = timeframe->blatchInputs[0];
705  ori_li = timeframe->oribLatchInputs;
706
707  for(i=0; i<nbLatches; i++){
708    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
709
710  }
711
712
713    /** create timeframe **/
714  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
715  timeframe->latchInputs[1] = li;
716  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
717  timeframe->blatchInputs[1] = bli;
718
719
720  bindex = index = 0;
721  Ntk_NetworkForEachLatch(network, gen, latch) {
722    char * name = Ntk_NodeReadName(latch);
723    node  = Ntk_LatchReadDataInput(latch);
724    mvfAig = lmvfAig = 0;
725    st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
726    mvfSize = array_n(mvfAig);
727    st_lookup(node2MvfAigTable, (char *)latch, &lmvfAig);
728    lmvfSize = array_n(lmvfAig);
729    if(mvfSize != lmvfSize) {
730        fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
731        exit(0);
732    }
733
734    else {
735      for(i=0; i< mvfSize; i++){
736        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
737
738        nv = PureSat_ExpandForEachCone(manager, v, old2new);
739        flags(nv) |= StateBitMask;
740        st_insert(old2new, (char *)v, (char *)nv);
741#ifdef TIMEFRAME_VERIFY_
742        fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n",
743              1, Ntk_NodeReadName(latch), i, v, nv);
744#endif
745        li[index++] = nv;
746        if(nv==bAig_Zero||nv==bAig_One)
747          continue;
748        if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
749          st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
750#ifdef TIMEFRAME_VERIFY_
751        fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
752#endif
753        }
754        else{
755          /*if they are not equal, resort to MultiLatchTable*/
756          if(strcmp(name,name1)){
757            if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
758#ifdef TIMEFRAME_VERIFY_
759              fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
760                     bAig_NonInvertedEdge(nv),name);
761#endif
762              st_insert(table,(char*)name,(char*)0);
763            }
764            else{
765              table = st_init_table(strcmp,st_strhash);
766#ifdef TIMEFRAME_VERIFY_
767              fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
768                     bAig_NonInvertedEdge(nv),name,name1);
769#endif
770              st_insert(table,(char*)name1,(char*)0);
771              st_insert(table,(char*)name,(char*)0);
772              st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
773            }
774          }
775        }
776
777      }
778    }
779
780
781    lmAigId = Ntk_NodeReadMAigId(node);
782    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
783    for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
784      lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
785      v = bAig_GetCanonical(manager, lbVar.node);
786
787      nv = PureSat_ExpandForEachCone(manager, v, old2new);
788      flags(nv) |= StateBitMask;
789      st_insert(old2new, (char *)v, (char *)nv);
790#ifdef TIMEFRAME_VERIFY_
791        ffprintf(vis_stdout,vis_stdout, "BLI(%d) %s(%d) : %d -> %d\n",
792              1, Ntk_NodeReadName(latch), i, v, nv);
793#endif
794      bli[bindex++] = nv;
795
796      tindex++;
797      if(nv==bAig_Zero||nv==bAig_One)
798        continue;
799      if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
800        st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
801#ifdef TIMEFRAME_VERIFY_
802        fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
803#endif
804      }
805      else{
806        /*if they are not equal, resort to MultiLatchTable*/
807        if(strcmp(name,name1)){
808          if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
809#ifdef TIMEFRAME_VERIFY_
810            fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
811                   bAig_NonInvertedEdge(nv),name);
812#endif
813            st_insert(table,(char*)name,(char*)0);
814          }
815          else{
816            table = st_init_table(strcmp,st_strhash);
817#ifdef TIMEFRAME_VERIFY_
818            fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
819                   bAig_NonInvertedEdge(nv),name,name1);
820#endif
821            st_insert(table,(char*)name1,(char*)0);
822            st_insert(table,(char*)name,(char*)0);
823            st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
824          }
825        }
826      }
827    }/*for(i=0, tindex=lmVar.bVars; i<lmVar.en...*/
828  }/*Ntk_NetworkForEachLatch(network, gen, latch) {*/
829
830
831#ifdef TIMEFRAME_VERIFY_
832
833  fprintf(vis_stdout,"after build latches of TF 1\n");
834#endif
835
836
837  timeframe->outputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
838  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
839  timeframe->outputs[0] = li;
840  index = 0;
841  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
842    st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
843    mvfSize = array_n(mvfAig);
844    for(i=0; i< mvfSize; i++){
845      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
846
847      nv = PureSat_ExpandForEachCone(manager, v, old2new);
848      st_insert(old2new, (char *)v, (char *)nv);
849      li[index++] = nv;
850    }
851  }
852
853  index = 0;
854  timeframe->internals = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
855  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
856  timeframe->internals[0] = li;
857  for(i=0; i<array_n(iindexArray); i++) {
858    v = array_fetch(bAigEdge_t, iindexArray, i);
859
860    nv = PureSat_ExpandForEachCone(manager, v, old2new);
861    st_insert(old2new, (char *)v, (char *)nv);
862    li[i] = nv;
863  }
864
865  /*change the class of latch vars of tf */
866  st_free_table(old2new);
867
868  timeframe->currentTimeframe = 0;
869
870  return(timeframe);
871
872}
873
874/**Function********************************************************************
875
876  Synopsis    [build more aig timeframes]
877
878  Description []
879
880  SideEffects []
881
882  SeeAlso     []
883
884******************************************************************************/
885void
886bAig_PureSat_ExpandTimeFrame(
887        Ntk_Network_t *network,
888        mAig_Manager_t *manager,
889        PureSat_Manager_t *pm,
890        int bound,
891        int withInitialState)
892{
893bAigTimeFrame_t *timeframe;
894int nLatches, nInputs, nOutputs, nInternals;
895int nbLatches, nbInputs;
896int i, j;
897int index, index1, bindex, tindex;
898int mvfSize, lmvfSize;
899int lmAigId;
900array_t *iindexArray;
901MvfAig_Function_t  *mvfAig, *lmvfAig;
902bAigEdge_t *li, *bli;
903bAigEdge_t *pre_li, *ori_li;
904bAigEdge_t v, nv;
905Ntk_Node_t *node, *latch;
906st_table   *node2MvfAigTable, *old2new;
907mAigMvar_t lmVar;
908mAigBvar_t lbVar;
909array_t   *bVarList, *mVarList;
910lsGen gen;
911
912st_table *idx2name, *table, *MultiLatchTable;
913char *name, *name1;
914
915
916  if(withInitialState) timeframe = manager->timeframe;
917  else                 timeframe = manager->timeframeWOI;
918
919  if(timeframe == 0)
920    timeframe = bAig_PureSat_InitTimeFrame(network, manager, pm,withInitialState);
921
922
923  idx2name = timeframe->idx2name;
924  MultiLatchTable = timeframe->MultiLatchTable;
925
926  node2MvfAigTable =
927        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
928
929  nbLatches = timeframe->nbLatches;
930  nbInputs = timeframe->nbInputs;
931  nLatches = timeframe->nLatches;
932  nInputs = timeframe->nInputs;
933  nOutputs = timeframe->nOutputs;
934  nInternals = timeframe->nInternals;
935
936  iindexArray = timeframe->iindexArray;
937
938  if(bound > timeframe->currentTimeframe) {
939    timeframe->latchInputs = (bAigEdge_t **)
940        realloc(timeframe->latchInputs, sizeof(bAigEdge_t *)*(bound+2));
941    timeframe->inputs = (bAigEdge_t **)
942      realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(bound+1));
943    timeframe->blatchInputs = (bAigEdge_t **)
944        realloc(timeframe->blatchInputs, sizeof(bAigEdge_t *)*(bound+2));
945    timeframe->binputs = (bAigEdge_t **)
946      realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(bound+1));
947    timeframe->outputs = (bAigEdge_t **)
948      realloc(timeframe->outputs, sizeof(bAigEdge_t *)*(bound+1));
949    timeframe->internals = (bAigEdge_t **)
950      realloc(timeframe->internals, sizeof(bAigEdge_t *)*(bound+1));
951  }
952
953  bVarList = mAigReadBinVarList(manager);
954  mVarList = mAigReadMulVarList(manager);
955
956  for(j=timeframe->currentTimeframe+1; j<=bound; j++) {
957    manager->class_ = j+1;
958    if(j>=manager->NumOfTable){
959      manager->NumOfTable *= 2;
960      manager->SymbolTableArray = REALLOC(st_table *,
961                 manager->SymbolTableArray,manager->NumOfTable);
962      manager->HashTableArray = REALLOC(bAigEdge_t *,
963                 manager->HashTableArray,manager->NumOfTable);
964    }
965    manager->SymbolTableArray[manager->class_] = st_init_table(strcmp,st_strhash);
966    manager->HashTableArray[manager->class_] = ALLOC(bAigEdge_t, bAig_HashTableSize);
967    for (i=0; i<bAig_HashTableSize; i++)
968      manager->HashTableArray[manager->class_][i]= bAig_NULL;
969
970
971    /** create new primary input node **/
972    timeframe->inputs = (bAigEdge_t **)
973        realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(j+1));
974    timeframe->binputs = (bAigEdge_t **)
975        realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(j+1));
976    bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
977    timeframe->binputs[j] = bli;
978    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
979    timeframe->inputs[j] = li;
980    index = 0;
981    index1 = 0;
982    bindex = 0;
983    Ntk_NetworkForEachPrimaryInput(network, gen, node) {
984
985      PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index,withInitialState);
986
987      st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
988      mvfSize = array_n(mvfAig);
989      for(i=0; i< mvfSize; i++){
990        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
991#ifdef TIMEFRAME_VERIFY_
992        fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
993#endif
994        index1++;
995      }
996    }
997    Ntk_NetworkForEachPseudoInput(network, gen, node) {
998
999      PureSat_CreateNewNode(manager, node2MvfAigTable, node, bli, li,  &bindex, &index,withInitialState);
1000
1001      st_lookup(node2MvfAigTable, (char *) node, &mvfAig);
1002      mvfSize = array_n(mvfAig);
1003      for(i=0; i< mvfSize; i++){
1004        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
1005#ifdef TIMEFRAME_VERIFY_
1006        fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
1007#endif
1008        index1++;
1009      }
1010    }
1011
1012    /** map previous time frame into current **/
1013    old2new = st_init_table(st_ptrcmp, st_ptrhash);
1014    pre_li = timeframe->inputs[j];
1015    ori_li = timeframe->oriInputs;
1016
1017    for(i=0; i<nInputs; i++){
1018      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
1019
1020    }
1021    pre_li = timeframe->latchInputs[j];
1022    ori_li = timeframe->oriLatchInputs;
1023
1024    for(i=0; i<nLatches; i++){
1025      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
1026
1027    }
1028
1029    pre_li = timeframe->binputs[j];
1030    ori_li = timeframe->oribInputs;
1031
1032    for(i=0; i<nbInputs; i++){
1033      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
1034
1035    }
1036
1037    pre_li = timeframe->blatchInputs[j];
1038    ori_li = timeframe->oribLatchInputs;
1039
1040    for(i=0; i<nbLatches; i++){
1041      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
1042
1043    }
1044
1045
1046    /** create new time frame **/
1047    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
1048    bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
1049    timeframe->latchInputs[j+1] = li;
1050    timeframe->blatchInputs[j+1] = bli;
1051    bindex = index = 0;
1052    Ntk_NetworkForEachLatch(network, gen, latch) {
1053      name = Ntk_NodeReadName(latch);
1054
1055      node  = Ntk_LatchReadDataInput(latch);
1056      mvfAig = lmvfAig = 0;
1057      st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
1058      mvfSize = array_n(mvfAig);
1059      st_lookup(node2MvfAigTable, (char *)latch, &lmvfAig);
1060      lmvfSize = array_n(lmvfAig);
1061      if(mvfSize != lmvfSize) {
1062        fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
1063        fprintf(vis_stdout, "          %s(%d), %s(%d)\n",
1064                Ntk_NodeReadName(node), mvfSize,
1065                Ntk_NodeReadName(latch), lmvfSize);
1066        exit(0);
1067      }
1068      else {
1069        for(i=0; i< mvfSize; i++){
1070          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
1071          nv = PureSat_ExpandForEachCone(manager, v, old2new);
1072          st_insert(old2new, (char *)v, (char *)nv);
1073#ifdef TIMEFRAME_VERIFY_
1074          fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n",
1075                  j+1, Ntk_NodeReadName(latch), i, v, nv);
1076#endif
1077          li[index++] = nv;
1078          flags(nv) |= StateBitMask;
1079          if(nv==bAig_Zero||nv==bAig_One)
1080            continue;
1081
1082          if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
1083            st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
1084#ifdef TIMEFRAME_VERIFY_
1085            fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
1086#endif
1087          }
1088          else{
1089            /*if they are not equal, resort to MultiLatchTable*/
1090            if(strcmp(name,name1)){
1091              if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
1092#ifdef TIMEFRAME_VERIFY_
1093                fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
1094                       bAig_NonInvertedEdge(nv),name);
1095#endif
1096                st_insert(table,(char*)name,(char*)0);
1097              }
1098              else{
1099                table = st_init_table(strcmp,st_strhash);
1100#ifdef TIMEFRAME_VERIFY_
1101                fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
1102                       bAig_NonInvertedEdge(nv),name,name1);
1103#endif
1104                st_insert(table,(char*)name1,(char*)0);
1105                st_insert(table,(char*)name,(char*)0);
1106                st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
1107              }
1108            }
1109          }
1110
1111        }/* for(i=0; i< mvfSize; i++){*/
1112      }/*else {*/
1113
1114      lmAigId = Ntk_NodeReadMAigId(node);
1115      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1116      for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
1117        lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
1118        v = bAig_GetCanonical(manager, lbVar.node);
1119        nv = PureSat_ExpandForEachCone(manager, v, old2new);
1120        flags(nv) |= StateBitMask;
1121        st_insert(old2new, (char *)v, (char *)nv);
1122#ifdef TIMEFRAME_VERIFY_
1123        fprintf(vis_stdout, "BLI(%d) %s(%d) : %d -> %d\n",
1124              j+1, Ntk_NodeReadName(latch), i, v, nv);
1125#endif
1126        bli[bindex++] = nv;
1127        if(nv==bAig_Zero||nv==bAig_One)
1128          continue;
1129
1130        if(!st_lookup(idx2name,(char*)bAig_NonInvertedEdge(nv),(char**)&name1)){
1131          st_insert(idx2name,(char*)bAig_NonInvertedEdge(nv),(char*)name);
1132#ifdef TIMEFRAME_VERIFY_
1133          fprintf(vis_stdout,"idx2name:%d-->%s\n",bAig_NonInvertedEdge(nv),name);
1134#endif
1135        }
1136        else{
1137          /*if they are not equal, resort to MultiLatchTable*/
1138          if(strcmp(name,name1)){
1139            if(st_lookup(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),&table)){
1140#ifdef TIMEFRAME_VERIFY_
1141              fprintf(vis_stdout,"found entry In MultiLatchTable for %d,insert %s \n",
1142                     bAig_NonInvertedEdge(nv),name);
1143#endif
1144              st_insert(table,(char*)name,(char*)0);
1145            }
1146            else{
1147              table = st_init_table(strcmp,st_strhash);
1148#ifdef TIMEFRAME_VERIFY_
1149              fprintf(vis_stdout,"NO entry In MultiLatchTable for %d,insert %s, %s \n",
1150                     bAig_NonInvertedEdge(nv),name,name1);
1151#endif
1152              st_insert(table,(char*)name1,(char*)0);
1153              st_insert(table,(char*)name,(char*)0);
1154              st_insert(MultiLatchTable,(char*)bAig_NonInvertedEdge(nv),(char*)table);
1155            }
1156          }
1157        }
1158
1159        tindex++;
1160      }
1161    }
1162
1163    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
1164    timeframe->outputs[j] = li;
1165    index = 0;
1166    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
1167      st_lookup(node2MvfAigTable, (char *)node, &mvfAig);
1168      mvfSize = array_n(mvfAig);
1169      for(i=0; i< mvfSize; i++){
1170        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
1171        nv = PureSat_ExpandForEachCone(manager, v, old2new);
1172        st_insert(old2new, (char *)v, (char *)nv);
1173        li[index++] = nv;
1174      }
1175    }
1176
1177    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
1178    timeframe->internals[j] = li;
1179    for(i=0; i<array_n(iindexArray); i++) {
1180      v = array_fetch(bAigEdge_t, iindexArray, i);
1181      nv = PureSat_ExpandForEachCone(manager, v, old2new);
1182      st_insert(old2new, (char *)v, (char *)nv);
1183      li[i] = nv;
1184    }
1185    st_free_table(old2new);
1186
1187
1188  }
1189
1190
1191  timeframe->currentTimeframe = bound;
1192}
1193
1194/**Function********************************************************************
1195
1196  Synopsis    [Name comparison function.]
1197
1198  Description [Name comparison function.]
1199
1200  SideEffects [none]
1201
1202  SeeAlso     []
1203
1204******************************************************************************/
1205static int
1206nameCompare(
1207  const void * node1,
1208  const void * node2)
1209{
1210  char *name1, *name2;
1211
1212  name1 = Ntk_NodeReadName((Ntk_Node_t *)node1);
1213  name2 = Ntk_NodeReadName((Ntk_Node_t *)node2);
1214  return(strcmp(*(char**)name1, *(char **)name2));
1215
1216}
1217
1218/**Function********************************************************************
1219
1220  Synopsis    [Compute number of encoding bits.]
1221
1222  Description [Compute number of encoding bits.]
1223
1224  SideEffects [none]
1225
1226  SeeAlso     []
1227
1228******************************************************************************/
1229static int
1230NoOfBitEncode( int n)
1231{
1232  int i = 0;
1233  int j = 1;
1234
1235  if (n < 2) return 1; /* Takes care of mv.values <= 1 */
1236
1237  while (j < n) {
1238    j = j * 2;
1239    i++;
1240  }
1241  return i;
1242}
Note: See TracBrowser for help on using the repository browser.