/**CFile*********************************************************************** FileName [bmcCmd.c] PackageName [bmc] Synopsis [Command interface for bounded model checking (bmc)] Author [Mohammad Awedh] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "bmcInt.h" static char rcsid[] UNUSED = "$Id: bmcCmd.c,v 1.83 2010/04/09 23:50:57 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static jmp_buf timeOutEnv; static int bmcTimeOut; /* timeout value */ static long alarmLapTime; /* starting CPU time for timeout */ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ /*static*/ BmcOption_t * ParseBmcOptions(int argc, char **argv); static int CommandBmc(Hrc_Manager_t ** hmgr, int argc, char ** argv); static int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv); static void TimeOutHandle(void); static void DispatchBmcCommand(Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options); static int CommandCnfSat(Hrc_Manager_t ** hmgr, int argc, char ** argv); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes the BMC package.] SideEffects [] SeeAlso [Bmc_End] ******************************************************************************/ void Bmc_Init(void) { Cmd_CommandAdd("bounded_model_check", CommandBmc, /* doesn't change network */ 0); Cmd_CommandAdd("cnf_sat", CommandCnfSat, /* doesn't change network */ 0); Cmd_CommandAdd("write_cnf", CommandWriteCnf, /* doesn't change network */ 0); } /**Function******************************************************************** Synopsis [Ends BMC package.] SideEffects [] SeeAlso [Bmc_Init] ******************************************************************************/ void Bmc_End(void) { } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Parse the user input for command "bmc".] Description [] SideEffects [] ******************************************************************************/ /*static*/ BmcOption_t * ParseBmcOptions( int argc, char **argv) { BmcOption_t *options = BmcOptionAlloc(); char *ltlFileName = NIL(char); unsigned int i; int c; if (!options){ return NIL(BmcOption_t); } options->dbgOut = 0; /* * Parse command line options. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "E:C:S:F:O::I:hiv:m:k:s:o:t:d:r:e")) != EOF) { switch(c) { case 'F': options->fairFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 0); if (options->fairFile == NIL(FILE)) { (void) fprintf(vis_stdout, "** bmc error: Cannot open the file %s\n", util_optarg); BmcOptionFree(options); return NIL(BmcOption_t); } break; case 'O': options->dbgOut = Cmd_FileOpen(util_optarg, "w", NIL(char *), 0); if(options->dbgOut == NIL(FILE)) { (void) fprintf(vis_stdout, "**bmc error: Cannot open %s for debug information.\n", util_optarg); BmcOptionFree(options); return NIL(BmcOption_t); } break; case 'm': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->minK = atoi(util_optarg); break; case 'k': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->maxK = atoi(util_optarg); break; case 's': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->step = atoi(util_optarg); break; case 'r': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->inductiveStep = atoi(util_optarg); break; case 'e': options->earlyTermination = TRUE; break; case 'd': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->dbgLevel = atoi(util_optarg); break; case 't' : options->timeOutPeriod = atoi(util_optarg); break; case 'i': options->printInputs = TRUE; break; case 'h': goto usage; case 'v': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg); break; case 'o': options->cnfFileName = util_strsav(util_optarg); break; case 'I' : options->incremental = atoi(util_optarg); break; case 'E': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->encoding = atoi(util_optarg); if((options->encoding < 0) || (options->encoding > 2)){ goto usage; } break; case 'S': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->satSolver = atoi(util_optarg); if((options->satSolver < 0) || (options->satSolver > 1)){ goto usage; } break; case 'C': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } options->clauses = atoi(util_optarg); if((options->clauses < 0) || (options->clauses > 2)){ goto usage; } break; default: goto usage; } } if (options->minK > options->maxK){ (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n"); goto usage; } /* * Open the ltl file. */ if (argc - util_optind == 0) { (void) fprintf(vis_stderr, "** bmc error: file containing ltl formulae not provided\n"); goto usage; } else if (argc - util_optind > 1) { (void) fprintf(vis_stderr, "** bmc error: too many arguments\n"); goto usage; } ltlFileName = util_strsav(argv[util_optind]); /* Read LTL Formulae */ if (!ltlFileName) goto usage; options->ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0); if (options->ltlFile == NIL(FILE)) { (void) fprintf(vis_stdout,"** bmc error: Cannot open the file %s\n", ltlFileName); FREE(ltlFileName); BmcOptionFree(options); return NIL(BmcOption_t); } FREE(ltlFileName); /* create SAT Solver input file */ if (options->cnfFileName == NIL(char)) { options->satInFile = BmcCreateTmpFile(); if (options->satInFile == NIL(char)){ BmcOptionFree(options); return NIL(BmcOption_t); } } else { options->satInFile = options->cnfFileName; } /* create SAT Solver output file */ options->satOutFile = BmcCreateTmpFile(); if (options->satOutFile == NIL(char)){ BmcOptionFree(options); return NIL(BmcOption_t); } return options; usage: (void) fprintf(vis_stderr, "usage: bmc [-h][-m minimum_length][-k maximum_length][-s step][-r inductive_step][-e][-F ][-d debug_level][-E ][-C ][-S ][-O ][-I ][-v verbosity_level][-t period][-o ] \n"); (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); (void) fprintf(vis_stderr, " -m \tminimum length of counterexample to be checked (default is 0)\n"); (void) fprintf(vis_stderr, " -k \tmaximum length of counterexample to be checked (default is 1)\n"); (void) fprintf(vis_stderr, " -s \tincrementing value of counterexample length (default is 1)\n"); (void) fprintf(vis_stderr, " -r \tUse check for termination at each inductive_step to check if the property passes (default is 0).\n"); (void) fprintf(vis_stderr, " -e \tUse early termination to check if the property passes. Valid only with -r \n"); (void) fprintf(vis_stderr, " -F \n"); (void) fprintf(vis_stderr, " -d \n"); (void) fprintf(vis_stderr, " debug_level = 0 => No debugging performed (Default)\n"); (void) fprintf(vis_stderr, " debug_level = 1 => Debugging with minimal output: generate counter-example if the LTL formula fails.\n"); (void) fprintf(vis_stderr, " debug_level = 2 => Debugging with full output in Aiger format: generate counter-example if the LTL formula fails.\n"); (void) fprintf(vis_stderr, " -O \n"); (void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n"); (void) fprintf(vis_stderr, " -v \n"); (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n"); (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n"); (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n"); (void) fprintf(vis_stderr, " -t time out period\n"); (void) fprintf(vis_stderr, " -E \n"); (void) fprintf(vis_stderr, " encoding = 0 => Original BMC encoding (Default)\n"); (void) fprintf(vis_stderr, " encoding = 1 => SNF encoding\n"); (void) fprintf(vis_stderr, " encoding = 2 => Fixpoint encoding\n"); /* (void) fprintf(vis_stderr, " encoding = 3 => FNF encoding\n"); */ (void) fprintf(vis_stderr, " -S \n"); (void) fprintf(vis_stderr, " sat_solver = 0 => CirCUs (Default)\n"); (void) fprintf(vis_stderr, " sat_solver = 1 => cusp\n"); (void) fprintf(vis_stderr, " -C \n"); (void) fprintf(vis_stderr, " clauses = 0 => Apply CirCUs on circuit (Default)\n"); (void) fprintf(vis_stderr, " clauses = 1 => Apply SAT solver on CNF (new)\n"); (void) fprintf(vis_stderr, " clauses = 2 => Apply SAT solver on CNF (old)\n"); (void) fprintf(vis_stderr, " -I \n"); (void) fprintf(vis_stderr, " level = 1 => Trace Objective\n"); (void) fprintf(vis_stderr, " level = 2 => Distill\n"); (void) fprintf(vis_stderr, " level = 3 => Trace Objective + Distill\n"); (void) fprintf(vis_stderr, " -o contains CNF of the counterexample\n"); (void) fprintf(vis_stderr, " The input file containing LTL formulae to be checked.\n"); BmcOptionFree(options); return NIL(BmcOption_t); } /**Function******************************************************************** Synopsis [Alloc Memory for BmcOption_t.] SideEffects [] SeeAlso [] ******************************************************************************/ BmcOption_t * BmcOptionAlloc(void) { BmcOption_t *result = ALLOC(BmcOption_t, 1); if (!result){ return result; } result->ltlFile = NIL(FILE); result->fairFile = NIL(FILE); result->cnfFileName = NIL(char); result->minK = 0; result->maxK = 1; result->step = 1; result->timeOutPeriod = 0; result->startTime = 0; result->verbosityLevel = BmcVerbosityNone_c; result->dbgLevel = 0; result->inductiveStep = 0; result->printInputs = FALSE; result->satSolverError = FALSE; result->satInFile = NIL(char); result->satOutFile = NIL(char); result->incremental = 0; result->earlyTermination = 0; result->satSolver = CirCUs; /* default is 0 */ result->clauses = 0; /* default is 0 */ result->encoding = 0; /* default is 0 */ return result; } /**Function******************************************************************** Synopsis [Free BmcOption_t, and close files.] SideEffects [] SeeAlso [] ******************************************************************************/ void BmcOptionFree( BmcOption_t *result) { if (result->ltlFile != NIL(FILE)){ fclose(result->ltlFile); } if (result->cnfFileName != NIL(char)){ FREE(result->cnfFileName); } else if (result->satInFile != NIL(char)) { unlink(result->satInFile); FREE(result->satInFile); } if (result->fairFile != NIL(FILE)){ fclose(result->fairFile); } if (result->satOutFile != NIL(char)) { unlink(result->satOutFile); FREE(result->satOutFile); } FREE(result); } /**Function******************************************************************** Synopsis [Create a temporary file] Description [] SideEffects [] ******************************************************************************/ char * BmcCreateTmpFile(void) { #if HAVE_MKSTEMP && HAVE_CLOSE char cnfFileName[] = "/tmp/vis.XXXXXX"; int fd; #else char *cnfFileName; char buffer[512]; #endif #if HAVE_MKSTEMP && HAVE_CLOSE fd = mkstemp(cnfFileName); if (fd == -1){ #else cnfFileName = util_strsav(tmpnam(buffer)); if (cnfFileName == NIL(char)){ #endif (void)fprintf(vis_stderr,"** bmc error: Can not create temporary file. "); (void)fprintf(vis_stderr,"Clean up /tmp and try again.\n"); return NIL(char); } #if HAVE_MKSTEMP && HAVE_CLOSE close(fd); #endif return util_strsav(cnfFileName); } /* createTmpFile() */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Implements the bounded_model_check command] CommandName [bounded_model_check] CommandSynopsis [Performs a SAT-based LTL model checking on a flattened network] CommandArguments [\[-h\] \[-v <verbosity_level>\] \[-m <minimum_length>\] \[-k <maximum_length>\] \[-s <step_value>\] \[-r <termination_check_step>\] \[-e\] \[-F <fairness_file>\] \[-S <sat_solver>\] \[-E <encoding>\] \[-C <clause_type>\] \[-I <inc_level>\] \[-d <dbg_level>\] \[-t <timeOutPeriod>\] \[-o <cnf_file>\] \[-i\] \[-O <debug_file>\] <ltl_file> ] CommandDescription [Performs a SAT-based LTL bounded model checking (BMC) on a flattened network. This command looks for a counterexample of length k ( minimum_length ≤ k ≤ maximum_length). If -r is specified, this command performs check for termination after each termination_check_step . If no counterexample is found, this command increases k by step_value (specifies by the -s option) until a counterexample is found, the search becomes intractable (timed out), or k reaches a bound (determine by the check for termination), and then we conclude that the LTL property passes. This command implements the basic encoding of Bounded Model Checking (BMC) as descibed in the paper "Symbolic Model Checking without BDDs". However, the -E option can be used to select other encoding scheme. We also applied some of the improvements in the BMC encoding described in the paper "Improving the Encoding of LTL Model Checking into SAT". To prove that an LTL property passes, we implement the termination methods that are descirebed in the papers "Checking Safety Properties Using Induction and a SAT-Solver" and "Proving More Properties with Bounded Model Checking". Before calling this command, the user should have initialized the design by calling the command flatten_hierarchy. If the user uses the -r option and the LTL property is a general LTL property, the command build_partition_maigs must be called. The aig graph must be built by calling the command build_partition_mdds

Command options:

-h
Print the command usage.

-m <minimum_length>
Minimum length of counterexample to be checked (default is 0).
-k <maximum_length>
Maximum length of counterexample to be checked (default is 1).
-s <step_value>
Incrementing value of counterexample length (default is 1).
-r <termination_check_step>
Check for termination for each termination_check_step (default is 0). 0 means don't check for termination.
-e
Activate early termination check. Check if there is no simple path starts from an initial state. Valid only for general LTL and safety properties. Must be used with -r option.
-S <sat_solver>
Specify SAT solver
sat_solver must be one of the following:

0: CirCUs (Default)

1: zChaff

-E <encoding>
Specify encoding scheme
encoding must be one of the following:

0: The original BMC encoding (Default)

1: SNF encoding

2: Fixpoint encoding

-C <clause_type>
Specify clause type
encoding must be one of the following:

0: Apply CirCUs SAT solver on circuit (Default)

1: Apply SAT solver on CNF generated form circuit

2: Apply SAT solver on CNF

-I <inc_level>
Specify increment sat solver type
encoding must be one of the following:

1: Trace Objective (Default)

2: Distill

3: Trace Objective + Distill

-F <fairness_file>
Read fairness constraints from <fairness_file>. Each formula in the file is a condition that must hold infinitely often on a fair path.
-o <cnf_file> Save CNF formula in <cnf_file>
-O <debug_file> Save counterexample to <debug_file>
-t <timeOutPeriod>
Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-v <verbosity_level>
Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_level must be one of the following:

0: No feedback provided. This is the default.

1: Feedback on code location.

2: Feedback on code location and CPU usage.

-d <dbg_level>
Specify the amount of debugging performed when the BMC models check the LTL formula.

dbg_level must be one of the following:

0: No debugging performed. dbg_level=0 is the default.

1: Debugging with minimal output: generate counter-example if the LTL formula fails and the counterexample length.

-i
Print input values causing transitions between states during debugging.

<ltl_file>
File containing LTL formulae to be checked.
] SideEffects [] SeeAlso [Ntk_NetworkAddApplInfo] ******************************************************************************/ static int CommandBmc( Hrc_Manager_t ** hmgr, int argc, char ** argv) { Ntk_Network_t *network; BmcOption_t *options; int i; array_t *formulaArray; array_t *LTLformulaArray; bAig_Manager_t *manager; array_t *constraintArray = NIL(array_t); /* * Parse command line options. */ if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { return 1; } /* * Read the network */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** bmc error: No network\n"); BmcOptionFree(options); return 1; } manager = Ntk_NetworkReadMAigManager(network); if (manager == NIL(mAig_Manager_t)) { (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n"); BmcOptionFree(options); return 1; } /* We need the bdd when building the transition relation of the automaton */ if(options->inductiveStep !=0){ Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t); designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr); if (designFsm == NIL(Fsm_Fsm_t)) { return 1; } } /* time out */ if (options->timeOutPeriod > 0) { /* Set the static variables used by the signal handler. */ bmcTimeOut = options->timeOutPeriod; alarmLapTime = options->startTime = util_cpu_ctime(); (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(options->timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stdout, "\n# BMC: timeout occurred after %d seconds.\n", options->timeOutPeriod); (void) fprintf(vis_stdout, "# BMC: data may be corrupted.\n"); BmcOptionFree(options); alarm(0); return 1; } } formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); if (formulaArray == NIL(array_t)) { (void) fprintf(vis_stderr, "** bmc error: error in parsing CTL* Fromula from file\n"); BmcOptionFree(options); return 1; } if (array_n(formulaArray) == 0) { (void) fprintf(vis_stderr, "** bmc error: No formula in file\n"); BmcOptionFree(options); Ctlsp_FormulaArrayFree(formulaArray); return 1; } LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); Ctlsp_FormulaArrayFree(formulaArray); if (LTLformulaArray == NIL(array_t)){ (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n"); BmcOptionFree(options); return 1; } if (options->fairFile != NIL(FILE)) { constraintArray = BmcReadFairnessConstraints(options->fairFile); if(constraintArray == NIL(array_t)){ Ctlsp_FormulaArrayFree(LTLformulaArray); BmcOptionFree(options); return 1; } if(!Ctlsp_LtlFormulaArrayIsPropositional(constraintArray)){ Ctlsp_FormulaArrayAddLtlFairnessConstraints(LTLformulaArray, constraintArray); Ctlsp_FormulaArrayFree(constraintArray); constraintArray = NIL(array_t); } } /* Call a proper BMC function based on LTL formula. */ for (i = 0; i < array_n(LTLformulaArray); i++) { Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, i); DispatchBmcCommand(network, ltlFormula, constraintArray, options); } /* Free used memeory */ if (constraintArray != NIL(array_t)){ Ctlsp_FormulaArrayFree(constraintArray); } Ctlsp_FormulaArrayFree(LTLformulaArray); BmcOptionFree(options); fflush(vis_stdout); fflush(vis_stderr); alarm(0); return 0; }/* CommandBmc() */ /**Function******************************************************************** Synopsis [Handle function for timeout.] Description [This function is called when the time out occurs. Since alarm is set with an elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire again later.] SideEffects [] ******************************************************************************/ static void TimeOutHandle(void) { int seconds = (int) ((util_cpu_ctime() - alarmLapTime) / 1000); if (seconds < bmcTimeOut) { unsigned slack = (unsigned) (bmcTimeOut - seconds); (void) signal(SIGALRM, (void(*)(int)) TimeOutHandle); (void) alarm(slack); } else { longjmp(timeOutEnv, 1); } } /* TimeOutHandle */ /**Function******************************************************************** Synopsis [Dispatch BMC] Description [Call a proper BMC routine. The -E for BMC encoding scheme -C clause generation -S SAT solver 0 CirCUs 1 zChaff ] SideEffects [] ******************************************************************************/ static void DispatchBmcCommand( Ntk_Network_t *network, Ctlsp_Formula_t *ltlFormula, array_t *constraintArray, BmcOption_t *options) { Ctlsp_Formula_t *negLtlFormula = Ctlsp_LtllFormulaNegate(ltlFormula); st_table *CoiTable = st_init_table(st_ptrcmp, st_ptrhash); assert(ltlFormula != NIL(Ctlsp_Formula_t)); assert(network != NIL(Ntk_Network_t)); /* print out the given LTL formula */ fprintf(vis_stdout, "Formula: "); Ctlsp_FormulaPrint(vis_stdout, ltlFormula); fprintf(vis_stdout, "\n"); if (options->verbosityLevel >= BmcVerbosityMax_c){ fprintf(vis_stdout, "Negated formula: "); Ctlsp_FormulaPrint(vis_stdout, negLtlFormula); fprintf(vis_stdout, "\n"); } /* Compute the cone of influence of the LTL formula */ BmcGetCoiForLtlFormula(network, negLtlFormula, CoiTable); if(options->clauses == 2){ /* Generate clauses for each time frame. This is the old way of generating clauses in BMC. */ if (constraintArray != NIL(array_t)){ BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options); } else /* If the LTL formula is propositional. */ if(Ctlsp_isPropositionalFormula(negLtlFormula)){ BmcLtlVerifyProp(network, negLtlFormula, CoiTable, options); } else /* If the LTL formula is of type G(p) (its negation is of type F(q)), where p and q are propositional. */ if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){ BmcLtlVerifyGp(network, negLtlFormula, CoiTable, options); } else /* If the LTL formula is of type F(p) (its negation is of type G(q)), where p and q are propositional. */ if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){ BmcLtlVerifyFp(network, negLtlFormula, CoiTable, options); } else /* If the depth of the LTL formula (the maximum level of nesting temporal operators) = 1 */ /* if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){ BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options); } else */ /* If the LTL formula is of type FG(p) (its negation is of type GF(q)), where p and q are propositional. */ if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){ BmcLtlVerifyFGp(network, negLtlFormula, CoiTable, options); } else /* All other LTL formulae */ BmcLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, NIL(array_t), options); } else { /* Build AIG for each time frame. */ if (constraintArray != NIL(array_t)){ if(options->encoding == 0){ BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options, 0); } else if(options->encoding == 1){ BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, constraintArray, options, 1); } else if(options->encoding == 2){ BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula, CoiTable, constraintArray, options); } } else /* If the LTL formula is propositional. */ if(Ctlsp_isPropositionalFormula(negLtlFormula)){ BmcCirCUsLtlVerifyProp(network, negLtlFormula, CoiTable, options); } else /* If the LTL formula is of type G(p) (its negation is of type F(q)), where p and q are propositional. */ if(Ctlsp_LtlFormulaIsFp(negLtlFormula)){ BmcCirCUsLtlVerifyGp(network, negLtlFormula, CoiTable, options); } else /* If the LTL formula is of type F(p) (its negation is of type G(q)), where p and q are propositional. */ if (Ctlsp_LtlFormulaIsGp(negLtlFormula)){ BmcCirCUsLtlVerifyFp(network, negLtlFormula, CoiTable, options); } else /* If the depth of the LTL formula (the maximum level of nesting temporal operators) = 1 if (Ctlsp_LtlFormulaDepth(negLtlFormula) == 1){ BmcLtlVerifyUnitDepth(network, negLtlFormula, CoiTable, options); } else If the LTL formula is of type FG(p) (its negation is of type GF(q)), where p and q are propositional. */ if(Ctlsp_LtlFormulaIsGFp(negLtlFormula)){ BmcCirCUsLtlVerifyFGp(network, negLtlFormula, CoiTable, options); } else if(Ctlsp_LtlFormulaTestIsSyntacticallyCoSafe(negLtlFormula) || (Ltl_AutomatonGetStrength(BmcAutLtlToAutomaton(network,ltlFormula)) == 0)) { BmcCirCUsLtlCheckSafety(network, negLtlFormula, options, CoiTable); } else { /* All other LTL formulae */ if(options->encoding == 0){ BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, NIL(array_t), options, 0); } else if(options->encoding == 1){ BmcCirCUsLtlVerifyGeneralLtl(network, negLtlFormula, CoiTable, NIL(array_t), options, 1); } else if(options->encoding == 2){ BmcCirCUsLtlVerifyGeneralLtlFixPoint(network, negLtlFormula, CoiTable, NIL(array_t), options); } } } st_free_table(CoiTable); Ctlsp_FormulaFree(negLtlFormula); } /* DispatchBmcCommand() */ /**Function******************************************************************** Synopsis [cnf_sat] Description [] CommandName [cnf_sat] CommandSynopsis [Perform SAT solving with CNF input] CommandArguments [\[-h\] \[-a <assgined_filename>\] \[-f <output_filename>\] \[-t <timeout>\] \[-v <verbose>\] \[-b\] <cnf_filename> ] CommandDescription [Perform SAT solving with CirCUs after reading CNF file

-b
If the given CNF has small number of variables and clause then the BDD is built from the CNF clauses. If the monolithic BDD is built then we can conclude SAT or UNSAT, otherwise the normal SAT algorithm is invoked.

-t <timeOutPeriod>
Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-f <output_filename>
Specify the output filename to save the satisfying assignments and the statistics of SAT solving.

] SideEffects [] SeeAlso [] ******************************************************************************/ static int CommandCnfSat( Hrc_Manager_t ** hmgr, int argc, char ** argv) { satOption_t *option; char *filename, c; char *forcedAssignFilename; int timeOutPeriod, i; option = sat_InitOption(); timeOutPeriod = -1; forcedAssignFilename = 0; util_getopt_reset(); while ((c = util_getopt(argc, argv, "a:bf:ht:v:c:")) != EOF) { switch(c) { case 'h': goto usage; case 'b' : option->BDDMonolithic = 1; break; case 'f' : option->outFilename = strdup(util_optarg); break; case 'a' : forcedAssignFilename = strdup(util_optarg); break; case 't' : timeOutPeriod = atoi(util_optarg); break; case 'v': for (i = 0; i < (int)(strlen(util_optarg)); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } option->verbose = (Bmc_VerbosityLevel) atoi(util_optarg); break; //Bing: for unsat core case 'c': option->coreGeneration = 1; option->unsatCoreFileName = strdup(util_optarg); option->minimizeConflictClause = 0; option->clauseDeletionHeuristic = 0; break; default: goto usage; } } if (argc - util_optind == 0) { (void) fprintf(vis_stderr, "** ERROR : file containing cnf file not provided\n"); goto usage; } else if (argc - util_optind > 1) { (void) fprintf(vis_stderr, "** ERROR : too many arguments\n"); goto usage; } filename = util_strsav(argv[util_optind]); if(forcedAssignFilename) option->forcedAssignArr = sat_ReadForcedAssignment(forcedAssignFilename); if (timeOutPeriod > 0) { bmcTimeOut = timeOutPeriod; alarmLapTime = util_cpu_ctime(); (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stderr, "** ERROR : timeout occurred after %d seconds.\n", timeOutPeriod); alarm(0); return 1; } } sat_CNFMain(option, filename); return 0; usage: (void) fprintf(vis_stderr, "usage: cnf_sat [-h] [-v verboseLevel] [-t timeout] \n"); (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); (void) fprintf(vis_stderr, " -a \tto make forced assignment\n"); (void) fprintf(vis_stderr, " -f \twrite log to the file\n"); (void) fprintf(vis_stderr, " -b \tuse BDD based method\n"); (void) fprintf(vis_stderr, " -v \n"); (void) fprintf(vis_stderr, " -t time out period\n"); (void) fprintf(vis_stderr, " -c UNSAT core generation\n"); (void) fprintf(vis_stderr, " CNF file to be checked.\n"); return 1; } #if 0 /**Function******************************************************************** Synopsis [Implements the bdd_sat command.] Description [This command integrates BDD-based methods with SAT-based method to model safety property of the form AG(p). Where p is either a propositional formula or a path formula consists of only the temporal operator X.] CommandName [bdd_sat_bounded_model_check] CommandSynopsis [performs an LTL bounded model checking on a flattened network] CommandArguments [\[-h\] \[-v <verbosity_level>\] \[-d <dbg_level>\] \[-i\] -m <minimum_length> -k <maximum_length> -s <step_value> -o <cnf_file> <ltl_file> ] -F <fairness_file> -o <cnf_file> <ltl_file> ] CommandDescription [Performs an LTL bounded model checking on a flattened network. This command looks for a counterexample of length ≥ minimum_length and ≤ maximum_length. It increments the length by step_value. Before calling this command, the user should have initialized the design by calling the command flatten_hierarchy, and then calling the command build_partition_maigs.

The value of maximum length must be >= minimum length.

Command options:

-h
Print the command usage.

-m <minimum_length>
Minimum length of counterexample to be checked (default is 0).
-k <maximum_length>
Maximum length of counterexample to be checked (default is 1).
-s <step_value>
Incrementing value of counterexample length (default is 1).
-r <inductive_Step>
Use inductive proof at each step_value to check if the property passes (default is 0). 0 means don't use the inductive proof. BMC will check using the indcution if the property passes if the current length of the counterexample is a multiple of inductive_Step.
-F <fairness_file>
Read fairness constraints from <fairness_file>. Each formula in the file is a condition that must hold infinitely often on a fair path.
-o <cnf_file> Save the CNF formula in <cnf_file>
-t <timeOutPeriod>
Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-v <verbosity_level>
Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_level must be one of the following:

0: No feedback provided. This is the default.

1: Feedback on code location.

2: Feedback on code location and CPU usage.

-d <dbg_level>
Specify the amount of debugging performed when the BMC models check the LTL formula.

dbg_level must be one of the following:

0: No debugging performed. dbg_level=0 is the default.

1: Debugging with minimal output: generate counter-example if the LTL formula fails and the counterexample length.

-h
Print the command usage.

-i
Print input values causing transitions between states during debugging.

-o <cnf_file>;
File containing CNF of the counterexample if exist. If specifies, the user can exam this file looking for information about the generated path. This file will be the input to the SAT solver. The contents of this file is in dimacs format.
<ltl_file>
File containing LTL formulas to be model checked.
] SideEffects [] SeeAlso [Ntk_NetworkAddApplInfo] ******************************************************************************/ int CommandBddSat( Hrc_Manager_t ** hmgr, int argc, char ** argv) { Ntk_Network_t *network; BmcOption_t *options; array_t *formulaArray; bAig_Manager_t *mAigManager; Fsm_Fsm_t *fsm; mdd_manager *mddManager; int startTime; /* * Parse command line options. */ if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) { return 1; } /* Read the network */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** bdd_sat error: No network\n"); BmcOptionFree(options); return 1; } /* read fsm */ fsm = Fsm_NetworkReadOrCreateFsm(network); if (fsm == NIL(Fsm_Fsm_t)) { (void) fprintf(vis_stdout, "** bdd_sat error: Can't read or create fsm\n"); BmcOptionFree(options); return 1; } mddManager = Fsm_FsmReadMddManager(fsm); /* mdd manager */ mAigManager = Ntk_NetworkReadMAigManager(network); if (mAigManager == NIL(mAig_Manager_t)) { (void) fprintf(vis_stdout, "** bdd_sat error: run build_partition_maigs command first\n"); BmcOptionFree(options); return 1; } formulaArray = Ctlsp_FileParseFormulaArray(options->ltlFile); if (formulaArray == NIL(array_t)) { (void) fprintf(vis_stderr, "** bdd_sat error: Error in parsing CTL* Fromula from file\n"); BmcOptionFree(options); return 1; } if (array_n(formulaArray) == 0) { (void) fprintf(vis_stderr, "** bdd_sat error: No formula in file\n"); BmcOptionFree(options); array_free(formulaArray); return 1; } /* time out */ if (options->timeOutPeriod > 0) { /* Set the static variables used by the signal handler. */ bmcTimeOut = options->timeOutPeriod; alarmLapTime = options->startTime = util_cpu_ctime(); (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(options->timeOutPeriod); if (setjmp(timeOutEnv) > 0) { (void) fprintf(vis_stdout, "\n# bdd_sat: timeout occurred after %d seconds.\n", options->timeOutPeriod); (void) fprintf(vis_stdout, "# bdd_sat: data may be corrupted.\n"); BmcOptionFree(options); alarm(0); return 1; } } /* bdd and sat to model check the LTL property.*/ BmcBddSat(network, formulaArray, options); Ctlsp_FormulaArrayFree(formulaArray); fflush(vis_stdout); fflush(vis_stderr); BmcOptionFree(options); alarm(0); return 0; /* normal exit */ }/* CommandBddSat() */ #endif int CommandWriteCnf(Hrc_Manager_t ** hmgr, int argc, char ** argv) { Ntk_Network_t *network; bAig_Manager_t *manager; array_t *formulaArray; array_t *LTLformulaArray; char * outFileName = NIL(char); char * ltlFileName = NIL(char); FILE * ltlFile; FILE * outFile; int c,i; int maxK = 0; st_table *allLatches; BmcCnfClauses_t *cnfClauses = NIL(BmcCnfClauses_t); outFile = vis_stdout ; // Parse option util_getopt_reset(); while ((c = util_getopt(argc, argv, "f:o:k:h")) != EOF) { switch(c) { case 'h': goto usage; case 'o' : outFileName = strdup(util_optarg); outFile = Cmd_FileOpen(outFileName, "w", NIL(char *), 0); break; case 'f' : ltlFileName = strdup(util_optarg); break; case 'k': for (i = 0; i < strlen(util_optarg); i++) { if (!isdigit((int)util_optarg[i])) { goto usage; } } maxK = atoi(util_optarg); break; break; default: goto usage; } } network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { (void) fprintf(vis_stdout, "** bmc error: No network\n"); return 1; } manager = Ntk_NetworkReadMAigManager(network); if (manager == NIL(mAig_Manager_t)) { (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n"); return 1; } // Create a clause database cnfClauses = BmcCnfClausesAlloc(); // Gnerate clauses for an initialized path of length k // nodeToMvfAigTable Maps each node to its Multi-function And/Inv graph st_table* nodeToMvfAigTable = (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY); assert(nodeToMvfAigTable != NIL(st_table)); allLatches = st_init_table(st_ptrcmp, st_ptrhash); // Get all the latches of the network lsGen gen ; Ntk_Node_t *node; Ntk_NetworkForEachNode(network,gen, node){ if (Ntk_NodeTestIsLatch(node)){ st_insert(allLatches, (char *) node, (char *) 0); } } BmcCnfGenerateClausesForPath(network, 0, maxK, BMC_INITIAL_STATES, cnfClauses, nodeToMvfAigTable, allLatches); // If ltl file exists if(ltlFileName != NIL(char)) { ltlFile = Cmd_FileOpen(ltlFileName, "r", NIL(char *), 0); formulaArray = Ctlsp_FileParseFormulaArray(ltlFile); if (formulaArray == NIL(array_t)) { (void) fprintf(vis_stderr, "** bmc error: error in parsing ltl Fromula from file\n"); return 1; } LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray); for (i = 0; i < array_n(LTLformulaArray); i++) { Ctlsp_Formula_t *ltlFormula = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, i); BmcGenerateCnfForLtl(network, ltlFormula, 0, maxK, 0, cnfClauses); } } // Write Clauses st_generator *stGen; char *name; int cnfIndex,k; st_foreach_item_int(cnfClauses->cnfIndexTable, stGen, &name, &cnfIndex) { fprintf(outFile, "c %s %d\n",name, cnfIndex); } (void) fprintf(outFile, "p cnf %d %d\n", cnfClauses->cnfGlobalIndex-1, cnfClauses->noOfClauses); if (cnfClauses->clauseArray != NIL(array_t)) { for (i = 0; i < cnfClauses->nextIndex; i++) { k = array_fetch(int, cnfClauses->clauseArray, i); (void) fprintf(outFile, "%d%c", k, (k == 0) ? '\n' : ' '); } } if(outFileName != NIL(char)) fclose(outFile); return 1; usage: (void) fprintf(vis_stderr, "usage: write_cnf [-h] [-f ltl file] [-o outfile] [k]\n"); (void) fprintf(vis_stderr, " -h \tprint the command usage\n"); (void) fprintf(vis_stderr, " -f \tto add a ltlfile\n"); (void) fprintf(vis_stderr, " -o \twrite output in outputfile\n"); (void) fprintf(vis_stderr, " -k \tnumber of unroll steps\n"); return 1; }