source: vis_dev/vis-2.3/src/bmc/bmcCmd.c @ 102

Last change on this file since 102 was 102, checked in by cecile, 12 years ago

add write_cnf of design cmd
File size: 44.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [bmcCmd.c]
4
5  PackageName [bmc]
6
7  Synopsis    [Command interface for bounded model checking (bmc)]
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#include "bmcInt.h"
18
19static char rcsid[] UNUSED = "$Id: bmcCmd.c,v 1.83 2010/04/09 23:50:57 fabio Exp $";
20
21/*---------------------------------------------------------------------------*/
22/* Constant declarations                                                     */
23/*---------------------------------------------------------------------------*/
24
25/*---------------------------------------------------------------------------*/
26/* Type declarations                                                         */
27/*---------------------------------------------------------------------------*/
28
29
30/*---------------------------------------------------------------------------*/
31/* Structure declarations                                                    */
32/*---------------------------------------------------------------------------*/
33
34
35/*---------------------------------------------------------------------------*/
36/* Variable declarations                                                     */
37/*---------------------------------------------------------------------------*/
38static jmp_buf timeOutEnv;
39static int bmcTimeOut;          /* timeout value */
40static long alarmLapTime;       /* starting CPU time for timeout */
41
42/**AutomaticStart*************************************************************/
43
44/*---------------------------------------------------------------------------*/
45/* Static function prototypes                                                */
46/*---------------------------------------------------------------------------*/
47
48/*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv);
49static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv);
50static int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv);
51static void TimeOutHandle(void);
52static void DispatchBmcCommand(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options);
53static int CommandCnfSat(Hrc_Manager_t ** hmgr, int argc, char ** argv);
54
55/**AutomaticEnd***************************************************************/
56
57
58/*---------------------------------------------------------------------------*/
59/* Definition of exported functions                                          */
60/*---------------------------------------------------------------------------*/
61
62/**Function********************************************************************
63
64  Synopsis    [Initializes the BMC package.]
65
66  SideEffects []
67
68  SeeAlso     [Bmc_End]
69
70******************************************************************************/
71void
72Bmc_Init(void)
73{
74  Cmd_CommandAdd("bounded_model_check", CommandBmc, /* doesn't change network */  0);
75 
76  Cmd_CommandAdd("cnf_sat", CommandCnfSat, /* doesn't change network */  0); 
77  Cmd_CommandAdd("write_cnf", CommandWriteCnf, /* doesn't change network */  0); 
78}
79
80/**Function********************************************************************
81
82  Synopsis    [Ends BMC package.]
83
84  SideEffects []
85
86  SeeAlso     [Bmc_Init]
87
88******************************************************************************/
89void
90Bmc_End(void)
91{
92}
93
94/*---------------------------------------------------------------------------*/
95/* Definition of internal functions                                          */
96/*---------------------------------------------------------------------------*/
97
98
99/**Function********************************************************************
100
101  Synopsis [Parse the user input for command "bmc".]
102
103  Description []
104
105  SideEffects []
106
107******************************************************************************/
108/*static*/ BmcOption_t *
109ParseBmcOptions(
110  int argc,
111  char **argv)
112{
113  BmcOption_t  *options = BmcOptionAlloc();
114  char *ltlFileName     = NIL(char);
115  unsigned int i;
116  int          c;
117 
118  if (!options){
119    return NIL(BmcOption_t);
120  }
121 
122  options->dbgOut = 0;
123  /*
124   * Parse command line options.
125   */
126  util_getopt_reset();
127  while ((c = util_getopt(argc, argv, "E:C:S:F:O::I:hiv:m:k:s:o:t:d:r:e")) != EOF) {
128    switch(c) {
129    case 'F':
130      options->fairFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0);
131      if (options->fairFile == NIL(FILE)) {
132        (void) fprintf(vis_stdout,
133                       "** bmc error: Cannot open the file %s\n",
134                       util_optarg);
135        BmcOptionFree(options);
136        return NIL(BmcOption_t);
137      }
138      break;
139    case 'O':
140      options->dbgOut = Cmd_FileOpen(util_optarg, "w", NIL(char *), 0);
141      if(options->dbgOut == NIL(FILE)) {
142        (void) fprintf(vis_stdout, "**bmc error: Cannot open %s for debug information.\n", util_optarg);
143         BmcOptionFree(options);
144         return NIL(BmcOption_t);
145      } 
146      break;
147    case 'm':
148      for (i = 0; i < strlen(util_optarg); i++) {
149        if (!isdigit((int)util_optarg[i])) {
150          goto usage;
151        }
152      }
153      options->minK = atoi(util_optarg);
154      break;
155    case 'k':
156      for (i = 0; i < strlen(util_optarg); i++) {
157        if (!isdigit((int)util_optarg[i])) {
158          goto usage;
159        }
160      }
161      options->maxK = atoi(util_optarg);
162      break;
163    case 's':
164      for (i = 0; i < strlen(util_optarg); i++) {
165        if (!isdigit((int)util_optarg[i])) {
166          goto usage;
167        }
168      }
169      options->step = atoi(util_optarg);
170      break;
171    case 'r':
172      for (i = 0; i < strlen(util_optarg); i++) {
173        if (!isdigit((int)util_optarg[i])) {
174          goto usage;
175        }
176      }
177      options->inductiveStep = atoi(util_optarg);
178      break;
179    case 'e':
180      options->earlyTermination = TRUE;
181      break;   
182    case 'd':
183      for (i = 0; i < strlen(util_optarg); i++) {
184        if (!isdigit((int)util_optarg[i])) {
185          goto usage;
186        }
187      }
188      options->dbgLevel = atoi(util_optarg);
189      break;   
190    case 't' :
191      options->timeOutPeriod = atoi(util_optarg);
192        break;
193    case 'i':
194      options->printInputs = TRUE;
195      break;   
196    case 'h':
197      goto usage;
198    case 'v':
199      for (i = 0; i < strlen(util_optarg); i++) {
200        if (!isdigit((int)util_optarg[i])) {
201          goto usage;
202        }
203      }
204      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
205      break;
206    case 'o':
207      options->cnfFileName = util_strsav(util_optarg);
208      break;   
209    case 'I' :
210      options->incremental = atoi(util_optarg);
211      break;
212    case 'E':
213      for (i = 0; i < strlen(util_optarg); i++) {
214        if (!isdigit((int)util_optarg[i])) {
215          goto usage;
216        }
217      }
218      options->encoding = atoi(util_optarg);
219      if((options->encoding < 0) || (options->encoding > 2)){
220        goto usage;
221      }
222      break;
223    case 'S':
224      for (i = 0; i < strlen(util_optarg); i++) {
225        if (!isdigit((int)util_optarg[i])) {
226          goto usage;
227        }
228      }
229      options->satSolver = atoi(util_optarg);
230      if((options->satSolver < 0) || (options->satSolver > 1)){
231        goto usage;
232      }
233      break;
234    case 'C':
235      for (i = 0; i < strlen(util_optarg); i++) {
236        if (!isdigit((int)util_optarg[i])) {
237          goto usage;
238        }
239      }
240      options->clauses = atoi(util_optarg);
241      if((options->clauses < 0) || (options->clauses > 2)){
242        goto usage;
243      }
244      break;
245    default:
246      goto usage;
247    }
248  }
249  if (options->minK > options->maxK){
250    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
251    goto usage;
252  }
253  /*
254   * Open the ltl file.
255   */
256  if (argc - util_optind == 0) {
257    (void) fprintf(vis_stderr, "** bmc error: file containing ltl formulae not provided\n");
258    goto usage;
259  }
260  else if (argc - util_optind > 1) {
261    (void) fprintf(vis_stderr, "** bmc error: too many arguments\n");
262    goto usage;
263  }
264  ltlFileName = util_strsav(argv[util_optind]);
265 
266  /* Read LTL Formulae */
267  if (!ltlFileName) 
268      goto usage;
269
270  options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
271  if (options->ltlFile == NIL(FILE)) {
272    (void) fprintf(vis_stdout,"** bmc error: Cannot open the file %s\n", ltlFileName);
273    FREE(ltlFileName);
274    BmcOptionFree(options);
275    return NIL(BmcOption_t);
276  }
277  FREE(ltlFileName);
278  /* create SAT Solver input file */
279  if (options->cnfFileName == NIL(char)) {
280    options->satInFile = BmcCreateTmpFile(); 
281    if (options->satInFile == NIL(char)){
282      BmcOptionFree(options);
283      return NIL(BmcOption_t);
284    }
285  } else {
286    options->satInFile = options->cnfFileName;
287  }
288  /* create SAT Solver output file */
289  options->satOutFile = BmcCreateTmpFile();
290  if (options->satOutFile == NIL(char)){
291    BmcOptionFree(options);
292    return NIL(BmcOption_t);
293  }
294  return options;
295 
296 usage:
297  (void) fprintf(vis_stderr, "usage: bmc [-h][-m minimum_length][-k maximum_length][-s step][-r inductive_step][-e][-F <fairness_file>][-d debug_level][-E <encoding>][-C <clauses>][-S <sat_solver>][-O <debug_file>][-I <level>][-v verbosity_level][-t period][-o <cnf_file>] <ltl_file>\n");
298  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
299  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
300  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
301  (void) fprintf(vis_stderr, "   -s \tincrementing value of counterexample length (default is 1)\n");
302  (void) fprintf(vis_stderr, "   -r \tUse check for termination at each inductive_step to check if the property passes (default is 0).\n");
303  (void) fprintf(vis_stderr, "   -e \tUse early termination to check if the property passes. Valid only with -r \n"); 
304  (void) fprintf(vis_stderr, "   -F <fairness_file>\n");
305  (void) fprintf(vis_stderr, "   -d <debug_level>\n");
306  (void) fprintf(vis_stderr, "       debug_level = 0 => No debugging performed (Default)\n");
307  (void) fprintf(vis_stderr, "       debug_level = 1 => Debugging with minimal output: generate counter-example if the LTL formula fails.\n");
308  (void) fprintf(vis_stderr, "       debug_level = 2 => Debugging with full output in Aiger format: generate counter-example if the LTL formula fails.\n");
309  (void) fprintf(vis_stderr, "   -O <debug_file>\n");
310  (void) fprintf(vis_stderr, "   -i \tPrint input values in debug traces.\n");
311  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
312  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
313  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
314  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
315  (void) fprintf(vis_stderr, "   -t <period> time out period\n");
316  (void) fprintf(vis_stderr, "   -E <encoding>\n");
317  (void) fprintf(vis_stderr, "       encoding = 0 => Original BMC encoding (Default)\n");
318  (void) fprintf(vis_stderr, "       encoding = 1 => SNF encoding\n");
319  (void) fprintf(vis_stderr, "       encoding = 2 => Fixpoint encoding\n");
320  /*
321  (void) fprintf(vis_stderr, "       encoding = 3 => FNF encoding\n");
322  */
323  (void) fprintf(vis_stderr, "   -S <sat_solver>\n");
324  (void) fprintf(vis_stderr, "       sat_solver = 0 => CirCUs (Default)\n");
325  (void) fprintf(vis_stderr, "       sat_solver = 1 => cusp\n");
326  (void) fprintf(vis_stderr, "   -C <clauses>\n");
327  (void) fprintf(vis_stderr, "       clauses = 0 => Apply CirCUs on circuit (Default)\n");
328  (void) fprintf(vis_stderr, "       clauses = 1 => Apply SAT solver on CNF (new)\n");
329  (void) fprintf(vis_stderr, "       clauses = 2 => Apply SAT solver on CNF (old)\n");
330  (void) fprintf(vis_stderr, "   -I <level>\n");
331  (void) fprintf(vis_stderr, "       level = 1 => Trace Objective\n");
332  (void) fprintf(vis_stderr, "       level = 2 => Distill\n");
333  (void) fprintf(vis_stderr, "       level = 3 => Trace Objective + Distill\n");
334  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n");
335  (void) fprintf(vis_stderr, "   <ltl_file> The input file containing LTL formulae to be checked.\n");
336
337  BmcOptionFree(options);
338  return NIL(BmcOption_t);
339}
340
341/**Function********************************************************************
342
343  Synopsis [Alloc Memory for BmcOption_t.]
344
345  SideEffects []
346
347  SeeAlso []
348******************************************************************************/
349BmcOption_t *
350BmcOptionAlloc(void)
351{
352  BmcOption_t *result = ALLOC(BmcOption_t, 1);
353 
354  if (!result){
355    return result;
356  }
357  result->ltlFile = NIL(FILE);
358  result->fairFile = NIL(FILE);
359  result->cnfFileName = NIL(char);
360  result->minK = 0;
361  result->maxK = 1;
362  result->step = 1;
363  result->timeOutPeriod  = 0;
364  result->startTime = 0;
365  result->verbosityLevel = BmcVerbosityNone_c;
366  result->dbgLevel       = 0;
367  result->inductiveStep  = 0;
368  result->printInputs    = FALSE;
369  result->satSolverError = FALSE;
370  result->satInFile  = NIL(char);
371  result->satOutFile = NIL(char);
372  result->incremental = 0;
373  result->earlyTermination = 0;
374  result->satSolver = CirCUs;  /* default is 0 */
375  result->clauses   = 0;  /* default is 0 */
376  result->encoding  = 0;  /* default is 0 */
377  return result;
378}
379
380/**Function********************************************************************
381
382  Synopsis [Free BmcOption_t, and close files.]
383
384  SideEffects []
385
386  SeeAlso []
387******************************************************************************/
388void
389BmcOptionFree(
390  BmcOption_t *result)
391{
392  if (result->ltlFile != NIL(FILE)){
393    fclose(result->ltlFile);
394  }
395  if (result->cnfFileName != NIL(char)){
396    FREE(result->cnfFileName);
397  } else if (result->satInFile != NIL(char)) {
398    unlink(result->satInFile);
399    FREE(result->satInFile);
400  }
401  if (result->fairFile != NIL(FILE)){
402    fclose(result->fairFile);
403  }
404  if (result->satOutFile != NIL(char)) {
405    unlink(result->satOutFile);
406    FREE(result->satOutFile);
407  }
408  FREE(result);
409}
410
411/**Function********************************************************************
412
413  Synopsis    [Create a temporary file]
414
415  Description []
416
417  SideEffects []
418
419******************************************************************************/
420char *
421BmcCreateTmpFile(void)
422{
423#if HAVE_MKSTEMP && HAVE_CLOSE 
424  char   cnfFileName[] = "/tmp/vis.XXXXXX";
425  int    fd;
426#else
427  char   *cnfFileName;
428  char   buffer[512];
429#endif
430
431#if HAVE_MKSTEMP && HAVE_CLOSE   
432  fd = mkstemp(cnfFileName);
433  if (fd == -1){
434#else
435  cnfFileName = util_strsav(tmpnam(buffer));
436  if (cnfFileName == NIL(char)){
437#endif       
438    (void)fprintf(vis_stderr,"** bmc error: Can not create temporary file. ");
439    (void)fprintf(vis_stderr,"Clean up /tmp and try again.\n");
440    return NIL(char);
441  }
442#if HAVE_MKSTEMP && HAVE_CLOSE
443  close(fd);
444#endif   
445  return util_strsav(cnfFileName);
446} /* createTmpFile() */
447
448/*---------------------------------------------------------------------------*/
449/* Definition of static functions                                            */
450/*---------------------------------------------------------------------------*/
451
452
453/**Function********************************************************************
454
455  Synopsis    [Implements the bounded_model_check command]
456
457  CommandName [bounded_model_check]
458
459  CommandSynopsis [Performs a SAT-based LTL model checking on a flattened network]
460
461  CommandArguments [\[-h\] \[-v &lt;verbosity_level&gt;\]
462                    \[-m &lt;minimum_length&gt;\] \[-k &lt;maximum_length&gt;\] \[-s &lt;step_value&gt;\]
463                    \[-r &lt;termination_check_step&gt;\] \[-e\]
464                    \[-F &lt;fairness_file&gt;\]
465                    \[-S &lt;sat_solver&gt;\] \[-E &lt;encoding&gt;\]
466                    \[-C &lt;clause_type&gt;\] \[-I &lt;inc_level&gt;\]
467                    \[-d &lt;dbg_level&gt;\] \[-t &lt;timeOutPeriod&gt;\]
468                    \[-o &lt;cnf_file&gt;\] \[-i\]
469                    \[-O &lt;debug_file&gt;\] &lt;ltl_file&gt; ]
470                   
471  CommandDescription [Performs a SAT-based LTL bounded model checking (BMC) on
472  a flattened network. This command looks for a counterexample of length <code>
473  k </code> ( minimum_length &le; <code> k </code> &le; maximum_length). If
474  <code> -r </code> is specified, this command performs check for termination
475  after each <code> termination_check_step </code>.  If no counterexample is
476  found, this command increases <code> k </code> by step_value (specifies by
477  the <code> -s </code> option) until a counterexample is found, the search
478  becomes intractable (timed out), or <code> k </code> reaches a bound
479  (determine by the check for termination), and then we conclude that the LTL
480  property passes.
481
482  This command implements the basic encoding of Bounded Model Checking (BMC) as
483  descibed in the paper "Symbolic Model Checking without BDDs".  However, the
484  <code> -E </code> option can be used to select other encoding scheme.  We
485  also applied some of the improvements in the BMC encoding described in the
486  paper "Improving the Encoding of LTL Model Checking into SAT".
487 
488  To prove that an LTL property passes, we implement the termination methods
489  that are descirebed in the papers "Checking Safety Properties Using Induction
490  and a SAT-Solver" and "Proving More Properties with Bounded Model Checking".
491 
492  Before calling this command, the user should have initialized the design by
493  calling the command <A HREF="flatten_hierarchyCmd.html"> <code>
494  flatten_hierarchy</code></A>. If the user uses the -r option and the LTL
495  property is a general LTL property, the command <A
496  HREF="build_partition_maigsCmd.html"> <code> build_partition_maigs</code></A>
497  must be called.  The aig graph must be built by calling the command <A
498  HREF="build_partition_mddsCmd.html"> <code>build_partition_mdds</code></A>
499  <p>
500 
501  Command options:
502  <p>
503  <dl>
504  <dt> -h
505  <dd> Print the command usage.
506 
507  <p>
508  <dt>-m <code>&lt;minimum_length&gt;</code>
509  <dd>Minimum length of counterexample to be checked (default is 0).
510
511  <dt>-k <code>&lt;maximum_length&gt;</code>
512  <dd>Maximum length of counterexample to be checked (default is 1).
513
514  <dt>-s <code>&lt;step_value&gt;</code>
515  <dd>Incrementing value of counterexample length (default is 1).
516
517  <dt>-r <code>&lt;termination_check_step&gt;</code>
518  <dd>Check for termination for each termination_check_step (default is 0). 0 means don't check for termination.
519
520  <dt>-e
521  <dd> Activate early termination check.  Check if there is no simple path starts from an initial state.
522       Valid only for general LTL and safety properties. Must be used with -r option.
523 
524  <dt>-S <code>&lt;sat_solver&gt;</code>
525  <dd> Specify SAT solver
526  <br><code>sat_solver</code>  must be one of the following:<p>
527  <code>0</code>: CirCUs (Default) <p>
528  <code>1</code>: zChaff <p>
529
530  <dt>-E <code>&lt;encoding&gt;</code>
531  <dd> Specify encoding scheme
532  <br><code>encoding</code>  must be one of the following:<p>
533  <code>0</code>: The original BMC encoding (Default) <p>
534  <code>1</code>: SNF encoding <p>
535  <code>2</code>: Fixpoint encoding <p>
536
537  <dt>-C <code>&lt;clause_type&gt;</code>
538  <dd> Specify clause type
539  <br><code>encoding</code>  must be one of the following:<p>
540  <code>0</code>: Apply CirCUs SAT solver on circuit (Default) <p>
541  <code>1</code>: Apply SAT solver on CNF generated form circuit<p>
542  <code>2</code>: Apply SAT solver on CNF <p>
543
544  <dt>-I <code>&lt;inc_level&gt;</code>
545  <dd> Specify increment sat solver type
546  <br><code>encoding</code>  must be one of the following:<p>
547  <code>1</code>: Trace Objective (Default) <p>
548  <code>2</code>: Distill <p>
549  <code>3</code>: Trace Objective + Distill <p>
550
551  <dt>-F <code>&lt;fairness_file&gt;</code>
552  <dd> Read fairness constraints from <code>&lt;fairness_file&gt;</code>.  Each
553  formula in the file is a condition that must hold infinitely often on a fair
554  path.
555 
556  <dt>-o <code>&lt;cnf_file&gt;</code>
557  Save CNF formula in <code>&lt;cnf_file&gt;</code>
558
559  <dt>-O <code>&lt;debug_file&gt;</code>
560  Save counterexample to <code>&lt;debug_file&gt;</code>
561 
562  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
563  <dd> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
564  <p>
565  <dt> -v  <code>&lt;verbosity_level&gt;</code>
566  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage and code status.
567
568  <br><code>verbosity_level</code>  must be one of the following:<p>
569 
570  <code>0</code>: No feedback provided. This is the default.<p>
571
572  <code>1</code>: Feedback on code location.<p>
573
574  <code>2</code>: Feedback on code location and CPU usage.<p>
575
576  <dt> -d <code> &lt;dbg_level&gt; </code> <dd> Specify the amount of
577  debugging performed when the BMC models check the LTL formula.
578  <p> <dd> <code> dbg_level</code> must be one
579  of the following:
580
581  <p><code>0</code>: No debugging performed.
582  <code>dbg_level</code>=<code>0</code> is the default.
583
584  <p><code>1</code>: Debugging with minimal output: generate counter-example
585  if the LTL formula fails and the counterexample length.
586
587  <p>
588  <dt> -i
589  <dd> Print input values causing transitions between states during debugging.
590  <p>
591 
592  <dt> <code> &lt;ltl_file&gt; </code>
593  <dd> File containing LTL formulae to be checked.
594 
595  </dl>
596  ]
597
598  SideEffects []
599
600  SeeAlso     [Ntk_NetworkAddApplInfo]
601
602******************************************************************************/
603static int
604CommandBmc(
605  Hrc_Manager_t ** hmgr,
606  int              argc,
607  char          ** argv)
608{
609  Ntk_Network_t     *network;
610  BmcOption_t       *options;
611  int               i;
612  array_t           *formulaArray;
613  array_t           *LTLformulaArray;
614  bAig_Manager_t    *manager;
615  array_t           *constraintArray = NIL(array_t);
616
617  /*
618   * Parse command line options.
619   */
620  if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
621      return 1;
622  }
623  /*
624   * Read the network
625   */
626  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
627  if (network == NIL(Ntk_Network_t)) {
628    (void) fprintf(vis_stdout, "** bmc error: No network\n");
629    BmcOptionFree(options);
630    return 1;
631  }
632  manager = Ntk_NetworkReadMAigManager(network);
633  if (manager == NIL(mAig_Manager_t)) {
634    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
635    BmcOptionFree(options);
636    return 1;
637  }
638  /*
639    We need the bdd when building the transition relation of the automaton
640  */
641  if(options->inductiveStep !=0){
642    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
643 
644    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
645    if (designFsm == NIL(Fsm_Fsm_t)) {
646      return 1;
647    }
648  }
649  /* time out */
650  if (options->timeOutPeriod > 0) {
651    /* Set the static variables used by the signal handler. */
652    bmcTimeOut = options->timeOutPeriod;
653    alarmLapTime = options->startTime = util_cpu_ctime();
654    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
655    (void) alarm(options->timeOutPeriod);
656    if (setjmp(timeOutEnv) > 0) {
657      (void) fprintf(vis_stdout,
658                     "\n# BMC: timeout occurred after %d seconds.\n",
659                     options->timeOutPeriod);
660      (void) fprintf(vis_stdout, "# BMC: data may be corrupted.\n");
661      BmcOptionFree(options);
662      alarm(0);
663      return 1;
664    }
665  }
666  formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
667  if (formulaArray == NIL(array_t)) {
668    (void) fprintf(vis_stderr,
669                   "** bmc error: error in parsing CTL* Fromula from file\n");
670    BmcOptionFree(options);
671    return 1;
672  }
673  if (array_n(formulaArray) == 0) {
674    (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
675    BmcOptionFree(options);
676    Ctlsp_FormulaArrayFree(formulaArray);
677    return 1;
678  }
679  LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
680  Ctlsp_FormulaArrayFree(formulaArray);
681  if (LTLformulaArray ==  NIL(array_t)){
682    (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
683    BmcOptionFree(options);
684    return 1;
685  }
686  if (options->fairFile != NIL(FILE)) {
687    constraintArray = BmcReadFairnessConstraints(options->fairFile);
688    if(constraintArray == NIL(array_t)){
689      Ctlsp_FormulaArrayFree(LTLformulaArray);
690      BmcOptionFree(options);
691      return 1;
692    }
693    if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){
694      Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray,
695                                                  constraintArray);
696      Ctlsp_FormulaArrayFree(constraintArray);
697      constraintArray = NIL(array_t);
698    }
699  }
700  /*
701    Call a proper BMC function based on LTL formula.
702  */
703  for (i = 0; i < array_n(LTLformulaArray); i++) { 
704    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *,
705                                                  LTLformulaArray, i);
706   
707    DispatchBmcCommand(network, ltlFormula, constraintArray, options);
708  }
709  /*
710    Free used memeory
711  */
712  if (constraintArray != NIL(array_t)){
713    Ctlsp_FormulaArrayFree(constraintArray);
714  }
715  Ctlsp_FormulaArrayFree(LTLformulaArray);
716  BmcOptionFree(options);
717  fflush(vis_stdout);
718  fflush(vis_stderr);
719  alarm(0);
720  return 0;
721
722}/* CommandBmc() */
723
724/**Function********************************************************************
725
726  Synopsis    [Handle function for timeout.]
727
728  Description [This function is called when the time out occurs.
729  Since alarm is set with an elapsed time, this function checks if the
730  CPU time corresponds to the timeout of the command.  If not, it
731  reprograms the alarm to fire again later.]
732
733  SideEffects []
734
735******************************************************************************/
736static void
737TimeOutHandle(void)
738{
739  int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000);
740
741  if (seconds < bmcTimeOut) {
742    unsigned slack = (unsigned) (bmcTimeOut - seconds);
743    (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle);
744    (void) alarm(slack);
745  } else {
746    longjmp(timeOutEnv, 1);
747  }
748} /* TimeOutHandle */
749
750
751/**Function********************************************************************
752
753  Synopsis    [Dispatch BMC]
754
755  Description [Call a proper BMC routine.
756
757  The -E for BMC encoding scheme
758      -C clause generation
759      -S SAT solver   0  CirCUs
760                      1 zChaff
761
762  ]
763
764  SideEffects []
765
766******************************************************************************/
767static void
768DispatchBmcCommand(
769  Ntk_Network_t   *network,
770  Ctlsp_Formula_t *ltlFormula,
771  array_t         *constraintArray,
772  BmcOption_t     *options)
773{
774  Ctlsp_Formula_t *negLtlFormula = Ctlsp_LtllFormulaNegate(ltlFormula);
775  st_table        *CoiTable      = st_init_table(st_ptrcmp, st_ptrhash);
776
777  assert(ltlFormula != NIL(Ctlsp_Formula_t));
778  assert(network != NIL(Ntk_Network_t));
779 
780  /*
781    print out the given LTL formula
782  */
783  fprintf(vis_stdout, "Formula: ");
784  Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
785  fprintf(vis_stdout, "\n");
786  if (options->verbosityLevel >= BmcVerbosityMax_c){
787    fprintf(vis_stdout, "Negated formula: ");
788    Ctlsp_FormulaPrint(vis_stdout, negLtlFormula);
789    fprintf(vis_stdout, "\n");
790  }
791  /*
792    Compute the cone of influence of the LTL formula
793  */
794  BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable);
795
796  if(options->clauses == 2){
797    /*
798      Generate clauses for each time frame.  This is the old way of generating
799      clauses in BMC.
800    */
801    if (constraintArray != NIL(array_t)){
802      BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
803                             constraintArray, options);
804    } else /*
805             If the LTL formula is propositional.
806           */
807      if(Ctlsp_isPropositionalFormula(negLtlFormula)){
808        BmcLtlVerifyProp(network, negLtlFormula, CoiTable, options);
809      } else /*
810               If the LTL formula is of type G(p) (its negation is
811               of type F(q)), where p and q are propositional.
812             */
813        if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){
814          BmcLtlVerifyGp(network, negLtlFormula, CoiTable, options);
815        } else /*
816                 If the LTL formula is of type F(p) (its negation is
817                 of type G(q)), where p and q are propositional.
818               */
819          if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){
820            BmcLtlVerifyFp(network, negLtlFormula, CoiTable, options);
821          } else /*
822                   If the depth of the LTL formula (the maximum level
823                   of nesting temporal operators) = 1
824                 */
825            /*
826            if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){
827              BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options);
828            } else
829            */
830              /*
831                 If the LTL formula is of type FG(p) (its negation is
832                 of type GF(q)), where p and q are propositional.
833              */
834              if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){
835                BmcLtlVerifyFGp(network, negLtlFormula, CoiTable, options);
836              } else
837                /*
838                  All other LTL formulae
839                */
840                BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable,
841                                       NIL(array_t), options);
842  } else {
843    /*
844     Build AIG for each time frame.
845     */
846    if (constraintArray != NIL(array_t)){
847      if(options->encoding == 0){
848       BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
849                                    CoiTable,
850                                   constraintArray, options, 0);
851      } else 
852        if(options->encoding == 1){
853          BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
854                                          CoiTable,
855                                          constraintArray, options, 1);
856        } else 
857          if(options->encoding == 2){
858            BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
859                                                 CoiTable,
860                                                 constraintArray, options);
861          }
862    } else
863      /*
864        If the LTL formula is propositional.
865      */
866      if(Ctlsp_isPropositionalFormula(negLtlFormula)){
867        BmcCirCUsLtlVerifyProp(network, negLtlFormula, CoiTable, options);
868      } else
869        /*
870          If the LTL formula is of type G(p) (its negation is
871          of type F(q)), where p and q are propositional.
872        */
873        if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){
874          BmcCirCUsLtlVerifyGp(network, negLtlFormula, CoiTable, options);
875        } else
876          /*
877            If the LTL formula is of type F(p) (its negation is
878            of type G(q)), where p and q are propositional.
879          */
880          if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){
881            BmcCirCUsLtlVerifyFp(network, negLtlFormula, CoiTable, options);
882          } else
883            /*
884              If the depth of the LTL formula (the maximum level
885              of nesting temporal operators) = 1
886             
887              if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){
888              BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options);
889              } else
890               
891              If the LTL formula is of type FG(p) (its negation is
892              of type GF(q)), where p and q are propositional.
893            */
894            if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){
895              BmcCirCUsLtlVerifyFGp(network, negLtlFormula, CoiTable, options);
896            } else
897              if(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(negLtlFormula) ||
898                 (Ltl_AutomatonGetStrength(BmcAutLtlToAutomaton(network,ltlFormula)) == 0))
899                {
900                  BmcCirCUsLtlCheckSafety(network, negLtlFormula, options, CoiTable);
901                }
902              else {
903                /*
904                  All other LTL formulae
905                */
906                if(options->encoding == 0){
907                  BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
908                                               CoiTable,
909                                               NIL(array_t), options, 0);
910                } else 
911                  if(options->encoding == 1){
912                    BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula,
913                                                    CoiTable,
914                                                    NIL(array_t), options, 1);
915                  } else 
916                    if(options->encoding == 2){
917                      BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula,
918                                                 CoiTable,
919                                                           NIL(array_t), options);
920                    }
921              } 
922  }
923 
924  st_free_table(CoiTable);
925  Ctlsp_FormulaFree(negLtlFormula);
926} /* DispatchBmcCommand() */
927
928
929/**Function********************************************************************
930
931  Synopsis    [cnf_sat]
932
933  Description []
934 
935  CommandName [cnf_sat]
936
937  CommandSynopsis [Perform SAT solving with CNF input]
938
939  CommandArguments [\[-h\] \[-a &lt;assgined_filename&gt;\]
940                    \[-f &lt;output_filename&gt;\]
941                    \[-t &lt;timeout&gt;\]
942                    \[-v &lt;verbose&gt;\]
943                    \[-b\] &lt;cnf_filename&gt; ]
944                   
945
946  CommandDescription [Perform SAT solving with CirCUs after reading CNF file
947  <p>
948  <dt> -b
949
950  <dd> If the given CNF has small number of variables and clause then
951  the BDD is built from the CNF clauses. If the monolithic BDD is built
952  then we can conclude SAT or UNSAT, otherwise the normal SAT algorithm
953  is invoked.
954
955  <p>
956  <p>
957  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
958
959  <dd> Specify the time out period (in seconds) after which the command
960  aborts. By default this option is set to infinity.
961
962  <p>
963
964  <p>
965  <dt> -f  <code>&lt;output_filename&gt;</code>
966  <dd> Specify the output filename to save the satisfying assignments and
967  the statistics of SAT solving.
968  <p>
969
970  ]
971
972  SideEffects []
973
974  SeeAlso     []
975
976******************************************************************************/
977
978static int
979CommandCnfSat(
980  Hrc_Manager_t ** hmgr,
981  int  argc,
982  char ** argv)
983{
984  satOption_t *option;
985  char *filename, c;
986  char *forcedAssignFilename;
987  int timeOutPeriod, i;
988
989  option = sat_InitOption();
990  timeOutPeriod = -1;
991  forcedAssignFilename = 0;
992  util_getopt_reset();
993  while ((c = util_getopt(argc, argv, "a:bf:ht:v:c:")) != EOF) {
994    switch(c) {
995      case 'h':
996        goto usage;
997      case 'b' :
998        option->BDDMonolithic = 1;
999        break;
1000      case 'f' :
1001        option->outFilename = strdup(util_optarg);
1002        break;
1003      case 'a' :
1004        forcedAssignFilename = strdup(util_optarg);
1005        break;
1006      case 't' :
1007        timeOutPeriod = atoi(util_optarg);
1008        break;
1009      case 'v':
1010        for (i = 0; i < (int)(strlen(util_optarg)); i++) {
1011          if (!isdigit((int)util_optarg[i])) {
1012            goto usage;
1013          }
1014        }
1015        option->verbose = (Bmc_VerbosityLevel) atoi(util_optarg);
1016        break;
1017
1018        //Bing: for unsat core
1019      case 'c':
1020        option->coreGeneration = 1;
1021        option->unsatCoreFileName = strdup(util_optarg);
1022        option->minimizeConflictClause = 0;
1023        option->clauseDeletionHeuristic = 0;
1024        break;
1025      default:
1026        goto usage;
1027    }
1028  }
1029
1030  if (argc - util_optind == 0) {
1031    (void) fprintf(vis_stderr, "** ERROR : file containing cnf file not provided\n");
1032    goto usage;
1033  }
1034  else if (argc - util_optind > 1) {
1035    (void) fprintf(vis_stderr, "** ERROR : too many arguments\n");
1036    goto usage;
1037  }
1038  filename = util_strsav(argv[util_optind]);
1039
1040  if(forcedAssignFilename)
1041    option->forcedAssignArr = sat_ReadForcedAssignment(forcedAssignFilename);
1042
1043  if (timeOutPeriod > 0) {
1044    bmcTimeOut = timeOutPeriod;
1045    alarmLapTime = util_cpu_ctime();
1046    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
1047    (void) alarm(timeOutPeriod);
1048    if (setjmp(timeOutEnv) > 0) {
1049      (void) fprintf(vis_stderr,
1050                "** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod);
1051      alarm(0);
1052      return 1;
1053    }
1054  }
1055
1056  sat_CNFMain(option, filename);
1057
1058  return 0;
1059
1060  usage:
1061  (void) fprintf(vis_stderr, "usage: cnf_sat [-h] [-v verboseLevel] [-t timeout] <cnf_file>\n");
1062  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
1063  (void) fprintf(vis_stderr, "   -a <filename> \tto make forced assignment\n");
1064  (void) fprintf(vis_stderr, "   -f <filename> \twrite log to the file\n");
1065  (void) fprintf(vis_stderr, "   -b \tuse BDD based method\n");
1066  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
1067  (void) fprintf(vis_stderr, "   -t <period> time out period\n");
1068  (void) fprintf(vis_stderr, "   -c <filename> UNSAT core generation\n");
1069  (void) fprintf(vis_stderr, "   <cnf_file> CNF file to be checked.\n");
1070  return 1;
1071}
1072
1073
1074#if 0
1075/**Function********************************************************************
1076
1077  Synopsis    [Implements the bdd_sat command.]
1078
1079  Description [This command integrates BDD-based methods with SAT-based method
1080  to model safety property of the form AG(p). Where p is either a propositional
1081  formula or a path formula consists of only the temporal operator X.]
1082 
1083  CommandName [bdd_sat_bounded_model_check]
1084
1085  CommandSynopsis [performs an LTL bounded model checking on a flattened network]
1086
1087  CommandArguments [\[-h\] \[-v &lt;verbosity_level&gt;\]  \[-d &lt;dbg_level&gt;\] \[-i\]
1088                    -m &lt;minimum_length&gt; -k &lt;maximum_length&gt; -s &lt;step_value&gt;
1089                    -o &lt;cnf_file&gt; &lt;ltl_file&gt; ]
1090
1091                    -F &lt;fairness_file&gt; -o &lt;cnf_file&gt; &lt;ltl_file&gt; ]
1092
1093  CommandDescription [Performs an LTL bounded model checking on a flattened
1094  network. This command looks for a counterexample of length &ge; minimum_length
1095  and &le; maximum_length. It increments the length by step_value.
1096 
1097  Before calling this command, the user should have initialized the design
1098  by calling the command <A HREF="flatten_hierarchyCmd.html"> <code>
1099  flatten_hierarchy</code></A>, and
1100  then calling the command <A HREF="build_partition_maigsCmd.html"> <code>
1101  build_partition_maigs</code></A>.<p>
1102  The value of maximum length must be >= minimum length.<p>
1103
1104  Command options:
1105  <p>
1106
1107  <dl>
1108
1109  <dt> -h
1110  <dd> Print the command usage.
1111  <p>
1112
1113  <dt>-m <code>&lt;minimum_length&gt;</code>
1114  <dd>Minimum length of counterexample to be checked (default is 0).
1115
1116  <dt>-k <code>&lt;maximum_length&gt;</code>
1117  <dd>Maximum length of counterexample to be checked (default is 1).
1118
1119  <dt>-s <code>&lt;step_value&gt;</code>
1120  <dd>Incrementing value of counterexample length (default is 1).
1121
1122  <dt>-r <code>&lt;inductive_Step&gt;</code>
1123  <dd>Use inductive proof at each step_value to check if the property passes (default is 0). 0 means
1124  don't use the inductive proof. BMC will check using the indcution if the property passes if the current
1125  length of the counterexample is a multiple of inductive_Step.
1126 
1127  <dt>-F <code>&lt;fairness_file&gt;</code>
1128  <dd> Read fairness constraints from <code>&lt;fairness_file&gt;</code>.  Each
1129  formula in the file is a condition that must hold infinitely often on a fair
1130  path.
1131
1132  <dt>-o <code>&lt;cnf_file&gt;</code>
1133  Save the CNF formula in <code>&lt;cnf_file&gt;</code>
1134 
1135  <dt> -t  <code>&lt;timeOutPeriod&gt;</code>
1136  <dd> Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.
1137  <p>
1138  <dt> -v  <code>&lt;verbosity_level&gt;</code>
1139  <dd> Specify verbosity level. This sets the amount of feedback  on CPU usage and code status.
1140
1141  <br><code>verbosity_level</code>  must be one of the following:<p>
1142 
1143  <code>0</code>: No feedback provided. This is the default.<p>
1144
1145  <code>1</code>: Feedback on code location.<p>
1146
1147  <code>2</code>: Feedback on code location and CPU usage.<p>
1148
1149  <dt> -d <code> &lt;dbg_level&gt; </code> <dd> Specify the amount of
1150  debugging performed when the BMC models check the LTL formula.
1151  <p> <dd> <code> dbg_level</code> must be one
1152  of the following:
1153
1154  <p><code>0</code>: No debugging performed.
1155  <code>dbg_level</code>=<code>0</code> is the default.
1156
1157  <p><code>1</code>: Debugging with minimal output: generate counter-example
1158  if the LTL formula fails and the counterexample length.
1159
1160  <p>
1161 
1162  <dt> -h
1163  <dd> Print the command usage.
1164  <p>
1165
1166  <dt> -i
1167  <dd> Print input values causing transitions between states during debugging.
1168  <p>
1169
1170  <dt> -o <code>&lt;cnf_file&gt</code>;
1171  <dd> File containing CNF of the counterexample if exist. If specifies, the
1172  user can exam this file looking for information about the generated path.
1173  This file will be the input to the SAT solver.  The contents of this file
1174  is in dimacs format.
1175 
1176  <dt> <code> &lt;ltl_file&gt; </code>
1177  <dd> File containing LTL formulas to be model checked.
1178 
1179  </dl>
1180  ]
1181
1182  SideEffects []
1183
1184  SeeAlso     [Ntk_NetworkAddApplInfo]
1185
1186******************************************************************************/
1187int
1188CommandBddSat(
1189  Hrc_Manager_t ** hmgr,
1190  int              argc,
1191  char          ** argv)
1192{
1193  Ntk_Network_t     *network;
1194  BmcOption_t       *options;
1195  array_t           *formulaArray;
1196  bAig_Manager_t    *mAigManager;
1197  Fsm_Fsm_t         *fsm;
1198  mdd_manager       *mddManager;
1199  int               startTime;
1200
1201
1202  /*
1203   * Parse command line options.
1204   */
1205  if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
1206      return 1;
1207  }
1208  /* Read the network */
1209  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1210  if (network == NIL(Ntk_Network_t)) {
1211    (void) fprintf(vis_stdout, "** bdd_sat error: No network\n");
1212    BmcOptionFree(options);
1213    return 1;
1214  }
1215  /* read fsm */
1216  fsm = Fsm_NetworkReadOrCreateFsm(network);
1217  if (fsm == NIL(Fsm_Fsm_t)) {
1218    (void) fprintf(vis_stdout, "** bdd_sat error: Can't read or create fsm\n");
1219    BmcOptionFree(options);
1220    return 1;
1221  }
1222  mddManager = Fsm_FsmReadMddManager(fsm); /* mdd manager */
1223 
1224  mAigManager = Ntk_NetworkReadMAigManager(network);
1225  if (mAigManager == NIL(mAig_Manager_t)) {
1226    (void) fprintf(vis_stdout, "** bdd_sat error: run build_partition_maigs command first\n");
1227    BmcOptionFree(options);
1228    return 1;
1229  }
1230  formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile);
1231  if (formulaArray == NIL(array_t)) {
1232    (void) fprintf(vis_stderr,
1233                   "** bdd_sat error: Error in parsing CTL* Fromula from file\n");
1234    BmcOptionFree(options);
1235    return 1;
1236  }
1237  if (array_n(formulaArray) == 0) {
1238    (void) fprintf(vis_stderr, "** bdd_sat error: No formula in file\n");
1239    BmcOptionFree(options);
1240    array_free(formulaArray);
1241    return 1;
1242  }
1243  /* time out */
1244  if (options->timeOutPeriod > 0) {
1245    /* Set the static variables used by the signal handler. */
1246    bmcTimeOut = options->timeOutPeriod;
1247    alarmLapTime = options->startTime = util_cpu_ctime();
1248    (void) signal(SIGALRM, (void(*)(int))TimeOutHandle);
1249    (void) alarm(options->timeOutPeriod);
1250    if (setjmp(timeOutEnv) > 0) {
1251      (void) fprintf(vis_stdout,
1252                     "\n# bdd_sat: timeout occurred after %d seconds.\n",
1253                     options->timeOutPeriod);
1254      (void) fprintf(vis_stdout, "# bdd_sat: data may be corrupted.\n");
1255      BmcOptionFree(options);
1256      alarm(0);
1257      return 1;
1258    }
1259  }
1260  /* bdd and sat to model check the LTL property.*/
1261  BmcBddSat(network, formulaArray, options);
1262
1263  Ctlsp_FormulaArrayFree(formulaArray);
1264  fflush(vis_stdout);
1265  fflush(vis_stderr);
1266  BmcOptionFree(options);
1267  alarm(0);
1268  return 0; /* normal exit */
1269}/* CommandBddSat() */
1270#endif
1271
1272
1273int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv)
1274{
1275  Ntk_Network_t     *network;
1276  bAig_Manager_t    *manager;
1277  array_t           *formulaArray;
1278  array_t           *LTLformulaArray;
1279  char              * outFileName = NIL(char); 
1280  char              * ltlFileName = NIL(char); 
1281  FILE * ltlFile;
1282  FILE * outFile;
1283  int c,i;
1284  int maxK = 0;
1285  st_table          *allLatches;
1286  BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
1287
1288
1289  outFile = vis_stdout ; 
1290  // Parse option
1291  util_getopt_reset();
1292  while ((c = util_getopt(argc, argv, "f:o:k:h")) != EOF) {
1293    switch(c) {
1294      case 'h':
1295        goto usage;
1296      case 'o' :
1297        outFileName = strdup(util_optarg);
1298    outFile = Cmd_FileOpen(outFileName, "w", NIL(char *), 0); 
1299        break;
1300      case 'f' :
1301        ltlFileName = strdup(util_optarg);
1302        break;
1303    case 'k':
1304      for (i = 0; i < strlen(util_optarg); i++) {
1305        if (!isdigit((int)util_optarg[i])) {
1306          goto usage;
1307        }
1308      }
1309      maxK = atoi(util_optarg);
1310      break;
1311
1312        break;
1313      default:
1314        goto usage;
1315    }
1316  }
1317  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
1318  if (network == NIL(Ntk_Network_t)) {
1319    (void) fprintf(vis_stdout, "** bmc error: No network\n");
1320    return 1;
1321  }
1322  manager = Ntk_NetworkReadMAigManager(network);
1323  if (manager == NIL(mAig_Manager_t)) {
1324    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
1325    return 1;
1326  }
1327   
1328    //    Create a clause database
1329     
1330    cnfClauses = BmcCnfClausesAlloc();
1331    // Gnerate clauses for an initialized path of length k
1332    // nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph
1333     st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
1334     assert(nodeToMvfAigTable != NIL(st_table));
1335      allLatches = st_init_table(st_ptrcmp, st_ptrhash);
1336
1337     // Get all the latches of the network
1338          lsGen           gen ;
1339          Ntk_Node_t            *node;
1340        Ntk_NetworkForEachNode(network,gen, node){
1341                if (Ntk_NodeTestIsLatch(node)){
1342                        st_insert(allLatches, (char *) node, (char *) 0);
1343                }
1344        }
1345
1346
1347    BmcCnfGenerateClausesForPath(network, 0, maxK, BMC_INITIAL_STATES,
1348                                 cnfClauses, nodeToMvfAigTable, allLatches);
1349
1350// If ltl file exists
1351 if(ltlFileName != NIL(char))
1352  { 
1353    ltlFile =  Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0);
1354  formulaArray  = Ctlsp_FileParseFormulaArray(ltlFile);
1355  if (formulaArray == NIL(array_t)) {
1356    (void) fprintf(vis_stderr,
1357                   "** bmc error: error in parsing ltl Fromula from file\n");
1358      return 1;
1359   }
1360    LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
1361    for (i = 0; i < array_n(LTLformulaArray); i++) { 
1362    Ctlsp_Formula_t *ltlFormula     = array_fetch(Ctlsp_Formula_t *,
1363                                                  LTLformulaArray, i);
1364    BmcGenerateCnfForLtl(network, ltlFormula, 0, maxK, 0, cnfClauses);
1365}
1366  }
1367
1368
1369// Write Clauses
1370
1371  st_generator *stGen;
1372  char         *name;
1373  int          cnfIndex,k;
1374
1375    st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) {
1376    fprintf(outFile, "c %s %d\n",name, cnfIndex);
1377  }
1378  (void) fprintf(outFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1,
1379                 cnfClauses->noOfClauses);
1380  if (cnfClauses->clauseArray != NIL(array_t)) {
1381    for (i = 0; i < cnfClauses->nextIndex; i++) {
1382      k = array_fetch(int, cnfClauses->clauseArray, i);
1383      (void) fprintf(outFile, "%d%c", k, (k == 0) ? '\n' : ' ');
1384    }
1385  }
1386 if(outFileName != NIL(char))
1387   fclose(outFile);
1388   
1389   return 1;
1390
1391   usage:
1392  (void) fprintf(vis_stderr, "usage: write_cnf [-h] [-f ltl file] [-o outfile] [k]\n");
1393  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
1394  (void) fprintf(vis_stderr, "   -f <filename> \tto add a ltlfile\n");
1395  (void) fprintf(vis_stderr, "   -o <filename> \twrite output in outputfile\n");
1396  (void) fprintf(vis_stderr, "   -k <value> \tnumber of unroll steps\n");
1397  return 1;
1398 
1399}
Note: See TracBrowser for help on using the repository browser.