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

Last change on this file since 25 was 15, checked in by cecile, 13 years ago

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