From 91db9b4a6c7d83ac93476e942b00d356ca42e000 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Thu, 20 Feb 2025 10:45:39 +0000 Subject: [PATCH] SystemVerilog: --initial-zero The SystemVerilog standard specifies that variables are to be zero initialized before simulation begins. Some synthesis tools generate logic to achieve this, whereas others do not. This adds the option --initial-zero to match the synthesis semantics when appropriate. --- regression/verilog/initial/initial-zero1.desc | 9 ++++ regression/verilog/initial/initial-zero1.sv | 13 +++++ src/ebmc/ebmc_parse_options.cpp | 1 + src/ebmc/ebmc_parse_options.h | 2 +- src/ebmc/transition_system.cpp | 4 ++ src/verilog/Makefile | 1 + src/verilog/verilog_expr.h | 6 +++ src/verilog/verilog_initializer.cpp | 48 +++++++++++++++++++ src/verilog/verilog_initializer.h | 19 ++++++++ src/verilog/verilog_language.cpp | 2 + src/verilog/verilog_language.h | 1 + src/verilog/verilog_synthesis.cpp | 43 +++++++++++++++-- src/verilog/verilog_synthesis.h | 1 + src/verilog/verilog_synthesis_class.h | 3 ++ 14 files changed, 148 insertions(+), 5 deletions(-) create mode 100644 regression/verilog/initial/initial-zero1.desc create mode 100644 regression/verilog/initial/initial-zero1.sv create mode 100644 src/verilog/verilog_initializer.cpp create mode 100644 src/verilog/verilog_initializer.h diff --git a/regression/verilog/initial/initial-zero1.desc b/regression/verilog/initial/initial-zero1.desc new file mode 100644 index 000000000..5e52114a5 --- /dev/null +++ b/regression/verilog/initial/initial-zero1.desc @@ -0,0 +1,9 @@ +CORE +initial-zero1.sv +--top main --initial-zero --bound 3 +^\[main\.p1\] main\.t == 0: PROVED up to bound 3$ +^\[main\.p2\] ##1 main\.t == 5: PROVED up to bound 3$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/verilog/initial/initial-zero1.sv b/regression/verilog/initial/initial-zero1.sv new file mode 100644 index 000000000..35da9a5ff --- /dev/null +++ b/regression/verilog/initial/initial-zero1.sv @@ -0,0 +1,13 @@ +module main(input clk); + + reg [7:0] t; + + always_ff @(posedge clk) t = 5; + + initial p1: assert property (t == 0); + initial p2: assert property (##1 t == 5); + + chandle ch; + initial p3: assert property (ch == null); + +endmodule diff --git a/src/ebmc/ebmc_parse_options.cpp b/src/ebmc/ebmc_parse_options.cpp index 573c43932..9a745a108 100644 --- a/src/ebmc/ebmc_parse_options.cpp +++ b/src/ebmc/ebmc_parse_options.cpp @@ -417,6 +417,7 @@ void ebmc_parse_optionst::help() " {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" + " {y--initial-zero} \t initialize variables with zero\n" "\n" "Debugging options:\n" " {y--preprocess} \t output the preprocessed source file\n" diff --git a/src/ebmc/ebmc_parse_options.h b/src/ebmc/ebmc_parse_options.h index aa3b69688..4ff7b7b3b 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):(ignore-initial)" + "(reset):(ignore-initial)(initial-zero)" "(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 71ea73b0e..1aca22783 100644 --- a/src/ebmc/transition_system.cpp +++ b/src/ebmc/transition_system.cpp @@ -178,6 +178,10 @@ static bool parse( if(cmdline.isset("ignore-initial")) options.set_option("ignore-initial", true); + // do --initial-zero + if(cmdline.isset("initial-zero")) + options.set_option("initial-zero", true); + language.set_language_options(options, message_handler); message.status() << "Parsing " << filename << messaget::eom; diff --git a/src/verilog/Makefile b/src/verilog/Makefile index 2e4bc1a6d..9f5932b50 100644 --- a/src/verilog/Makefile +++ b/src/verilog/Makefile @@ -7,6 +7,7 @@ SRC = aval_bval_encoding.cpp \ verilog_elaborate_type.cpp \ verilog_expr.cpp \ verilog_generate.cpp \ + verilog_initializer.cpp \ verilog_interfaces.cpp \ verilog_interpreter.cpp \ verilog_language.cpp \ diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index e99fdff48..e52366c1c 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -1073,6 +1073,12 @@ class verilog_initialt:public verilog_statementt operands().resize(1); } + explicit verilog_initialt(verilog_statementt _statement) + : verilog_statementt(ID_initial) + { + add_to_operands(std::move(_statement)); + } + verilog_statementt &statement() { return static_cast(op0()); diff --git a/src/verilog/verilog_initializer.cpp b/src/verilog/verilog_initializer.cpp new file mode 100644 index 000000000..ba9b71ec5 --- /dev/null +++ b/src/verilog/verilog_initializer.cpp @@ -0,0 +1,48 @@ +/*******************************************************************\ + +Module: Verilog Initializer + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#include "verilog_initializer.h" + +#include +#include + +std::optional verilog_zero_initializer(const typet &type) +{ + if(type.id() == ID_signedbv || type.id() == ID_unsignedbv) + return from_integer(0, type); + else if(type.id() == ID_bool) + return false_exprt{}; + else if(type.id() == ID_array) + { + auto &array_type = to_array_type(type); + auto zero_element_opt = verilog_zero_initializer(array_type.element_type()); + if(!zero_element_opt.has_value()) + return {}; + else + return array_of_exprt{*zero_element_opt, array_type}; + } + else if(type.id() == ID_struct) + { + auto &struct_type = to_struct_type(type); + exprt::operandst member_values; + for(auto &component : struct_type.components()) + { + auto member_value_opt = verilog_zero_initializer(component.type()); + if(!member_value_opt.has_value()) + return {}; + member_values.push_back(*member_value_opt); + } + return struct_exprt{std::move(member_values), struct_type}; + } + else if(type.id() == ID_verilog_chandle) + { + return constant_exprt{ID_NULL, type}; + } + else + return {}; +} diff --git a/src/verilog/verilog_initializer.h b/src/verilog/verilog_initializer.h new file mode 100644 index 000000000..6c8ea9f93 --- /dev/null +++ b/src/verilog/verilog_initializer.h @@ -0,0 +1,19 @@ +/*******************************************************************\ + +Module: Verilog Initializer + +Author: Daniel Kroening, dkr@amazon.com + +\*******************************************************************/ + +#ifndef CPROVER_VERILOG_INITIALIZER_H +#define CPROVER_VERILOG_INITIALIZER_H + +#include + +class exprt; +class typet; + +std::optional verilog_zero_initializer(const typet &); + +#endif diff --git a/src/verilog/verilog_language.cpp b/src/verilog/verilog_language.cpp index 6cd3bb386..4329a1272 100644 --- a/src/verilog/verilog_language.cpp +++ b/src/verilog/verilog_language.cpp @@ -40,6 +40,7 @@ void verilog_languaget::set_language_options( 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"); + initial_zero = options.get_bool_option("initial-zero"); } /*******************************************************************\ @@ -196,6 +197,7 @@ bool verilog_languaget::typecheck( module, parse_tree.standard, ignore_initial, + initial_zero, message_handler)) { return true; diff --git a/src/verilog/verilog_language.h b/src/verilog/verilog_language.h index 475d6ecba..9051afc20 100644 --- a/src/verilog/verilog_language.h +++ b/src/verilog/verilog_language.h @@ -95,6 +95,7 @@ class verilog_languaget:public languaget bool vl2smv_extensions = false; bool warn_implicit_nets = false; bool ignore_initial = false; + bool initial_zero = 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 fb471e806..983bf4294 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/src/verilog/verilog_synthesis.cpp @@ -23,6 +23,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "expr2verilog.h" #include "sva_expr.h" #include "verilog_expr.h" +#include "verilog_initializer.h" #include "verilog_lowering.h" #include "verilog_typecheck_expr.h" @@ -1463,6 +1464,7 @@ void verilog_synthesist::synth_module_instance( module_identifier, standard, ignore_initial, + initial_zero, get_message_handler()); for(auto &instance : statement.instances()) @@ -1933,6 +1935,8 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) { { DATA_INVARIANT(declarator.id() == ID_declarator, "must have declarator"); + auto lhs = declarator.symbol_expr(); + // This is reg x = ... or wire x = ... if(declarator.has_value()) { @@ -1941,9 +1945,7 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) { construct=constructt::INITIAL; event_guard=event_guardt::NONE; - auto lhs = declarator.symbol_expr(); auto rhs = declarator.value(); - const symbolt &symbol = ns.lookup(lhs); if(symbol.is_state_var) @@ -1964,6 +1966,26 @@ void verilog_synthesist::synth_decl(const verilog_declt &statement) { synth_continuous_assign(assign); } } + else if(initial_zero) + { + const symbolt &symbol = ns.lookup(lhs); + + if(symbol.is_state_var) + { + // much like: initial LHS=0; + auto rhs_opt = verilog_zero_initializer(lhs.type()); + if(!rhs_opt.has_value()) + { + throw errort().with_location(declarator.source_location()) + << "cannot zero-initialize `" << to_string(lhs) << "'"; + } + verilog_initialt initial{verilog_blocking_assignt{lhs, *rhs_opt}}; + initial.statement().add_source_location() = + declarator.source_location(); + initial.add_source_location() = declarator.source_location(); + synth_initial(initial); + } + } } } @@ -3724,11 +3746,18 @@ bool verilog_synthesis( const irep_idt &module, verilog_standardt standard, bool ignore_initial, + bool initial_zero, message_handlert &message_handler) { const namespacet ns(symbol_table); verilog_synthesist verilog_synthesis( - standard, ignore_initial, ns, symbol_table, module, message_handler); + standard, + ignore_initial, + initial_zero, + ns, + symbol_table, + module, + message_handler); return verilog_synthesis.typecheck_main(); } @@ -3757,7 +3786,13 @@ bool verilog_synthesis( message_handler.get_message_count(messaget::M_ERROR); verilog_synthesist verilog_synthesis( - standard, false, ns, symbol_table, module_identifier, message_handler); + standard, + false, + false, + ns, + symbol_table, + module_identifier, + message_handler); try { diff --git a/src/verilog/verilog_synthesis.h b/src/verilog/verilog_synthesis.h index 58b48403e..c353c38aa 100644 --- a/src/verilog/verilog_synthesis.h +++ b/src/verilog/verilog_synthesis.h @@ -20,6 +20,7 @@ bool verilog_synthesis( const irep_idt &module, verilog_standardt, bool ignore_initial, + bool initial_zero, message_handlert &); bool verilog_synthesis( diff --git a/src/verilog/verilog_synthesis_class.h b/src/verilog/verilog_synthesis_class.h index 4c8723c6b..679ea8234 100644 --- a/src/verilog/verilog_synthesis_class.h +++ b/src/verilog/verilog_synthesis_class.h @@ -43,6 +43,7 @@ class verilog_synthesist: verilog_synthesist( verilog_standardt _standard, bool _ignore_initial, + bool _initial_zero, const namespacet &_ns, symbol_table_baset &_symbol_table, const irep_idt &_module, @@ -50,6 +51,7 @@ class verilog_synthesist: : verilog_typecheck_baset(_standard, _ns, _message_handler), verilog_symbol_tablet(_symbol_table), ignore_initial(_ignore_initial), + initial_zero(_initial_zero), value_map(NULL), module(_module), temporary_counter(0) @@ -70,6 +72,7 @@ class verilog_synthesist: protected: bool ignore_initial; + bool initial_zero; [[nodiscard]] exprt synth_expr_rec(exprt expr, symbol_statet symbol_state);