source: vis_dev/vis-2.3/src/baig/baigTimeframe.c @ 80

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

vis2.3
  • Property svn:executable set to *
File size: 45.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [baigTimeframe.c]
4
5  PackageName [baig]
6
7  Synopsis    [Functions to manage timeframe expansion.]
8
9  Author      [HoonSang Jin]
10
11  Copyright [ This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16******************************************************************************/
17
18#include "maig.h"
19#include "ntk.h"
20#include "cmd.h"
21#include "baig.h"
22#include "baigInt.h"
23#include "heap.h"
24#include "sat.h"
25#include "bmc.h"
26
27static char rcsid[] UNUSED = "$ $";
28
29/* #define TIMEFRAME_VERIFY_ */
30/*---------------------------------------------------------------------------*/
31/* Constant declarations                                                     */
32/*---------------------------------------------------------------------------*/
33
34
35/*---------------------------------------------------------------------------*/
36/* Stucture declarations                                                     */
37/*---------------------------------------------------------------------------*/
38
39
40/*---------------------------------------------------------------------------*/
41/* Type declarations                                                         */
42/*---------------------------------------------------------------------------*/
43
44
45/*---------------------------------------------------------------------------*/
46/* Variable declarations                                                     */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Macro declarations                                                        */
51/*---------------------------------------------------------------------------*/
52
53
54/**AutomaticStart*************************************************************/
55
56/*---------------------------------------------------------------------------*/
57/* Static function prototypes                                                */
58/*---------------------------------------------------------------------------*/
59
60static int nameCompare(const void * node1, const void * node2);
61static int NoOfBitEncode(int n);
62static bAigEdge_t CaseNew(mAig_Manager_t *manager, bAigEdge_t *arr, array_t * encodeList, int index);
63
64/**AutomaticEnd***************************************************************/
65
66
67/*---------------------------------------------------------------------------*/
68/* Definition of exported functions                                          */
69/*---------------------------------------------------------------------------*/
70
71/**Function********************************************************************
72
73  Synopsis    [Expand timeframe n times]
74
75  Description [Expand timeframe n times. If withInitialState flag is set then
76               unroll transition function considering initial states, otherwise
77               the state variables of 0'th timeframe are free variables]
78
79  SideEffects []
80
81  SeeAlso     []
82
83******************************************************************************/
84void
85bAig_ExpandTimeFrame(
86        Ntk_Network_t *network,
87        mAig_Manager_t *manager,
88        int bound,
89        int withInitialState)
90{
91bAigTimeFrame_t *timeframe;
92int nLatches, nInputs, nOutputs, nInternals;
93int nbLatches, nbInputs;
94int i, j;
95int index, index1, bindex, tindex;
96int mvfSize, lmvfSize;
97int lmAigId;
98array_t *iindexArray;
99MvfAig_Function_t  *mvfAig, *lmvfAig;
100bAigEdge_t *li, *bli;
101bAigEdge_t *pre_li, *ori_li;
102bAigEdge_t v, nv = bAig_NULL;
103Ntk_Node_t *node, *latch;
104st_table   *node2MvfAigTable, *old2new;
105mAigMvar_t lmVar;
106mAigBvar_t lbVar;
107array_t   *bVarList, *mVarList;
108lsGen gen;
109
110
111  if(withInitialState) timeframe = manager->timeframe;
112  else                 timeframe = manager->timeframeWOI;
113
114  if(timeframe == 0) 
115    timeframe = bAig_InitTimeFrame(network, manager, withInitialState);
116
117  node2MvfAigTable = 
118        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
119
120  nbLatches = timeframe->nbLatches;
121  nbInputs = timeframe->nbInputs;
122  nLatches = timeframe->nLatches;
123  nInputs = timeframe->nInputs;
124  nOutputs = timeframe->nOutputs;
125  nInternals = timeframe->nInternals;
126
127  iindexArray = timeframe->iindexArray;
128
129  if(bound > timeframe->currentTimeframe) {
130    timeframe->latchInputs = (bAigEdge_t **)
131        realloc(timeframe->latchInputs, sizeof(bAigEdge_t *)*(bound+2));
132    timeframe->inputs = (bAigEdge_t **)
133      realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(bound+1));
134    timeframe->blatchInputs = (bAigEdge_t **)
135        realloc(timeframe->blatchInputs, sizeof(bAigEdge_t *)*(bound+2));
136    timeframe->binputs = (bAigEdge_t **)
137      realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(bound+1));
138    timeframe->outputs = (bAigEdge_t **)
139      realloc(timeframe->outputs, sizeof(bAigEdge_t *)*(bound+1));
140    timeframe->internals = (bAigEdge_t **)
141      realloc(timeframe->internals, sizeof(bAigEdge_t *)*(bound+1));
142  }
143
144  bVarList = mAigReadBinVarList(manager);
145  mVarList = mAigReadMulVarList(manager);
146
147  for(j=timeframe->currentTimeframe+1; j<=bound; j++) {
148    /** create new primary input node **/
149    timeframe->inputs = (bAigEdge_t **)
150        realloc(timeframe->inputs, sizeof(bAigEdge_t *)*(j+1));
151    timeframe->binputs = (bAigEdge_t **)
152        realloc(timeframe->binputs, sizeof(bAigEdge_t *)*(j+1));
153    bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
154    timeframe->binputs[j] = bli;
155    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
156    timeframe->inputs[j] = li;
157    index = 0;
158    index1 = 0;
159    bindex = 0;
160    Ntk_NetworkForEachPrimaryInput(network, gen, node) {
161      bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
162
163      st_lookup(node2MvfAigTable, node, &mvfAig);
164      mvfSize = array_n(mvfAig);
165      for(i=0; i< mvfSize; i++){
166        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
167#ifdef TIMEFRAME_VERIFY_
168        fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
169#endif
170        index1++;
171      }
172    }
173    Ntk_NetworkForEachPseudoInput(network, gen, node) {
174      bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li,  &bindex, &index);
175
176      st_lookup(node2MvfAigTable, node, &mvfAig);
177      mvfSize = array_n(mvfAig);
178      for(i=0; i< mvfSize; i++){
179        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
180#ifdef TIMEFRAME_VERIFY_
181        fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", j, Ntk_NodeReadName(node), i, v, li[index1]);
182#endif
183        index1++;
184      }
185    }
186
187    /** map previous time frame into current **/
188    old2new = st_init_table(st_ptrcmp, st_ptrhash);
189    pre_li = timeframe->inputs[j];
190    ori_li = timeframe->oriInputs;
191    for(i=0; i<nInputs; i++)
192      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
193
194    pre_li = timeframe->latchInputs[j];
195    ori_li = timeframe->oriLatchInputs;
196    for(i=0; i<nLatches; i++)
197      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
198
199    pre_li = timeframe->binputs[j];
200    ori_li = timeframe->oribInputs;
201    for(i=0; i<nbInputs; i++)
202      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
203
204    pre_li = timeframe->blatchInputs[j];
205    ori_li = timeframe->oribLatchInputs;
206    for(i=0; i<nbLatches; i++)
207      st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
208
209    /** create new time frame **/
210    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
211    bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
212    timeframe->latchInputs[j+1] = li;
213    timeframe->blatchInputs[j+1] = bli;
214    bindex = index = 0;
215    Ntk_NetworkForEachLatch(network, gen, latch) {
216      node  = Ntk_LatchReadDataInput(latch);
217      mvfAig = lmvfAig = 0;
218      st_lookup(node2MvfAigTable, node, &mvfAig);
219      mvfSize = array_n(mvfAig);
220      st_lookup(node2MvfAigTable, latch, &lmvfAig);
221      lmvfSize = array_n(lmvfAig);
222      if(mvfSize != lmvfSize) {
223        fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
224        fprintf(vis_stdout, "          %s(%d), %s(%d)\n", 
225                Ntk_NodeReadName(node), mvfSize, 
226                Ntk_NodeReadName(latch), lmvfSize);
227        for(i=0; i< mvfSize; i++){
228          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
229          nv = bAig_ExpandForEachCone(manager, v, old2new);
230          st_insert(old2new, (char *)v, (char *)nv);
231          li[index++] = nv;
232        }
233        for(i=mvfSize; i< lmvfSize; i++){
234          li[index++] = nv;
235        }
236      }
237      else {
238        for(i=0; i< mvfSize; i++){
239          v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
240          /**
241            fprintf(vis_stdout, "-------------------------------\n");
242            fprintf(vis_stdout, "      Latch input %d %d\n", v, manager->nodesArraySize);
243            fprintf(vis_stdout, "-------------------------------\n");
244            bAig_SatRebuildNodeVerifySub(v, manager->NodesArray);
245            **/
246
247          nv = bAig_ExpandForEachCone(manager, v, old2new);
248          flags(nv) |= StateBitMask;
249          st_insert(old2new, (char *)v, (char *)nv);
250#ifdef TIMEFRAME_VERIFY_
251          fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 
252                  j+1, Ntk_NodeReadName(latch), i, v, nv);
253#endif
254          li[index++] = nv;
255        }
256      }
257
258      lmAigId = Ntk_NodeReadMAigId(node);
259      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
260      for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
261        lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
262        tindex++;
263        v = bAig_GetCanonical(manager, lbVar.node);
264        nv = bAig_ExpandForEachCone(manager, v, old2new);
265        flags(nv) |= StateBitMask;
266        st_insert(old2new, (char *)v, (char *)nv);
267        bli[bindex++] = nv;
268      }
269    }
270
271    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
272    timeframe->outputs[j] = li;
273    index = 0;
274    Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
275      st_lookup(node2MvfAigTable, node, &mvfAig);
276      mvfSize = array_n(mvfAig);
277      for(i=0; i< mvfSize; i++){
278        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
279
280        /**
281          fprintf(vis_stdout, "-------------------------------\n");
282          fprintf(vis_stdout, "      Output %d\n", v);
283          fprintf(vis_stdout, "-------------------------------\n");
284          bAig_SatRebuildNodeVerifySub(v, manager->NodesArray);
285          **/
286
287        nv = bAig_ExpandForEachCone(manager, v, old2new);
288        st_insert(old2new, (char *)v, (char *)nv);
289#ifdef TIMEFRAME_VERIFY_
290        fprintf(vis_stdout, "PO(%d) %s(%d) : %d -> %d\n", j+1, Ntk_NodeReadName(node), i, v, li[index]);
291#endif
292      st_insert(old2new, (char *)v, (char *)nv);
293        li[index++] = nv;
294      }
295    }
296 
297    li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
298    timeframe->internals[j] = li;
299    for(i=0; i<array_n(iindexArray); i++) {
300      v = array_fetch(bAigEdge_t, iindexArray, i);
301      nv = bAig_ExpandForEachCone(manager, v, old2new);
302      st_insert(old2new, (char *)v, (char *)nv);
303      li[i] = nv;
304    }
305    st_free_table(old2new);
306  }
307
308  timeframe->currentTimeframe = bound;
309}
310
311/**Function********************************************************************
312
313  Synopsis    [Compare function for name ordering]
314
315  Description [Compare function for name ordering]
316
317  SideEffects []
318
319  SeeAlso     []
320
321******************************************************************************/
322static int
323nameCompare(
324  const void * node1,
325  const void * node2)
326{
327  char *name1, *name2;
328 
329  name1 = Ntk_NodeReadName((Ntk_Node_t *)node1);
330  name2 = Ntk_NodeReadName((Ntk_Node_t *)node2);
331  return(strcmp(*(char**)name1, *(char **)name2));
332
333} 
334
335
336/**Function********************************************************************
337
338  Synopsis    [Make first timeframe]
339
340  Description [Make first timeframe]
341
342  SideEffects []
343
344  SeeAlso     []
345
346******************************************************************************/
347bAigTimeFrame_t *
348bAig_InitTimeFrame(
349        Ntk_Network_t *network,
350        mAig_Manager_t *manager,
351        int withInitialState)
352{
353bAigTimeFrame_t *timeframe;
354array_t *latchArr, *inputArr, *outputArr;
355array_t *iindexArray;
356st_table   *li2index, *o2index, *i2index, *pi2index;
357st_table   *bli2index, *bpi2index;
358Ntk_Node_t *node, *latch;
359st_table   *node2MvfAigTable, *old2new;
360lsGen gen;
361int nLatches, nInputs, nOutputs, nInternals;
362int nbLatches, nbInputs;
363int i;
364int index, index1, mvfSize, lmvfSize;
365int bindex, tindex, tindex1;
366MvfAig_Function_t  *mvfAig, *tmpMvfAig, *lmvfAig;
367bAigEdge_t *li, *pre_li, *ori_li;
368bAigEdge_t *bli, *ori_bli;
369bAigEdge_t v=bAig_NULL, nv;
370mAigMvar_t mVar;
371mAigBvar_t bVar;
372array_t   *bVarList, *mVarList;
373int mAigId;
374int lmAigId;
375mAigMvar_t lmVar;
376mAigBvar_t lbVar;
377
378  node2MvfAigTable = 
379        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
380
381  timeframe = ALLOC(bAigTimeFrame_t, 1);
382  memset(timeframe, 0, sizeof(bAigTimeFrame_t));
383  if(withInitialState) manager->timeframe = timeframe;
384  else                 manager->timeframeWOI = timeframe;
385
386  latchArr = array_alloc(Ntk_Node_t *, 0);
387  inputArr = array_alloc(Ntk_Node_t *, 0);
388  outputArr = array_alloc(Ntk_Node_t *, 0);
389  timeframe->latchArr = latchArr;
390  timeframe->inputArr = inputArr;
391  timeframe->outputArr = outputArr;
392
393  li2index = st_init_table(st_ptrcmp, st_ptrhash);
394  o2index = st_init_table(st_ptrcmp, st_ptrhash);
395  i2index = st_init_table(st_ptrcmp, st_ptrhash);
396  pi2index = st_init_table(st_ptrcmp, st_ptrhash);
397
398  bli2index = st_init_table(st_ptrcmp, st_ptrhash);
399  bpi2index = st_init_table(st_ptrcmp, st_ptrhash);
400
401  timeframe->li2index = li2index;
402  timeframe->o2index = o2index;
403  timeframe->pi2index = pi2index;
404  timeframe->i2index = i2index;
405
406  timeframe->bli2index = bli2index;
407  timeframe->bpi2index = bpi2index;
408  /**
409   * count total number,
410   * insert into node array
411   * and make table for bAigEdge_t to index
412   **/
413
414  bVarList = mAigReadBinVarList(manager);
415  mVarList = mAigReadMulVarList(manager);
416
417  nLatches = 0;
418  nbLatches = 0;
419  Ntk_NetworkForEachLatch(network, gen, latch) {
420    array_insert_last(Ntk_Node_t *, latchArr, latch);
421    st_lookup(node2MvfAigTable, latch, &mvfAig);
422    mvfSize = array_n(mvfAig);
423    for(i=0; i< mvfSize; i++){
424      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
425      st_insert(li2index, (char *)v, (char *)(long)nLatches++);
426    }
427
428    mAigId = Ntk_NodeReadMAigId(latch);
429    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
430    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
431      bVar = array_fetch(mAigBvar_t, bVarList, index1);
432      st_insert(bli2index, (char *)bVar.node, (char *)(long)nbLatches++);
433      index1++;
434    }
435  }
436  timeframe->nLatches = nLatches;
437  timeframe->nbLatches = nbLatches;
438
439  nOutputs = 0;
440  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
441    array_insert_last(Ntk_Node_t *, outputArr, node);
442    st_lookup(node2MvfAigTable, node, &mvfAig);
443    mvfSize = array_n(mvfAig);
444    for(i=0; i< mvfSize; i++){
445      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
446      st_insert(o2index, (char *)(long)v, (char *)(long)nOutputs++);
447    }
448  }
449  timeframe->nOutputs = nOutputs;
450
451  timeframe->iindexArray = iindexArray = array_alloc(bAigEdge_t, 0);
452  nInternals = 0;
453  Ntk_NetworkForEachNode(network, gen, node) {
454    if(Ntk_NodeTestIsShadow(node))      continue;
455    if(Ntk_NodeTestIsCombInput(node))   continue;
456    if(Ntk_NodeTestIsCombOutput(node))continue;
457    if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
458      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
459      array_free(tmpMvfAig);
460      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
461    }
462    mvfSize = array_n(mvfAig);
463    for(i=0; i< mvfSize; i++){
464      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
465      if(!st_lookup(i2index, (char *)v, &index1)) {
466        array_insert_last(bAigEdge_t, iindexArray, v);
467        st_insert(i2index, (char *)v, (char *)(long)nInternals++);
468      }
469    }
470#ifdef TIMEFRAME_VERIFY_
471      if(!strcmp(Ntk_NodeReadName(node), "v25") ||
472         !strcmp(Ntk_NodeReadName(node), "v27")) {
473          fprintf(stdout, "current error %d %d\n", v, nInternals);
474      }
475#endif
476  }
477  timeframe->nInternals = nInternals;
478
479  nInputs = 0;
480  nbInputs = 0;
481  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
482    array_insert_last(Ntk_Node_t *, inputArr, node);
483    if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
484      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
485      array_free(tmpMvfAig);
486      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
487    }
488    mvfSize = array_n(mvfAig);
489    for(i=0; i< mvfSize; i++){
490      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
491        st_insert(pi2index, (char *)(long)v, (char *)(long)nInputs++);
492    }
493
494    mAigId = Ntk_NodeReadMAigId(node);
495    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
496    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
497      bVar = array_fetch(mAigBvar_t, bVarList, index1);
498      st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
499      index1++;
500    }
501  }
502  Ntk_NetworkForEachPseudoInput(network, gen, node)  {
503    array_insert_last(Ntk_Node_t *, inputArr, node);
504    if(!st_lookup(node2MvfAigTable, node, &mvfAig)) {
505      tmpMvfAig = Bmc_NodeBuildMVF(network, node);
506      array_free(tmpMvfAig);
507      mvfAig = Bmc_ReadMvfAig(node, node2MvfAigTable);
508    }
509    mvfSize = array_n(mvfAig);
510    for(i=0; i< mvfSize; i++){
511      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
512        st_insert(pi2index, (char *)(long)v, (char *)(long)nInputs++);
513    }
514
515    mAigId = Ntk_NodeReadMAigId(node);
516    mVar = array_fetch(mAigMvar_t, mVarList, mAigId);
517    for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
518      bVar = array_fetch(mAigBvar_t, bVarList, index1);
519      st_insert(bpi2index, (char *)bVar.node, (char *)(long)nbInputs++);
520      index1++;
521    }
522  }
523  timeframe->nInputs = nInputs;
524  timeframe->nbInputs = nbInputs;
525
526  array_sort(inputArr, nameCompare);
527  array_sort(latchArr, nameCompare);
528  array_sort(outputArr, nameCompare);
529
530    /** make 0 index bAigEdge_t **/
531  old2new = st_init_table(st_ptrcmp, st_ptrhash);
532  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
533  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
534  index1 = index = 0;
535  bindex = 0;
536  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
537    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
538
539    st_lookup(node2MvfAigTable, node, &mvfAig);
540    mvfSize = array_n(mvfAig);
541    for(i=0; i< mvfSize; i++){
542      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
543#ifdef TIMEFRAME_VERIFY_
544      fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
545#endif
546      st_insert(old2new, (char *)v, (char *)(li[index1++]));
547    }
548  }
549  Ntk_NetworkForEachPseudoInput(network, gen, node) {
550    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
551
552    st_lookup(node2MvfAigTable, node, &mvfAig);
553    mvfSize = array_n(mvfAig);
554    for(i=0; i< mvfSize; i++){
555      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
556#ifdef TIMEFRAME_VERIFY_
557      fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", -1, Ntk_NodeReadName(node), i, v, li[index1]);
558#endif
559      st_insert(old2new, (char *)v, (char *)(li[index1++]));
560    }
561  }
562
563  timeframe->blatchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
564  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
565  timeframe->blatchInputs[0] = bli;
566
567  timeframe->latchInputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *)*(2));
568  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
569  timeframe->latchInputs[0] = li;
570
571  ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
572  ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
573  timeframe->oriLatchInputs = ori_li;
574  timeframe->oribLatchInputs = ori_bli;
575
576  index1 = index = 0;
577  bindex = tindex = tindex1 = 0;
578
579  if(withInitialState == 0) {
580    Ntk_NetworkForEachLatch(network, gen, latch) {
581      bAig_CreateNewNode(manager, node2MvfAigTable, latch, bli, li, &bindex, &index);
582
583      st_lookup(node2MvfAigTable, latch, &mvfAig);
584      mvfSize = array_n(mvfAig);
585      for(i=0; i< mvfSize; i++){
586        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
587        st_insert(old2new, (char *)v, (char *)(li[index1]));
588  #ifdef TIMEFRAME_VERIFY_
589        fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
590  #endif
591        ori_li[index1++] = v;
592      }
593
594      lmAigId = Ntk_NodeReadMAigId(latch);
595      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
596      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
597        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
598        tindex1++;
599        v = bAig_GetCanonical(manager, lbVar.node);
600        ori_bli[tindex++] = v ;
601      }
602    }
603  }
604  else {
605    Ntk_NetworkForEachLatch(network, gen, latch) {
606      node  = Ntk_LatchReadInitialInput(latch);
607      mvfAig = lmvfAig = 0;
608      st_lookup(node2MvfAigTable, node, &mvfAig);
609      mvfSize = array_n(mvfAig);
610      if(!st_lookup(node2MvfAigTable, latch, &lmvfAig)) {
611        tmpMvfAig = Bmc_NodeBuildMVF(network, latch);
612        array_free(tmpMvfAig);
613        lmvfAig = Bmc_ReadMvfAig(latch, node2MvfAigTable);
614      }
615      lmvfSize = array_n(lmvfAig);
616      if(mvfSize != lmvfSize) {
617          fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
618          fprintf(vis_stdout, "          %s(%d), %s(%d)\n", 
619                  Ntk_NodeReadName(node), mvfSize, 
620                  Ntk_NodeReadName(latch), lmvfSize);
621        for(i=0; i< mvfSize; i++){
622          v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
623          nv = bAig_ExpandForEachCone(manager, v, old2new);
624          st_insert(old2new, (char *)v, (char *)nv);
625            li[index++] = nv;
626        }
627        for(i=mvfSize; i<lmvfSize; i++) {
628          nv = bAig_ExpandForEachCone(manager, v, old2new);
629          st_insert(old2new, (char *)v, (char *)nv);
630            li[index++] = nv;
631        }
632      }
633      else {
634        for(i=0; i< mvfSize; i++){
635          v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
636          nv = bAig_ExpandForEachCone(manager, v, old2new);
637          st_insert(old2new, (char *)v, (char *)nv);
638            li[index++] = nv;
639        }
640      }
641      for(i=0; i< lmvfSize; i++){
642        v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(lmvfAig, i));
643  #ifdef TIMEFRAME_VERIFY_
644          fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(latch), i, v, li[index1]);
645  #endif
646          ori_li[index1++] = v;
647      }
648      lmAigId = Ntk_NodeReadMAigId(latch);
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      node  = Ntk_LatchReadInitialInput(latch);
657      lmAigId = Ntk_NodeReadMAigId(node);
658      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
659      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
660        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
661        tindex1++;
662        v = bAig_GetCanonical(manager, lbVar.node);
663        if(st_lookup(old2new, (char *)v, &nv))
664          bli[bindex++]  = nv;
665        else
666          bli[bindex++]  = v;
667      }
668    }
669  }
670  st_free_table(old2new);
671
672  timeframe->binputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
673  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbInputs);
674  timeframe->binputs[0] = bli;
675
676  timeframe->inputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
677  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
678  ori_li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
679  ori_bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInputs);
680  timeframe->inputs[0] = li;
681  timeframe->oriInputs = ori_li;
682  timeframe->oribInputs = ori_bli;
683  index1 = index = 0;
684  tindex = bindex = tindex1 = 0;
685  Ntk_NetworkForEachPrimaryInput(network, gen, node) {
686    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
687
688    st_lookup(node2MvfAigTable, node, &mvfAig);
689    mvfSize = array_n(mvfAig);
690    for(i=0; i< mvfSize; i++){
691      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
692#ifdef TIMEFRAME_VERIFY_
693        fprintf(vis_stdout, "IN(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
694#endif
695        ori_li[index1++] = v;
696    }
697    lmAigId = Ntk_NodeReadMAigId(node);
698    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
699    for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
700      lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
701      tindex1++;
702      v = bAig_GetCanonical(manager, lbVar.node);
703      ori_bli[tindex++] = v;
704    }
705  }
706  Ntk_NetworkForEachPseudoInput(network, gen, node) {
707    bAig_CreateNewNode(manager, node2MvfAigTable, node, bli, li, &bindex, &index);
708
709    st_lookup(node2MvfAigTable, node, &mvfAig);
710    mvfSize = array_n(mvfAig);
711    for(i=0; i< mvfSize; i++){
712      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
713#ifdef TIMEFRAME_VERIFY_
714        fprintf(vis_stdout, "PI(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index1]);
715#endif
716        ori_li[index1++] = v;
717    }
718    lmAigId = Ntk_NodeReadMAigId(node);
719    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
720    for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++) {
721      lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
722      tindex1++;
723      v = bAig_GetCanonical(manager, lbVar.node);
724      ori_bli[tindex++] = v;
725    }
726  }
727
728    /** map node of previous timeframe into current timeframe **/
729  old2new = st_init_table(st_ptrcmp, st_ptrhash);
730  pre_li = timeframe->inputs[0];
731  ori_li = timeframe->oriInputs;
732  for(i=0; i<nInputs; i++)
733    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
734  pre_li = timeframe->latchInputs[0];
735  ori_li = timeframe->oriLatchInputs;
736  for(i=0; i<nLatches; i++)
737    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
738
739  pre_li = timeframe->binputs[0];
740  ori_li = timeframe->oribInputs;
741  for(i=0; i<nbInputs; i++)
742    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
743  pre_li = timeframe->blatchInputs[0];
744  ori_li = timeframe->oribLatchInputs;
745  for(i=0; i<nbLatches; i++)
746    st_insert(old2new, (char *)ori_li[i], (char *)pre_li[i]);
747
748    /** create timeframe **/
749  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nLatches);
750  timeframe->latchInputs[1] = li;
751  bli = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nbLatches);
752  timeframe->blatchInputs[1] = bli;
753  bindex = index = 0;
754  Ntk_NetworkForEachLatch(network, gen, latch) {
755    node  = Ntk_LatchReadDataInput(latch);
756    mvfAig = lmvfAig = 0;
757    st_lookup(node2MvfAigTable, node, &mvfAig);
758    mvfSize = array_n(mvfAig);
759    st_lookup(node2MvfAigTable, latch, &lmvfAig);
760    lmvfSize = array_n(lmvfAig);
761    if(mvfSize != lmvfSize) {
762        fprintf(vis_stdout, "WARNING : the number of values of signals mismatched\n");
763        fprintf(vis_stdout, "          %s(%d), %s(%d)\n", 
764                Ntk_NodeReadName(node), mvfSize, 
765                Ntk_NodeReadName(latch), lmvfSize);
766      for(i=0; i< mvfSize; i++){
767        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
768        nv = bAig_ExpandForEachCone(manager, v, old2new);
769        st_insert(old2new, (char *)v, (char *)nv);
770        li[index++] = nv;
771      }
772      for(i=mvfSize; i< lmvfSize; i++){
773        li[index++] = nv;
774      }
775    }
776    else {
777      for(i=0; i< mvfSize; i++){
778        v = bAig_GetCanonical(manager,MvfAig_FunctionReadComponent(mvfAig, i));
779        nv = bAig_ExpandForEachCone(manager, v, old2new);
780/*      flags(nv) |= StateBitMask; */
781        st_insert(old2new, (char *)v, (char *)nv);
782#ifdef TIMEFRAME_VERIFY_
783        fprintf(vis_stdout, "LI(%d) %s(%d) : %d -> %d\n", 
784                  1, Ntk_NodeReadName(latch), i, v, nv);
785#endif
786        li[index++] = nv;
787      }
788    }
789    /* State bit mapping **/
790    lmAigId = Ntk_NodeReadMAigId(node);
791    lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
792    for(i=0, tindex=lmVar.bVars; i<lmVar.encodeLength; i++) {
793      lbVar = array_fetch(mAigBvar_t, bVarList, tindex);
794      tindex++;
795      v = bAig_GetCanonical(manager, lbVar.node);
796      nv = bAig_ExpandForEachCone(manager, v, old2new);
797      flags(nv) |= StateBitMask;
798      st_insert(old2new, (char *)v, (char *)nv);
799      bli[bindex++] = nv;
800    }
801
802  }
803
804  timeframe->outputs = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
805  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nOutputs);
806  timeframe->outputs[0] = li;
807  index = 0;
808  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
809    st_lookup(node2MvfAigTable, node, &mvfAig);
810    mvfSize = array_n(mvfAig);
811    for(i=0; i< mvfSize; i++){
812      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
813      nv = bAig_ExpandForEachCone(manager, v, old2new);
814#ifdef TIMEFRAME_VERIFY_
815        fprintf(vis_stdout, "PO(%d) %s(%d) : %d -> %d\n", 0, Ntk_NodeReadName(node), i, v, li[index]);
816#endif
817      st_insert(old2new, (char *)v, (char *)nv);
818      li[index++] = nv;
819    }
820  }
821
822  index = 0;
823  timeframe->internals = (bAigEdge_t **)malloc(sizeof(bAigEdge_t *));
824  li = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*nInternals);
825  timeframe->internals[0] = li;
826  for(i=0; i<array_n(iindexArray); i++) {
827    v = array_fetch(bAigEdge_t, iindexArray, i);
828    nv = bAig_ExpandForEachCone(manager, v, old2new);
829    st_insert(old2new, (char *)v, (char *)nv);
830    li[i] = nv;
831  }
832  st_free_table(old2new);
833
834  timeframe->currentTimeframe = 0;
835
836  return(timeframe);
837
838}
839
840/**Function********************************************************************
841
842  Synopsis    [Create aig node for free variables]
843
844  Description [Create aig node for free variables,
845               such as primary input and pseudo input]
846
847  SideEffects []
848
849  SeeAlso     []
850
851******************************************************************************/
852void
853bAig_CreateNewNode(
854        mAig_Manager_t *manager, 
855        st_table *node2MvfAigTable,
856        Ntk_Node_t *node, 
857        bAigEdge_t *bli,
858        bAigEdge_t *li,
859        int *bindex, 
860        int *index)
861{
862  int i, j, value, noBits;
863  bAigEdge_t *arr, v, tv;
864  MvfAig_Function_t  *mvfAig;
865  array_t *encodeList;
866  bAigEdge_t *ManagerNodesArray;
867  bAigTimeFrame_t *timeframe;
868 
869  timeframe = manager->timeframe;
870
871  value = Var_VariableReadNumValues(Ntk_NodeReadVariable(node));
872  noBits = NoOfBitEncode(value);
873  arr = (bAigEdge_t *)malloc(sizeof(bAigEdge_t)*noBits);
874  mvfAig = 0;
875  st_lookup(node2MvfAigTable, node, &mvfAig);
876  for(i=0; i<noBits; i++) {
877    arr[i] = bAig_CreateNode(manager, bAig_NULL, bAig_NULL);
878    bli[(*bindex)++] = arr[i];
879
880    flags(arr[i]) |= IsSystemMask;
881  }
882
883  for(i=0; i<value; i++) {
884    v = MvfAig_FunctionReadComponent(mvfAig, i);
885    /**
886    if(v == bAig_Zero)          li[(*index)++] = bAig_Zero;
887    else if(v == bAig_One)      li[(*index)++] = bAig_One;
888    else {
889    }
890    **/
891      encodeList = array_alloc(bAigEdge_t, 0);
892      for(j=0; j<value; j++) {
893        if(j == i)array_insert_last(bAigEdge_t, encodeList, mAig_One);
894        else    array_insert_last(bAigEdge_t, encodeList, mAig_Zero);
895      }
896      tv = CaseNew(manager, arr, encodeList, noBits-1);
897      li[(*index)++] = tv;
898
899      ManagerNodesArray = manager->NodesArray;
900
901      array_free(encodeList);
902      if(v == bAig_Zero){
903        flags(tv) |= StaticLearnMask;
904        if(timeframe->assertedArray == 0)
905          timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
906        array_insert_last(bAigEdge_t, timeframe->assertedArray, bAig_Not(tv));
907      }
908      else if(v == bAig_One){
909        flags(tv) |= StaticLearnMask;
910        if(timeframe->assertedArray == 0)
911          timeframe->assertedArray = array_alloc(bAigEdge_t, 0);
912        array_insert_last(bAigEdge_t, timeframe->assertedArray, tv);
913      }
914  }
915  free(arr);
916}
917   
918/**Function********************************************************************
919
920  Synopsis    [Compute bits is needed for encode n]
921
922  Description [Compute bits is needed for encode n]
923
924  SideEffects []
925
926  SeeAlso     []
927
928******************************************************************************/
929static int
930NoOfBitEncode( int n)
931{
932  int i = 0;
933  int j = 1;
934
935  if (n < 2) return 1; /* Takes care of mv.values <= 1 */
936
937  while (j < n) {
938    j = j * 2;
939    i++;
940  }
941  return i;
942}
943
944/**Function********************************************************************
945
946  Synopsis    [Extract bit from multi valued array]
947
948  Description [Extract bit from multi valued array]
949
950  SideEffects []
951
952  SeeAlso     []
953
954******************************************************************************/
955static bAigEdge_t
956CaseNew(mAig_Manager_t *manager,
957  bAigEdge_t      *arr,
958  array_t *       encodeList,
959  int             index) 
960{
961  int encodeLen;
962  int i, count;
963  bAigEdge_t v;
964  bAigEdge_t    andResult1, andResult2, orResult, result;
965  bAigEdge_t    node1, node2;
966  array_t *newEncodeList;
967
968  encodeLen = array_n(encodeList);
969  if (encodeLen == 1)
970    return array_fetch(bAigEdge_t, encodeList, 0);
971  newEncodeList =  array_alloc(bAigEdge_t, 0);
972
973  v = arr[index];
974  count = 0;
975  for (i=0; i< (encodeLen/2); i++){
976    node1 = array_fetch(bAigEdge_t, encodeList, count++);
977    node2 = array_fetch(bAigEdge_t, encodeList, count++);
978 
979     /*  performs ITE operator */
980    andResult1 = bAig_And(manager, v,           node2);
981    andResult2 = bAig_And(manager, bAig_Not(v), node1);
982    orResult   = bAig_Or (manager, andResult1,  andResult2);
983    flags(andResult1) |= IsSystemMask;
984    flags(andResult2) |= IsSystemMask;
985    flags(orResult) |= IsSystemMask;
986   
987    array_insert_last(bAigEdge_t, newEncodeList, orResult);
988  }
989
990  if(encodeLen%2){
991    node1 = array_fetch(bAigEdge_t, encodeList, count);
992    array_insert_last(bAigEdge_t, newEncodeList, node1);
993  }
994
995  result = CaseNew(manager, arr, newEncodeList, index-1);
996  array_free(newEncodeList);
997  return(result);
998}
999
1000 
1001/**Function********************************************************************
1002
1003  Synopsis    [Expand timeframe for aig node ]
1004
1005  Description [Expand timeframe for aig node ]
1006
1007  SideEffects []
1008
1009  SeeAlso     []
1010
1011******************************************************************************/
1012bAigEdge_t
1013bAig_ExpandForEachCone(
1014        mAig_Manager_t *manager,
1015        bAigEdge_t v,
1016        st_table *old2new)
1017{
1018  bAigEdge_t left, right, nv;
1019
1020  v = bAig_GetCanonical(manager, v);
1021  if(v == bAig_One || v == bAig_Zero)   return(v);
1022  if(v == bAig_NULL)    {
1023      fprintf(vis_stdout, "current error\n");
1024      return(v);
1025  }
1026
1027
1028  if(st_lookup(old2new, (char *)v, &nv))
1029    return(nv);
1030  if(st_lookup(old2new, (char *)bAig_Not(v), &nv))
1031    return(bAig_Not(nv));
1032
1033  left = bAig_ExpandForEachCone(manager, leftChild(v), old2new);
1034  right = bAig_ExpandForEachCone(manager, rightChild(v), old2new);
1035
1036  nv = bAig_And(manager, left, right);
1037
1038  flags(nv) |= IsSystemMask;
1039 
1040  if(bAig_IsInverted(v))        nv = bAig_Not(nv);
1041  st_insert(old2new, (char *)v, (char *)nv);
1042
1043  return(nv);
1044
1045}
1046
1047
1048
1049/**Function********************************************************************
1050
1051  Synopsis    [Check connectivity between aig nodes]
1052
1053  Description [Check connectivity between aig nodes]
1054
1055  SideEffects []
1056
1057  SeeAlso     []
1058
1059******************************************************************************/
1060void
1061bAig_CheckConnect(
1062        bAig_Manager_t *manager,
1063        int from, int to)
1064{
1065int reached;
1066
1067  reached = bAig_CheckConnectFanin(manager, from, leftChild(to));
1068  if(reached == 0)
1069    reached = bAig_CheckConnectFanin(manager, from, rightChild(to));
1070
1071  if(reached == 0)
1072    fprintf(stdout, "Node %d is not (backward) reachable from node %d\n",
1073            from, to);
1074
1075  reached = bAig_CheckConnectFanout(manager, from, to);
1076  if(reached == 0)
1077    fprintf(stdout, "Node %d is not (forward) reachable from node %d\n",
1078            to, from);
1079
1080}
1081
1082
1083/**Function********************************************************************
1084
1085  Synopsis    [Check connectivity of each fanin aig nodes]
1086
1087  Description [Check connectivity of each fanin aig nodes]
1088
1089  SideEffects []
1090
1091  SeeAlso     []
1092
1093******************************************************************************/
1094int
1095bAig_CheckConnectFanin(bAig_Manager_t *manager,
1096        int from, int to)
1097{
1098int left, right;
1099int reached;
1100
1101  if(bAig_NonInvertedEdge(from) == bAig_NonInvertedEdge(to))
1102    return(1);
1103
1104  left = leftChild(to);
1105  if(left == 2) 
1106    return(0);
1107
1108  right = leftChild(to);
1109
1110
1111  reached = bAig_CheckConnectFanin(manager, from, left);
1112  if(reached == 1)
1113    return(1);
1114  reached = bAig_CheckConnectFanin(manager, from, right);
1115  if(reached == 1)
1116    return(1);
1117
1118  return(0);
1119}
1120
1121/**Function********************************************************************
1122
1123  Synopsis    [Check connectivity of each fanout aig nodes]
1124
1125  Description [Check connectivity of each fanout aig nodes]
1126
1127  SideEffects []
1128
1129  SeeAlso     []
1130
1131******************************************************************************/
1132int
1133bAig_CheckConnectFanout(bAig_Manager_t *manager,
1134        int from, int to)
1135{
1136long *pfan, cur;
1137int size, j;
1138int reached;
1139
1140  size = nFanout(from);
1141  for(j=0, pfan = (bAigEdge_t *)fanout(from); j<size; j++) {
1142    cur = pfan[j];
1143    cur = cur >> 1;
1144    reached = bAig_CheckConnectFanout(manager, cur, to);
1145    if(reached == 1)
1146      return(1);
1147  }
1148  return(0);
1149}
1150
1151/**Function********************************************************************
1152
1153  Synopsis    [Get cone of influence nodes of given aig node]
1154
1155  Description [Get cone of influence nodes of given aig node]
1156
1157  SideEffects []
1158
1159  SeeAlso     []
1160
1161******************************************************************************/
1162void
1163bAig_GetCOIForNode(Ntk_Node_t *node, st_table *table)
1164{
1165int i;
1166Ntk_Node_t *faninNode;
1167
1168  if(node == NIL(Ntk_Node_t)){
1169    return;
1170  }
1171  if (Ntk_NodeTestIsLatch(node)){
1172    st_insert(table, (char *)node, (char *)node);
1173    return;
1174  }
1175
1176  Ntk_NodeForEachFanin(node, i, faninNode) {
1177    bAig_GetCOIForNode(faninNode, table);
1178  }
1179  return;
1180}
1181
1182/**Function********************************************************************
1183
1184  Synopsis    [Print cone of influence nodes of given aig node]
1185
1186  Description [Print cone of influence nodes of given aig node]
1187
1188  SideEffects []
1189
1190  SeeAlso     []
1191
1192******************************************************************************/
1193void
1194bAig_GetCOIForNodeMain(Ntk_Network_t * network, char *name)
1195{
1196int i, found;
1197Ntk_Node_t *node, *faninNode;
1198lsGen gen;
1199st_generator *gen1;
1200st_table *table;
1201
1202  node = Ntk_NetworkFindNodeByName(network, name);
1203  if(node == 0) {
1204    found = 0;
1205    Ntk_NetworkForEachNode(network, gen, node) {
1206      if(!strcmp(Ntk_NodeReadName(node), name)) {
1207        found = 1;
1208        break;
1209      }
1210    }
1211
1212    if(found == 0)
1213      node = 0;
1214  }
1215 
1216  if(node == NIL(Ntk_Node_t)){
1217    return;
1218  }
1219  if (Ntk_NodeTestIsLatch(node)){
1220    fprintf(stdout, "%s\n", Ntk_NodeReadName(node));
1221    return;
1222  }
1223
1224  table = st_init_table(st_ptrcmp, st_ptrhash);
1225
1226  Ntk_NodeForEachFanin(node, i, faninNode) {
1227    bAig_GetCOIForNode(faninNode, table);
1228  }
1229
1230  st_foreach_item(table, gen1, &node, &node) {
1231    fprintf(stdout, "%s\n", Ntk_NodeReadName(node));
1232  }
1233
1234  st_free_table(table);
1235  return;
1236}
1237
1238
1239/**Function********************************************************************
1240
1241  Synopsis    [Check status of latch]
1242
1243  Description [Check status of latch]
1244
1245  SideEffects []
1246
1247  SeeAlso     []
1248
1249******************************************************************************/
1250void
1251bAig_CheckLatchStatus(Ntk_Network_t * network, bAig_Manager_t *manager)
1252{
1253Ntk_Node_t *node; 
1254Ntk_Node_t *data, *init;
1255lsGen gen;
1256mAigMvar_t lmVar;
1257mAigBvar_t lbVar;
1258int tindex1, v, i, lmAigId;
1259array_t   *mVarList, *bVarList;
1260
1261  mVarList = mAigReadMulVarList(manager);
1262  bVarList = mAigReadBinVarList(manager);
1263  Ntk_NetworkForEachNode(network, gen, node) {
1264    if(Ntk_NodeTestIsPrimaryInput(node)) {
1265      fprintf(stdout, "Primary I %s :", Ntk_NodeReadName(node));
1266      lmAigId = Ntk_NodeReadMAigId(node);
1267      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1268      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
1269        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
1270        v = bAig_GetCanonical(manager, lbVar.node);
1271        fprintf(stdout, "%d ", v);
1272      }
1273      fprintf(stdout, "\n");
1274    }
1275  }
1276  Ntk_NetworkForEachNode(network, gen, node) {
1277    if(Ntk_NodeTestIsPseudoInput(node)) {
1278      fprintf(stdout, "Pseudo I %s :", Ntk_NodeReadName(node));
1279      lmAigId = Ntk_NodeReadMAigId(node);
1280      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1281      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
1282        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
1283        v = bAig_GetCanonical(manager, lbVar.node);
1284        fprintf(stdout, "%d ", v);
1285      }
1286      fprintf(stdout, "\n");
1287    }
1288  }
1289  Ntk_NetworkForEachNode(network, gen, node) {
1290    if (Ntk_NodeTestIsLatch(node)){
1291      fprintf(stdout, "Latch %s :", Ntk_NodeReadName(node));
1292      lmAigId = Ntk_NodeReadMAigId(node);
1293      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1294      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
1295        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
1296        v = bAig_GetCanonical(manager, lbVar.node);
1297        fprintf(stdout, "%d ", v);
1298      }
1299      fprintf(stdout, "\n");
1300
1301      data  = Ntk_LatchReadDataInput(node);
1302      fprintf(stdout, "  data input %s :", Ntk_NodeReadName(data));
1303      lmAigId = Ntk_NodeReadMAigId(data);
1304      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1305      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
1306        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
1307        v = bAig_GetCanonical(manager, lbVar.node);
1308        fprintf(stdout, "%d ", v);
1309      }
1310      fprintf(stdout, "\n");
1311
1312      init = Ntk_LatchReadInitialInput(node);
1313      fprintf(stdout, "  latch init %s :", Ntk_NodeReadName(init));
1314      lmAigId = Ntk_NodeReadMAigId(init);
1315      lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1316      for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
1317        lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
1318        v = bAig_GetCanonical(manager, lbVar.node);
1319        fprintf(stdout, "%d ", v);
1320      }
1321      fprintf(stdout, "\n");
1322    }
1323  }
1324  Ntk_NetworkForEachNode(network, gen, node) {
1325    lmAigId = Ntk_NodeReadMAigId(node);
1326    if(lmAigId == 2 || lmAigId == 0) {
1327      fprintf(stdout, "node aig id %s\n", Ntk_NodeReadName(node));
1328    }
1329  }
1330}
1331
1332/**Function********************************************************************
1333
1334  Synopsis    [Print status of aig node]
1335
1336  Description [Print status of aig node]
1337
1338  SideEffects []
1339
1340  SeeAlso     []
1341
1342******************************************************************************/
1343void
1344bAig_PrintNodeAigStatus(bAig_Manager_t *manager, Ntk_Node_t *node)
1345{
1346mAigMvar_t lmVar;
1347mAigBvar_t lbVar;
1348int tindex1, v, i, lmAigId;
1349array_t   *mVarList, *bVarList;
1350
1351  mVarList = mAigReadMulVarList(manager);
1352  bVarList = mAigReadBinVarList(manager);
1353  fprintf(stdout, "node %s :", Ntk_NodeReadName(node));
1354  lmAigId = Ntk_NodeReadMAigId(node);
1355  lmVar = array_fetch(mAigMvar_t, mVarList, lmAigId);
1356  for(i=0, tindex1=lmVar.bVars; i<lmVar.encodeLength; i++, tindex1++) {
1357    lbVar = array_fetch(mAigBvar_t, bVarList, tindex1);
1358    v = bAig_GetCanonical(manager, lbVar.node);
1359    fprintf(stdout, "%d ", v);
1360  }
1361  fprintf(stdout, "\n");
1362}
1363
1364/**Function********************************************************************
1365
1366  Synopsis    [Check status of aig node]
1367
1368  Description [Check status of aig node]
1369
1370  SideEffects []
1371
1372  SeeAlso     []
1373
1374******************************************************************************/
1375void
1376bAig_PrintNodeAigStatusWithName(Ntk_Network_t * network, bAig_Manager_t *manager, char *name)
1377{
1378Ntk_Node_t *node;
1379
1380  node = Ntk_NetworkFindNodeByName(network, name);
1381  bAig_PrintNodeAigStatus(manager, node);
1382}
1383
1384/**Function********************************************************************
1385
1386  Synopsis    [ Free timeframe ]
1387
1388  Description [ Free timeframe ]
1389
1390  SideEffects []
1391
1392  SeeAlso     []
1393
1394******************************************************************************/
1395void
1396bAig_FreeTimeFrame(bAigTimeFrame_t * timeframe)
1397{
1398int i; 
1399long *li;
1400
1401   if(timeframe == 0)   return;
1402
1403   if(timeframe->li2index)      st_free_table(timeframe->li2index);
1404   if(timeframe->o2index)       st_free_table(timeframe->o2index);
1405   if(timeframe->i2index)       st_free_table(timeframe->i2index);
1406   if(timeframe->pi2index)      st_free_table(timeframe->pi2index);
1407   if(timeframe->latchArr)      array_free(timeframe->latchArr);
1408   if(timeframe->inputArr)      array_free(timeframe->inputArr);
1409   if(timeframe->outputArr)     array_free(timeframe->outputArr);
1410   if(timeframe->iindexArray)   array_free(timeframe->iindexArray);
1411   if(timeframe->assertedArray) array_free(timeframe->assertedArray);
1412   if(timeframe->oriLatchInputs)free(timeframe->oriLatchInputs);
1413   if(timeframe->oriInputs)     free(timeframe->oriInputs);
1414   if(timeframe->oribLatchInputs)free(timeframe->oribLatchInputs);
1415   if(timeframe->oribInputs)     free(timeframe->oribInputs);
1416
1417   if(timeframe->inputs) {
1418     for(i=0; i<timeframe->currentTimeframe; i++) {
1419        li = timeframe->inputs[i];
1420        if(li)  free(li);
1421     }
1422     free(timeframe->inputs);
1423   }
1424   if(timeframe->binputs) {
1425     for(i=0; i<timeframe->currentTimeframe; i++) {
1426        li = timeframe->binputs[i];
1427        if(li)  free(li);
1428     }
1429     free(timeframe->binputs);
1430   }
1431   if(timeframe->outputs) {
1432     for(i=0; i<timeframe->currentTimeframe; i++) {
1433        li = timeframe->outputs[i];
1434        if(li)  free(li);
1435     }
1436     free(timeframe->outputs);
1437   }
1438   if(timeframe->latchInputs) {
1439     for(i=0; i<timeframe->currentTimeframe; i++) {
1440        li = timeframe->latchInputs[i];
1441        if(li)  free(li);
1442     }
1443     free(timeframe->latchInputs);
1444   }
1445   if(timeframe->blatchInputs) {
1446     for(i=0; i<timeframe->currentTimeframe; i++) {
1447        li = timeframe->blatchInputs[i];
1448        if(li)  free(li);
1449     }
1450     free(timeframe->blatchInputs);
1451   }
1452   if(timeframe->internals) {
1453     for(i=0; i<timeframe->currentTimeframe; i++) {
1454        li = timeframe->internals[i];
1455        if(li)  free(li);
1456     }
1457     free(timeframe->internals);
1458   }
1459}
1460
Note: See TracBrowser for help on using the repository browser.