From 77f64a7ef23314b3a2988d5c215e96fe3d1f26dc Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 18 Feb 2025 09:52:44 +0000 Subject: [PATCH] ebmc: --ignore-initial This adds the --igore-initial command line option to ebmc, which allows reasoning about the transition relation only of a Verilog file. --- .../verilog/initial/ignore-initial1.desc | 9 +++++++++ regression/verilog/initial/ignore-initial1.sv | 16 ++++++++++++++++ .../test.desc => initial/initial1.desc} | 2 +- .../{initial1/main.v => initial/initial1.v} | 0 src/ebmc/ebmc_parse_options.cpp | 10 +++++++--- src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/transition_system.cpp | 4 ++++ src/verilog/verilog_language.cpp | 9 ++++++++- src/verilog/verilog_language.h | 1 + src/verilog/verilog_synthesis.cpp | 18 ++++++++++++------ src/verilog/verilog_synthesis.h | 4 ++-- src/verilog/verilog_synthesis_class.h | 6 +++--- 12 files changed, 64 insertions(+), 17 deletions(-) create mode 100644 regression/verilog/initial/ignore-initial1.desc create mode 100644 regression/verilog/initial/ignore-initial1.sv rename regression/verilog/{initial1/test.desc => initial/initial1.desc} (86%) rename regression/verilog/{initial1/main.v => initial/initial1.v} (100%) diff --git a/regression/verilog/initial/ignore-initial1.desc b/regression/verilog/initial/ignore-initial1.desc new file mode 100644 index 000000000..3c6a70dae --- /dev/null +++ b/regression/verilog/initial/ignore-initial1.desc @@ -0,0 +1,9 @@ +CORE +ignore-initial1.sv +--top main --bound 1 --ignore-initial +^\[main\.p1\] always main\.x == 20 || main\.x == 5: REFUTED$ +^\[main\.p2\] always main\.y == 30 || main\.y == 6: REFUTED$ +^EXIT=10$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/initial/ignore-initial1.sv b/regression/verilog/initial/ignore-initial1.sv new file mode 100644 index 000000000..c5c6ee7f4 --- /dev/null +++ b/regression/verilog/initial/ignore-initial1.sv @@ -0,0 +1,16 @@ +module main(input clk); + + reg [7:0] x, y = 30; + + initial x=20; + + always_ff @(posedge clk) x=5; + always_ff @(posedge clk) y=6; + + // fails, owing to nondeterministic initial state + p1: assert property (x==20 || x==5); + + // fails, owing to nondeterministic initial state + p2: assert property (y==30 || y==6); + +endmodule diff --git a/regression/verilog/initial1/test.desc b/regression/verilog/initial/initial1.desc similarity index 86% rename from regression/verilog/initial1/test.desc rename to regression/verilog/initial/initial1.desc index cfd3731f6..f6ffcc859 100644 --- a/regression/verilog/initial1/test.desc +++ b/regression/verilog/initial/initial1.desc @@ -1,5 +1,5 @@ CORE -main.v +initial1.v --module main --bound 2 ^EXIT=0$ ^SIGNAL=0$ diff --git a/regression/verilog/initial1/main.v b/regression/verilog/initial/initial1.v similarity index 100% rename from regression/verilog/initial1/main.v rename to regression/verilog/initial/initial1.v diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index f561bca9a..5e01e3ca9 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -356,9 +356,6 @@ void ebmc_parse_optionst::help() " {y--numbered-trace} \t give a trace with identifiers numbered by timeframe\n" " {y--show-properties} \t list the properties in the model\n" " {y--property} {uid} \t check the property with given ID\n" - " {y-I} {upath} \t set include path\n" - " {y--systemverilog} \t force SystemVerilog instead of Verilog\n" - " {y--reset} {uexpr} \t set up module reset\n" " {y--liveness-to-safety} \t translate liveness properties to safety properties\n" "\n" "Methods:\n" @@ -398,6 +395,13 @@ void ebmc_parse_optionst::help() " {y--yices} \t use Yices as solver\n" " {y--z3} \t use Z3 as solver\n" "\n" + "Verilog options:\n" + " {y-I} {upath} \t set include path\n" + " {y-D} {uvar}[={uvalue}] \t set preprocessor define\n" + " {y--systemverilog} \t force SystemVerilog instead of Verilog\n" + " {y--reset} {uexpr} \t set up module reset\n" + " {y--ignore-initial} \t disregard initial blocks\n" + "\n" "Debugging options:\n" " {y--preprocess} \t output the preprocessed source file\n" " {y--show-parse} \t show parse trees\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index d6abed1e8..03bb8772b 100644 --- a/src/ebmc/ebmc_parse_options.h +++ b/src/ebmc/ebmc_parse_options.h @@ -35,7 +35,7 @@ class ebmc_parse_optionst:public parse_options_baset "(outfile):(xml-ui)(verbosity):(gui)" "(json-modules):(json-properties):(json-result):" "(neural-liveness)(neural-engine):" - "(reset):" + "(reset):(ignore-initial)" "(version)(verilog-rtl)(verilog-netlist)" "(compute-interpolant)(interpolation)(interpolation-vmcai)" "(ic3)(property):(constr)(h)(new-mode)(aiger)" diff --git a/src/ebmc/transition_system.cpp b/src/ebmc/transition_system.cpp index e6fc9d95c..71ea73b0e 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -174,6 +174,10 @@ static bool parse( if(cmdline.isset('D')) options.set_option("defines", cmdline.get_values('D')); + // do --ignore-initial + if(cmdline.isset("ignore-initial")) + options.set_option("ignore-initial", true); + language.set_language_options(options, message_handler); message.status() << "Parsing " << filename << messaget::eom; diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index cde151f21..6cd3bb386 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -39,6 +39,7 @@ void verilog_languaget::set_language_options( include_paths = options.get_list_option("I"); initial_defines = options.get_list_option("defines"); warn_implicit_nets = options.get_bool_option("warn-implicit-nets"); + ignore_initial = options.get_bool_option("ignore-initial"); } /*******************************************************************\ @@ -191,8 +192,14 @@ bool verilog_languaget::typecheck( message.debug() << "Synthesis " << module << messaget::eom; if(verilog_synthesis( - symbol_table, module, parse_tree.standard, message_handler, optionst{})) + symbol_table, + module, + parse_tree.standard, + ignore_initial, + message_handler)) + { return true; + } return false; } diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index a590d498c..475d6ecba 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -94,6 +94,7 @@ class verilog_languaget:public languaget bool force_systemverilog = false; bool vl2smv_extensions = false; bool warn_implicit_nets = false; + bool ignore_initial = false; std::list include_paths; std::list initial_defines; verilog_parse_treet parse_tree; diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index ee12837dc..fb471e806 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -1459,7 +1459,11 @@ void verilog_synthesist::synth_module_instance( // make sure the module is synthesized already verilog_synthesis( - symbol_table, module_identifier, standard, get_message_handler(), options); + symbol_table, + module_identifier, + standard, + ignore_initial, + get_message_handler()); for(auto &instance : statement.instances()) expand_module_instance(module_symbol, instance, trans); @@ -1782,6 +1786,9 @@ void verilog_synthesist::synth_initial( << "initial module item expected to have one operand"; } + if(ignore_initial) + return; + construct=constructt::INITIAL; event_guard=event_guardt::NONE; @@ -3716,12 +3723,12 @@ bool verilog_synthesis( symbol_table_baset &symbol_table, const irep_idt &module, verilog_standardt standard, - message_handlert &message_handler, - const optionst &options) + bool ignore_initial, + message_handlert &message_handler) { const namespacet ns(symbol_table); verilog_synthesist verilog_synthesis( - standard, ns, symbol_table, module, options, message_handler); + standard, ignore_initial, ns, symbol_table, module, message_handler); return verilog_synthesis.typecheck_main(); } @@ -3744,14 +3751,13 @@ bool verilog_synthesis( message_handlert &message_handler, const namespacet &ns) { - optionst options; symbol_tablet symbol_table; const auto errors_before = message_handler.get_message_count(messaget::M_ERROR); verilog_synthesist verilog_synthesis( - standard, ns, symbol_table, module_identifier, options, message_handler); + standard, false, ns, symbol_table, module_identifier, message_handler); try { diff --git a/src/verilog/verilog_synthesis.h b/src/verilog/verilog_synthesis.h index f5730e905..58b48403e 100644 --- a/src/verilog/verilog_synthesis.h +++ b/src/verilog/verilog_synthesis.h @@ -19,8 +19,8 @@ bool verilog_synthesis( symbol_table_baset &, const irep_idt &module, verilog_standardt, - message_handlert &, - const optionst &); + bool ignore_initial, + message_handlert &); bool verilog_synthesis( exprt &, diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h index 8d53fab07..4c8723c6b 100644 --- a/src/verilog/verilog_synthesis_class.h +++ b/src/verilog/verilog_synthesis_class.h @@ -42,14 +42,14 @@ class verilog_synthesist: public: verilog_synthesist( verilog_standardt _standard, + bool _ignore_initial, const namespacet &_ns, symbol_table_baset &_symbol_table, const irep_idt &_module, - const optionst &_options, message_handlert &_message_handler) : verilog_typecheck_baset(_standard, _ns, _message_handler), verilog_symbol_tablet(_symbol_table), - options(_options), + ignore_initial(_ignore_initial), value_map(NULL), module(_module), temporary_counter(0) @@ -69,7 +69,7 @@ class verilog_synthesist: [[nodiscard]] exprt synth_expr(exprt expr, symbol_statet symbol_state); protected: - const optionst &options; + bool ignore_initial; [[nodiscard]] exprt synth_expr_rec(exprt expr, symbol_statet symbol_state);