ebmc: --word-level-smv

CHANGELOG

@@ -4,6 +4,7 @@
 * SystemVerilog: assignment patterns with keys for structs
 * SMV: LTL V operator, xnor operator
 * SMV: word types and operators
+* --smv-word-level outputs the model as word-level SMV
 
 # EBMC 5.5
 

regression/ebmc/smv-word-level/verilog1.desc

@@ -0,0 +1,11 @@
+CORE
+verilog1.v
+--smv-word-level
+^MODULE main$
+^VAR x : unsigned word\[32\];$
+^INIT main\.x = 0ud32_0$
+^INVAR Verilog::main\.x_aux0 = main\.x \+ 0ud32_1$
+^TRANS next\(main\.x\) = Verilog::main\.x_aux0$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/verilog1.v

@@ -0,0 +1,10 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x = 0;
+
+  always @(posedge clk)
+    x = x + 1;
+
+endmodule

src/ebmc/Makefile

@@ -24,6 +24,7 @@ SRC = \
       netlist.cpp \
       neural_liveness.cpp \
       output_file.cpp \
+      output_smv_word_level.cpp \
       output_verilog.cpp \
       property_checker.cpp \
       random_traces.cpp \

src/ebmc/ebmc_parse_options.cpp

@@ -21,6 +21,7 @@ Author: Daniel Kroening, [email protected]
 #include "netlist.h"
 #include "neural_liveness.h"
 #include "output_file.h"
+#include "output_smv_word_level.h"
 #include "property_checker.h"
 #include "random_traces.h"
 #include "ranking_function.h"
@@ -215,6 +216,15 @@ int ebmc_parse_optionst::doit()
     auto properties = ebmc_propertiest::from_command_line(
       cmdline, transition_system, ui_message_handler);
 
+    if(cmdline.isset("smv-word-level"))
+    {
+      auto filename = cmdline.value_opt("outfile").value_or("-");
+      output_filet output_file{filename};
+      output_smv_word_level(
+        transition_system, properties, output_file.stream());
+      return 0;
+    }
+
     if(cmdline.isset("show-properties"))
     {
       show_properties(properties, ui_message_handler);
@@ -418,6 +428,7 @@ void ebmc_parse_optionst::help()
     " {y--smv-netlist}               \t show netlist in SMV format\n"
     " {y--dot-netlist}               \t show netlist in DOT format\n"
     " {y--show-trans}                \t show transition system\n"
+    " {y--smv-word-level}            \t output word-level SMV\n"
     " {y--verbosity} {u#}            \t verbosity level, from 0 (silent) to 10 (everything)\n"
     // clang-format on
     "\n");

src/ebmc/ebmc_parse_options.h

@@ -44,7 +44,8 @@ class ebmc_parse_optionst:public parse_options_baset
         "(smt2)(bitwuzla)(boolector)(cvc3)(cvc4)(cvc5)(mathsat)(yices)(z3)"
         "(minisat)(cadical)"
         "(aig)(stop-induction)(stop-minimize)(start):(coverage)(naive)"
-        "(compute-ct)(dot-netlist)(smv-netlist)(vcd):"
+        "(compute-ct)(dot-netlist)(smv-netlist)(smv-word-level)"
+        "(vcd):"
         "(random-traces)(trace-steps):(random-seed):(traces):"
         "(random-trace)(random-waveform)"
         "(bmc-with-assumptions)"

src/ebmc/output_smv_word_level.cpp

@@ -0,0 +1,217 @@
+/*******************************************************************\
+
+Module: Word-Level SMV Output
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "output_smv_word_level.h"
+
+#include <util/bitvector_types.h>
+
+#include <smvlang/expr2smv.h>
+
+#include "ebmc_error.h"
+#include "ebmc_properties.h"
+#include "transition_system.h"
+
+#include <ostream>
+
+class smv_type_printert
+{
+public:
+  explicit smv_type_printert(const typet &__type) : _type(__type)
+  {
+  }
+
+  const typet &type() const
+  {
+    return _type;
+  }
+
+protected:
+  const typet &_type;
+};
+
+std::ostream &
+operator<<(std::ostream &out, const smv_type_printert &type_printer)
+{
+  auto &type = type_printer.type();
+
+  if(type.id() == ID_bool)
+    return out << "boolean";
+  else if(type.id() == ID_signedbv)
+    return out << "signed word[" << to_signedbv_type(type).get_width() << "]";
+  else if(type.id() == ID_unsignedbv)
+    return out << "unsigned word[" << to_unsignedbv_type(type).get_width()
+               << "]";
+  else
+    throw ebmc_errort{} << "cannot convert type " << type.id() << " to SMV";
+
+  return out;
+}
+
+static void smv_state_variables(
+  const transition_systemt &transition_system,
+  std::ostream &out)
+{
+  bool found = false;
+
+  const auto module = transition_system.main_symbol->name;
+  const auto &symbol_table = transition_system.symbol_table;
+
+  for(auto m_it = symbol_table.symbol_module_map.lower_bound(module);
+      m_it != symbol_table.symbol_module_map.upper_bound(module);
+      m_it++)
+  {
+    const irep_idt &identifier = m_it->second;
+
+    symbol_tablet::symbolst::const_iterator s_it =
+      symbol_table.symbols.find(identifier);
+
+    if(s_it == symbol_table.symbols.end())
+      throw ebmc_errort{} << "failed to find symbol " << identifier;
+
+    const symbolt &symbol = s_it->second;
+
+    if(symbol.is_state_var)
+    {
+      out << "VAR " << symbol.base_name << " : "
+          << smv_type_printert{symbol.type} << ";\n";
+      found = true;
+    }
+  }
+
+  if(found)
+    out << '\n';
+}
+
+static void
+smv_initial_states(const exprt &expr, const namespacet &ns, std::ostream &out)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      smv_initial_states(conjunct, ns, out);
+  }
+  else if(expr.is_true())
+  {
+    // ignore
+  }
+  else
+  {
+    out << "INIT " << expr2smv(expr, ns) << '\n';
+  }
+}
+
+static void smv_initial_states(
+  const transition_systemt &transition_system,
+  std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+  smv_initial_states(transition_system.trans_expr.init(), ns, out);
+}
+
+static void
+smv_invar(const exprt &expr, const namespacet &ns, std::ostream &out)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      smv_initial_states(conjunct, ns, out);
+  }
+  else if(expr.is_true())
+  {
+    // ignore
+  }
+  else
+  {
+    out << "INVAR " << expr2smv(expr, ns) << '\n';
+  }
+}
+
+static void
+smv_invar(const transition_systemt &transition_system, std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+  smv_invar(transition_system.trans_expr.invar(), ns, out);
+}
+
+static void smv_transition_relation(
+  const exprt &expr,
+  const namespacet &ns,
+  std::ostream &out)
+{
+  if(expr.id() == ID_and)
+  {
+    for(auto &conjunct : expr.operands())
+      smv_initial_states(conjunct, ns, out);
+  }
+  else if(expr.is_true())
+  {
+    // ignore
+  }
+  else
+  {
+    out << "TRANS " << expr2smv(expr, ns) << '\n';
+  }
+}
+
+static void smv_transition_relation(
+  const transition_systemt &transition_system,
+  std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+  smv_transition_relation(transition_system.trans_expr.trans(), ns, out);
+}
+
+static void smv_properties(
+  const transition_systemt &transition_system,
+  const ebmc_propertiest &properties,
+  std::ostream &out)
+{
+  const namespacet ns(transition_system.symbol_table);
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled() || property.is_assumed())
+      continue;
+
+    if(is_CTL(property.normalized_expr))
+    {
+      out << "CTLSPEC " << expr2smv(property.normalized_expr, ns);
+    }
+    else if(is_LTL(property.normalized_expr))
+    {
+      out << "LTLSPEC " << expr2smv(property.normalized_expr, ns);
+    }
+    else
+      out << "-- " << property.identifier << ": not converted\n";
+
+    out << '\n';
+  }
+}
+
+void output_smv_word_level(
+  const transition_systemt &transition_system,
+  const ebmc_propertiest &properties,
+  std::ostream &out)
+{
+  out << "MODULE main\n\n";
+
+  // state-holding elements first
+  smv_state_variables(transition_system, out);
+
+  // initial state constraints
+  smv_initial_states(transition_system, out);
+
+  // in-state invariants
+  smv_invar(transition_system, out);
+
+  // transition relation
+  smv_transition_relation(transition_system, out);
+
+  // properties
+  smv_properties(transition_system, properties, out);
+}

src/ebmc/output_smv_word_level.h

@@ -0,0 +1,23 @@
+/*******************************************************************\
+
+Module: Word-Level SMV Output
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef EBMC_OUTPUT_SMV_WORD_LEVEL_H
+#define EBMC_OUTPUT_SMV_WORD_LEVEL_H
+
+#include <iosfwd>
+
+class ebmc_propertiest;
+class transition_systemt;
+
+/// outputs word-level SMV
+void output_smv_word_level(
+  const transition_systemt &,
+  const ebmc_propertiest &,
+  std::ostream &);
+
+#endif // EBMC_OUTPUT_SMV_WORD_LEVEL_H