source: vis_dev/vis-2.3/src/baig/baigCmd.c @ 50

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

vis2.3

File size: 20.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [baigCmd.c]
4
5  PackageName [baig]
6
7  Synopsis    [Functions to initialize and shut down the bAig manager.]
8
9  Author      [Mohammad Awedh]
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 "ctlsp.h"
24
25static char rcsid[] UNUSED = "$Id: baigCmd.c,v 1.32 2009/04/12 00:14:03 fabio Exp $";
26
27/*---------------------------------------------------------------------------*/
28/* Constant declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31
32/*---------------------------------------------------------------------------*/
33/* Stucture declarations                                                     */
34/*---------------------------------------------------------------------------*/
35
36
37/*---------------------------------------------------------------------------*/
38/* Type declarations                                                         */
39/*---------------------------------------------------------------------------*/
40
41
42/*---------------------------------------------------------------------------*/
43/* Variable declarations                                                     */
44/*---------------------------------------------------------------------------*/
45static jmp_buf timeOutEnv;
46static int bmcTimeOut;          /* timeout value */
47static long alarmLapTime;       /* starting CPU time for timeout */
48
49
50/*---------------------------------------------------------------------------*/
51/* Macro declarations                                                        */
52/*---------------------------------------------------------------------------*/
53
54
55/**AutomaticStart*************************************************************/
56
57/*---------------------------------------------------------------------------*/
58/* Static function prototypes                                                */
59/*---------------------------------------------------------------------------*/
60
61static int CommandPrintPartitionAig(Hrc_Manager_t ** hmgr, int argc, char ** argv);
62static int CommandPrintAigStats(Hrc_Manager_t ** hmgr, int argc, char ** argv);
63static int CommandCheckInvariantSat(Hrc_Manager_t ** hmgr, int argc, char ** argv);
64static void TimeOutHandle(void);
65
66/**AutomaticEnd***************************************************************/
67
68
69/*---------------------------------------------------------------------------*/
70/* Definition of exported functions                                          */
71/*---------------------------------------------------------------------------*/
72
73/**Function********************************************************************
74
75  Synopsis    [Initialize baig package]
76
77  SideEffects [none]
78
79  SeeAlso     [bAig_End]
80
81******************************************************************************/
82void
83bAig_Init(void)
84{
85  Cmd_CommandAdd("print_partition_aig_dot", CommandPrintPartitionAig, 0);
86  Cmd_CommandAdd("print_aig_stats", CommandPrintAigStats, 0);
87  Cmd_CommandAdd("check_invariant_sat", CommandCheckInvariantSat, 0);
88}
89
90
91/**Function********************************************************************
92
93  Synopsis [End baig package]
94
95  SideEffects []
96
97  SeeAlso     [bAig_Init]
98
99******************************************************************************/
100void
101bAig_End(void)
102{
103}
104
105/**Function********************************************************************
106
107  Synopsis    [Creates a new bAig manager.]
108
109  Description [Creates a new bAig manager, Create a NodeArray of size equal to
110  maxSize * bAigNodeSize. Returns a pointer to the manager if successful;
111  NULL otherwise.]
112
113  SideEffects [None]
114
115  SeeAlso     []
116
117******************************************************************************/
118bAig_Manager_t *
119bAig_initAig(
120  int maxSize /* maximum number of nodes in the AIG graph */
121)
122{
123  int i;
124
125  bAig_Manager_t *manager = ALLOC(bAig_Manager_t,1);
126  if (manager == NIL( bAig_Manager_t)){
127    return NIL( bAig_Manager_t);
128  }
129  /*Bing:*/
130  memset(manager,0,sizeof(bAig_Manager_t ));
131
132  maxSize = maxSize * bAigNodeSize;  /* each node is a size of bAigNodeSize */
133
134  /* ??? */
135  /*  maxSize = (maxSize/bAigNodeSize)*bAigNodeSize;
136  if (maxSize >  bAigArrayMaxSize ) {
137  }*/
138  manager->NodesArray = ALLOC(bAigEdge_t, maxSize);
139  manager->maxNodesArraySize = maxSize;
140  manager->nodesArraySize = bAigFirstNodeIndex;
141
142  fanout(0) = 0;
143  canonical(0) = 0;
144  flags(0) = 0;
145  aig_value(0) = 2;
146  next(0) = bAig_NULL;
147  /*Bing:*/
148  memset(manager->NodesArray,0,maxSize*sizeof(bAigEdge_t));
149
150  manager->SymbolTable = st_init_table(strcmp,st_strhash);
151  manager->nameList = ALLOC(char *, manager->maxNodesArraySize/bAigNodeSize);
152  manager->bddIdArray = ALLOC(int, manager->maxNodesArraySize/bAigNodeSize);
153  manager->bddArray = ALLOC(bdd_t *, manager->maxNodesArraySize/bAigNodeSize);
154
155  manager->HashTable =  ALLOC(bAigEdge_t, bAig_HashTableSize);
156  for (i=0; i<bAig_HashTableSize; i++)
157    manager->HashTable[i]= bAig_NULL; 
158
159  manager->mVarList = array_alloc(mAigMvar_t, 0);
160  manager->bVarList = array_alloc(mAigBvar_t, 0);
161  manager->timeframe = 0;
162  manager->timeframeWOI = 0;
163  manager->literals = 0;
164   
165  /* Bing: for MultiCut */
166  manager->SymbolTableArray = ALLOC(st_table *,100);
167  manager->HashTableArray = ALLOC(bAigEdge_t *,100);
168  manager->NumOfTable = 100;
169
170  /* Bing: for interpolation */
171  manager->class_ = 1;
172  manager->InitState = bAig_One;
173  manager->assertArray = (satArray_t *)0;
174
175  return(manager);
176
177} /* end of bAig_Init */
178
179
180/**Function********************************************************************
181
182  Synopsis [Quit bAig manager]
183
184  SideEffects []
185
186  SeeAlso     []
187
188******************************************************************************/
189void
190bAig_quit(
191  bAig_Manager_t *manager)
192{
193  char          *name;
194  st_generator  *stGen;
195  bAigEdge_t    varIndex;
196
197  if (manager->mVarList != NIL(array_t)){
198    array_free(manager->mVarList);
199  }
200  if (manager->bVarList != NIL(array_t)){
201    array_free(manager->bVarList);
202  }
203  FREE(manager->HashTable);
204  st_foreach_item(manager->SymbolTable, stGen, &name, &varIndex) {
205    FREE(name);
206  }
207  st_free_table(manager->SymbolTable);
208  /* i is too small to represent 80000
209  for (i=0; i< manager->maxNodesArraySize/bAigNodeSize ; i++){
210    FREE(manager->nameList[i]);
211  }
212  */
213  FREE(manager->nameList);
214  FREE(manager->NodesArray);
215  bAig_FreeTimeFrame(manager->timeframe);
216  bAig_FreeTimeFrame(manager->timeframeWOI);
217  FREE(manager);
218
219  /* Free SymbolTableArray and HashTableArray? */
220}
221
222/**Function********************************************************************
223
224  Synopsis    []
225
226  Description []
227
228  SideEffects [None]
229
230  SeeAlso     []
231
232******************************************************************************/
233void 
234bAig_NodePrint(
235   bAig_Manager_t *manager,
236   bAigEdge_t node)
237{
238  if (node == bAig_Zero) {
239    printf("0");
240    return;
241  }
242  if (node == bAig_One) {
243    printf("1");
244    return;
245  }
246  if (bAig_IsInverted(node)){
247    printf(" NOT(");
248  }
249  if (bAigIsVar(manager,node)) {
250    printf("Var Node");
251  } else {
252    printf("(");
253    bAig_NodePrint(manager, leftChild(node));
254    printf("AND");
255    bAig_NodePrint(manager, rightChild(node));
256    printf(")");
257  }
258  if (bAig_IsInverted(node)){
259    printf(")");
260  }
261
262} /* bAig_NodePrint */
263
264
265/*---------------------------------------------------------------------------*/
266/* Definition of internal functions                                          */
267/*---------------------------------------------------------------------------*/
268
269
270/*---------------------------------------------------------------------------*/
271/* Definition of static functions                                            */
272/*---------------------------------------------------------------------------*/
273
274/**Function********************************************************************
275
276  Synopsis    [Implements the print_partition_aig_dot command.]
277 
278  CommandName [print_partition_aig_dot]
279
280  CommandSynopsis [Print a dot description of the AND/INVERTER graph that was
281  built for the flattened network]
282
283  CommandArguments [\[-h\] &lt;file_name&gt;]
284
285  CommandDescription [Write a file in the format taken by the tool <tt>dot</tt>
286  depicting the topology of the AND/INVERTER graph.
287  Dot is a tool that given a description of a graph in a certain format it
288  produces a postscript print of the graph.
289  For more information about <tt>dot</tt> look in <a
290  href="http://www.research.att.com/orgs/ssr/book/reuse">
291  http://www.research.att.com/orgs/ssr/book/reuse</a>. Once a dot file is
292  produced with this command, the shell command <tt>dot -Tps <filename>
293  &gt;<file>.ps</tt> will produce the postscript file depicting the network.<p>
294
295  If no argument is specified on the command line, the description is written
296  to the standard output.<p>
297
298  Command options:<p>
299  <dl><dt> -h
300  <dd> Print the command usage.
301  </dl>]
302
303  SideEffects []
304
305  SeeAlso     []
306
307******************************************************************************/
308static int
309CommandPrintPartitionAig(
310  Hrc_Manager_t ** hmgr,
311  int  argc,
312  char ** argv)
313{
314  FILE *fp;
315  int c, i, mvfSize;
316  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
317  mAig_Manager_t *manager;
318  MvfAig_Function_t  *mvfAig;
319  bAigEdge_t v;
320  Ntk_Node_t *node, *latch;
321  st_table   *node2MvfAigTable;
322  lsGen gen;
323
324  util_getopt_reset();
325  while ((c = util_getopt(argc,argv,"h")) != EOF){
326    switch(c){
327      case 'h':
328        goto usage;
329      default:
330        goto usage;
331    }
332  }
333  /* Check if the network has been read in */
334  if (network == NIL(Ntk_Network_t)) {
335    return 1;
336  }
337
338  if (argc == 1) {
339    fp = stdout;
340  }
341  else if (argc == 2) {
342    fp = Cmd_FileOpen(*(++argv), "w", NIL(char *), /* silent */ 1);
343    if (fp == NIL(FILE)) {
344      (void) fprintf(vis_stderr, "Cannot write to %s\n", *argv);
345      return 1;
346    }
347  }
348  else {
349    goto usage;
350  }
351
352  manager = Ntk_NetworkReadMAigManager(network);
353
354  if (manager == NIL(mAig_Manager_t)) {
355    return 1;
356  }
357  node2MvfAigTable = 
358        (st_table *)Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
359
360  Ntk_NetworkForEachLatch(network, gen, latch) {
361    node = Ntk_LatchReadDataInput(latch);
362    st_lookup(node2MvfAigTable, node, &mvfAig);
363    mvfSize = array_n(mvfAig);
364    for(i=0; i< mvfSize; i++){
365      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
366      bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
367    }
368  }
369  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
370    st_lookup(node2MvfAigTable, node, &mvfAig);
371    mvfSize = array_n(mvfAig);
372    for(i=0; i< mvfSize; i++){
373      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
374      bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
375    }
376  }
377
378  Ntk_NetworkForEachNode(network, gen, node) {
379    st_lookup(node2MvfAigTable, node, &mvfAig);
380    mvfSize = array_n(mvfAig);
381    for(i=0; i< mvfSize; i++){
382      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
383      bAig_SetMaskTransitiveFanin(manager, v, VisitedMask);
384    }
385  }
386
387  bAig_PrintDot(fp, manager);
388  Ntk_NetworkForEachLatch(network, gen, latch) {
389    node = Ntk_LatchReadInitialInput(latch);
390    st_lookup(node2MvfAigTable, node, &mvfAig);
391    mvfSize = array_n(mvfAig);
392    for(i=0; i< mvfSize; i++){
393      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
394      bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
395    }
396  }
397  Ntk_NetworkForEachPrimaryOutput(network, gen, node) {
398    st_lookup(node2MvfAigTable, node, &mvfAig);
399    mvfSize = array_n(mvfAig);
400    for(i=0; i< mvfSize; i++){
401      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
402      bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
403    }
404  }
405  Ntk_NetworkForEachNode(network, gen, node) {
406    st_lookup(node2MvfAigTable, node, &mvfAig);
407    mvfSize = array_n(mvfAig);
408    for(i=0; i< mvfSize; i++){
409      v = bAig_GetCanonical(manager, MvfAig_FunctionReadComponent(mvfAig, i));
410      bAig_ResetMaskTransitiveFanin(manager, v, VisitedMask, ResetVisitedMask);
411    }
412  }
413
414  return 0;
415usage:
416  (void) fprintf(vis_stderr, "usage: print_partition_aig_dot [-h] [file]\n");
417  (void) fprintf(vis_stderr, "    -h\t\tprint the command usage\n");
418  return 1;
419}
420
421/**Function********************************************************************
422
423  Synopsis    [Implements the print_aig_stats command.]
424  CommandName [print_aig_stats]
425
426  CommandSynopsis [print statistics about the AND/INVERTER graph.]
427
428  CommandArguments [\[-h\] \[-n\]]
429
430  CommandDescription [Print the following statistics about the AND/INVERTER
431  graph:
432
433 <dl>
434  <li> <b>Maximum number of nodes:</b> the maximum number of nodes in the AND/
435  INVERTER graph.
436
437  <li> <b>Current number of nodes:</b> the number of nodes in the AND/INVERTER
438  graph that are used.
439
440 </dl>
441
442  Note that <tt>build_partition_maigs</tt> must be called before this command.<p>
443
444  Command options:<p>
445
446  <dl>
447  <dt> -n
448  <dd> Print the name of the nodes.<p>
449  <dt> -h
450  <dd> Print the command usage.<p>
451  </dl>
452  ]
453
454  SideEffects []
455
456  SeeAlso     []
457
458******************************************************************************/
459static int
460CommandPrintAigStats(
461  Hrc_Manager_t ** hmgr,
462  int  argc,
463  char ** argv)
464{
465  Ntk_Network_t *network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
466  mAig_Manager_t *manager;
467  int i;
468  int printVar = 0;
469  int c;
470
471  /*
472   * Parse command line options.
473   */
474  util_getopt_reset();
475  while ((c = util_getopt(argc, argv, "hn")) != EOF) {
476    switch(c) {
477      case 'h':
478        goto usage;
479     case 'n':
480       printVar = 1;
481        break;
482      default:
483        goto usage;
484    }
485  }
486  if (network == NIL(Ntk_Network_t)) {
487    return 1;
488  }
489
490  manager = Ntk_NetworkReadMAigManager(network);
491
492  if (manager == NIL(mAig_Manager_t)) {
493    return 1;
494  }
495  (void) fprintf(vis_stdout,"And/Inverter graph Static Report\n");
496  (void) fprintf(vis_stdout,"Maximum number of nodes: %ld\n", manager->maxNodesArraySize/bAigNodeSize);
497  (void) fprintf(vis_stdout,"Current number of nodes: %ld\n\n", manager->nodesArraySize/bAigNodeSize);
498  if (printVar == 1){
499     (void) fprintf(vis_stdout,"Nodes name\n");
500     for(i=1; i< manager->nodesArraySize/bAigNodeSize; i++){
501        if (manager->nameList[i][0] != 'N'){
502           (void) fprintf(vis_stdout,"%s\n", manager->nameList[i]);
503        }
504     }
505  }
506  return 0;
507usage:
508  (void) fprintf(vis_stderr, "usage: print_aig_stats [-h] [-n] \n");
509  (void) fprintf(vis_stderr, "   -h print the command usage\n");
510  (void) fprintf(vis_stderr, "   -n list of variables\n");
511  return 1;             /* error exit */
512}
513
514/**Function********************************************************************
515
516  Synopsis    [Implements the check_invariant_sat command.]
517  CommandName [check_invariant_sat]
518
519  CommandSynopsis [Check invariant property using sat based unmounded model checking]
520
521  CommandArguments [\[-h\] \[-d\]
522                    \[-t &lt;timeOutPeriod&gt;\]
523                    \[-m &lt;method&gt;\]
524                    \[-v &lt;verbosity_level&gt;\]
525                    &lt;inv_file&gt; ]
526
527  CommandDescription [Perform SAT-based unbounded model checking on
528  And-Inverter-Graph. The command compute fixed point of AG using AX operation.
529  AX is implemented using AllSAT enumeration algorithm.
530
531  Command options:<p>
532
533  <dl>
534  <dt> -d
535  <dd> Disable inclusion test on initial states.<p>
536
537  <dt> -v  <code>&lt;verbosity_level&gt;</code>
538  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage and code status.
539
540  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
541  <dd> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
542  <p>
543
544  <dt> -m  <code>&lt;method&gt;</code>
545  <dd> Specify the method for AllSAT algorithm.
546  <p>
547
548
549  <dt> -h
550  <dd> Print the command usage.<p>
551  </dl>
552
553  <dt> <code> &lt;inv_file&gt; </code>
554  <dd> File containing Invariant formulae to be checked.
555  ]
556
557  SideEffects []
558
559  SeeAlso     []
560
561******************************************************************************/
562static int
563CommandCheckInvariantSat(
564  Hrc_Manager_t ** hmgr,
565  int  argc,
566  char ** argv)
567{
568char *filename;
569FILE *fin;
570array_t *invarArray;
571Ntk_Network_t     *network;
572bAig_Manager_t    *manager;
573bAigTransition_t *t;
574Ctlsp_Formula_t *formula;
575char c;int i, property;
576int timeOutPeriod;
577int passFlag, method;
578int interface, verbose;
579int inclusion_test;
580int constrain;
581int reductionUsingUnsat;
582int disableLifting;
583
584  timeOutPeriod = -1;
585  method = 1;
586  interface = 0;
587  inclusion_test = 1;
588  verbose = 0;
589  constrain = 1;
590  reductionUsingUnsat = 0;
591  disableLifting = 0;
592  util_getopt_reset();
593  while ((c = util_getopt(argc, argv, "hicdt:m:v:ul")) != EOF) {
594    switch(c) {
595      case 'h':
596        goto usage;
597      case 'i' :
598        interface = 1;
599        break;
600      case 'd' :
601        inclusion_test = 0;
602        break;
603      case 'c' :
604        constrain = 0;
605        break;
606      case 'u' :
607        reductionUsingUnsat = 1;
608        break;
609      case 'l' :
610        disableLifting = 1;
611        break;
612      case 't' :
613        timeOutPeriod = atoi(util_optarg);
614        break;
615      case 'v' :
616        verbose = atoi(util_optarg);
617        break;
618      case 'm' :
619        method = atoi(util_optarg);
620        break;
621    }
622  }
623  if (argc - util_optind == 0) {
624    (void) fprintf(vis_stderr, "** ERROR : file containing property file not provided\n");
625    goto usage;
626  }
627  else if (argc - util_optind > 1) {
628    (void) fprintf(vis_stderr, "** ERROR : too many arguments\n");
629    goto usage;
630  }
631  filename = util_strsav(argv[util_optind]);
632
633  if(!(fin = fopen(filename, "r"))) {
634    fprintf(vis_stdout, "Error : can't open invariant file %s\n", filename);
635    return(1);
636  }
637  invarArray = Ctlsp_FileParseFormulaArray(fin);
638  fclose(fin);
639
640  if (timeOutPeriod > 0) {
641    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
642    (void) alarm(timeOutPeriod);
643    if (setjmp(timeOutEnv) > 0) {
644      (void) fprintf(vis_stderr,
645                "** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod);
646      alarm(0);
647      return 1;
648    }
649  }
650
651  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
652  manager = Ntk_NetworkReadMAigManager(network);
653
654  t = bAigCreateTransitionRelation(network, manager);
655  t->method = method;
656  t->interface = interface;
657  t->inclusionInitial = inclusion_test;
658  t->verbose = verbose;
659  t->constrain = constrain;
660  t->disableLifting = disableLifting;
661  t->reductionUsingUnsat = reductionUsingUnsat;
662
663  if(t->verbose > 1) 
664    bAigPrintTransitionInfo(t);
665
666
667  fprintf(vis_stdout, "# INV: Summary of invariant pass/fail\n");
668  for(i=0; i<array_n(invarArray); i++) {
669    formula = array_fetch(Ctlsp_Formula_t *, invarArray, i);
670    Ctlsp_FormulaPrint(vis_stdout, formula);
671    fprintf(vis_stdout, "\n");
672
673    property = bAig_CreatebAigForInvariant(network, manager, formula);
674
675    passFlag = bAigCheckInvariantWithAG(t, property);
676
677    if(passFlag == 1) {
678      fprintf(vis_stdout, "# INV: formula passed --- ");
679      Ctlsp_FormulaPrint(vis_stdout, Ctlsp_FormulaReadOriginalFormula(formula));
680      fprintf(vis_stdout, "\n");
681    }
682    else {
683      fprintf(vis_stdout, "# INV: formula failed --- ");
684      Ctlsp_FormulaPrint(vis_stdout, Ctlsp_FormulaReadOriginalFormula(formula));
685      fprintf(vis_stdout, "\n");
686    }
687  }
688
689  return(0);
690
691  usage:
692  (void) fprintf(vis_stderr, "usage: check_invariant_sat [-h] <inv_file>\n");
693  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
694  (void) fprintf(vis_stderr, "   -d \tdisable inclusion test on initial states\n");
695  (void) fprintf(vis_stderr, "   -m : 0 disable lifting\n");
696  (void) fprintf(vis_stderr, "        1 enable lifting (default)\n");
697  (void) fprintf(vis_stderr, "   <inv_file> Invariant file to be checked.\n");
698
699  return(1);
700}
701
702
703/**Function********************************************************************
704
705  Synopsis    [Handle function for timeout.]
706
707  Description [This function is called when the time out occurs.
708  Since alarm is set with an elapsed time, this function checks if the
709  CPU time corresponds to the timeout of the command.  If not, it
710  reprograms the alarm to fire again later.]
711
712  SideEffects []
713
714******************************************************************************/
715static void
716TimeOutHandle(void)
717{
718  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
719
720  if (seconds < bmcTimeOut) {
721    unsigned slack = (unsigned) (bmcTimeOut - seconds);
722    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
723    (void) alarm(slack);
724  } else {
725    longjmp(timeOutEnv, 1);
726  }
727} /* TimeOutHandle */
728
Note: See TracBrowser for help on using the repository browser.