Verilog: create the transition relation from the RTL representation

regression/ebmc/netlist/netlist-output1.desc

@@ -6,7 +6,6 @@ activate-multi-line-match
   Verilog::\$root.main\.clk=0->false \(input\)
   Verilog::\$root.main\.data=1->false \(input\)
   Verilog::\$root.main\.some_register=2->!3 \(latch\)
-  Verilog::\$root.main\.some_register_aux0=!3->false \(wire\)
 
 Total no. of variable bits: 3
 Total no. of latch bits: 1

regression/ebmc/smv-netlist/s_until1.desc

@@ -1,7 +1,7 @@
 CORE
 s_until1.sv
 --smv-netlist
-^LTLSPEC \!node144 U node51$
+^LTLSPEC \!node144 U node23$
 ^LTLSPEC TRUE U node151$
 ^EXIT=0$
 ^SIGNAL=0$

regression/ebmc/smv-word-level/assignment-to-part-select1.desc

@@ -2,10 +2,7 @@ CORE
 assignment-to-part-select1.sv
 --smv-word-level
 ^MODULE main$
-^INVAR data = data_aux2$
-^INVAR data_aux2 = \(\(\(\(\(\(\(\(data_aux1
-^INVAR data_aux1 = \(\(\(\(\(\(\(\(data_aux0
-^INVAR data_aux0 = \(\(\(\(\(\(\(\(0uh32_10
+^INVAR data = 0uh8_40 :: 0ud8_48 :: 0ud8_32 :: 0uh32_10\[7:0\]
 ^LTLSPEC G data = 0uh32_40302010$
 ^EXIT=0$
 ^SIGNAL=0$

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

@@ -4,8 +4,7 @@ verilog1.sv
 ^MODULE main$
 ^VAR x : unsigned word\[32\];$
 ^INIT x = 0ud32_0$
-^INVAR x_aux0 = x \+ unsigned\(0sd32_1\)$
-^TRANS next\(x\) = x_aux0$
+^TRANS next\(x\) = x \+ unsigned\(0sd32_1\)$
 ^LTLSPEC F x = unsigned\(0sd32_10\)$
 ^EXIT=0$
 ^SIGNAL=0$

regression/verilog/initial/declaration_assignment1.desc

@@ -1,9 +1,12 @@
-KNOWNBUG
+CORE
 declaration_assignment1.sv
 
+^\[main\.assert\.1\] main\.some_data == 123: PROVED .*$
+^\[main\.assert\.2\] always main\.some_data == 123: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This gives the wrong result.
+Variable declaration assignments happen before any initial or always
+procedure, per 1800-2017 10.5.

regression/verilog/structs/member_assignment2.desc

@@ -0,0 +1,12 @@
+CORE
+member_assignment2.sv
+--bound 3
+^\[main\.p1\] always \(##1 main\.s\.field1 == 0\): PROVED up to bound 3$
+^\[main\.p2\] always \(##1 main\.s\.field2 == 1\): PROVED up to bound 3$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This is the first example in
+https://github.com/diffblue/hw-cbmc/issues/2103

regression/verilog/structs/member_assignment2.sv

@@ -0,0 +1,23 @@
+typedef struct {
+  logic field1;
+  logic field2;
+} structure_t;
+
+module main(input wire clk);
+
+  structure_t s;
+
+  // The fields of a struct may be assigned in different
+  // always constructs.
+  always @(posedge clk) begin
+    s.field1 <= 0;
+  end
+
+  always @(posedge clk) begin
+    s.field2 <= 1;
+  end
+
+  p1: assert property (@(posedge clk) ##1 s.field1 == 0);
+  p2: assert property (@(posedge clk) ##1 s.field2 == 1);
+
+endmodule

regression/verilog/synthesis/always_comb2.no-simple-aig.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 always_comb2.sv
 --aig
 ^\[main\.p0\] always main\.data == 0 -> main\.decoded == 1: PROVED .*$
@@ -9,4 +9,4 @@ always_comb2.sv
 --
 ^warning: ignoring
 --
-This segfaults.
+This used to segfault.

src/hw-cbmc/hw_cbmc_parse_options.cpp

@@ -488,6 +488,11 @@ int hw_cbmc_parse_optionst::doit()
 
     verilog_ebmc_languaget verilog_language(
       verilog_cmdline, ui_message_handler);
+
+    // We unwind the module that is given on the command line, and
+    // hence need the transition relation of that module.
+    verilog_language.use_synthesis = true;
+
     auto transition_system = verilog_language.transition_system();
 
     if(!transition_system.has_value())

src/verilog/Makefile

@@ -31,6 +31,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_standard.cpp \
       verilog_symbol_table.cpp \
       verilog_synthesis.cpp \
+      verilog_transition_relation.cpp \
       verilog_typecheck.cpp \
       verilog_typecheck_base.cpp \
       verilog_typecheck_expr.cpp \

src/verilog/verilog_ebmc_language.cpp

@@ -31,6 +31,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #include "verilog_preprocessor.h"
 #include "verilog_rtl.h"
 #include "verilog_synthesis.h"
+#include "verilog_transition_relation.h"
 #include "verilog_typecheck.h"
 #include "verilog_types.h"
 
@@ -201,30 +202,38 @@ void verilog_ebmc_languaget::typecheck_module(
     const namespacet ns(symbol_table);
     rtl.output(ns, std::cout);
 
-    return; // no synthesis
+    return;
   }
 
-  messaget message(message_handler);
-  log.status() << "Synthesis " << module.identifier << messaget::eom;
+  // The hw-cbmc flow continues to use synthesis, since it unwinds
+  // the module that is given on the command line, and hence requires
+  // the transition relation of that module.
+  if(use_synthesis)
+  {
+    log.status() << "Synthesis " << module.identifier << messaget::eom;
 
-  const bool ignore_initial = cmdline.isset("ignore-initial");
-  const bool initial_zero = cmdline.isset("initial-zero");
+    const bool ignore_initial = cmdline.isset("ignore-initial");
+    const bool initial_zero = cmdline.isset("initial-zero");
 
-  try
-  {
-    verilog_synthesis(
-      symbol_table,
-      module.identifier,
-      module.parse_tree.standard,
-      ignore_initial,
-      initial_zero,
-      message_handler);
-  }
-  catch(ebmc_errort)
-  {
-    log.error() << "CONVERSION ERROR" << messaget::eom;
-    throw ebmc_errort{}.with_exit_code(2);
+    try
+    {
+      verilog_synthesis(
+        symbol_table,
+        module.identifier,
+        module.parse_tree.standard,
+        ignore_initial,
+        initial_zero,
+        message_handler);
+    }
+    catch(ebmc_errort)
+    {
+      log.error() << "CONVERSION ERROR" << messaget::eom;
+      throw ebmc_errort{}.with_exit_code(2);
+    }
   }
+
+  // Otherwise, the transition relation is created from the RTL
+  // representation when the $root module is converted.
 }
 
 transition_systemt verilog_ebmc_languaget::typecheck(
@@ -347,14 +356,38 @@ void verilog_ebmc_languaget::create_root_module(
   const bool ignore_initial = cmdline.isset("ignore-initial");
   const bool initial_zero = cmdline.isset("initial-zero");
 
-  // Synthesize $root, which expands the top-level module instance
-  transition_system.trans_expr = verilog_synthesis(
-    symbol_table,
-    root_identifier,
-    standard,
-    ignore_initial,
-    initial_zero,
-    message_handler);
+  // Create the transition relation for $root from its RTL
+  // representation, which expands the top-level module instance.
+  // The hw-cbmc flow uses synthesis instead.
+  try
+  {
+    if(use_synthesis)
+    {
+      transition_system.trans_expr = verilog_synthesis(
+        symbol_table,
+        root_identifier,
+        standard,
+        ignore_initial,
+        initial_zero,
+        message_handler);
+    }
+    else
+    {
+      transition_system.trans_expr = verilog_transition_relation(
+        symbol_table,
+        root_identifier,
+        standard,
+        ignore_initial,
+        initial_zero,
+        message_handler);
+    }
+  }
+  catch(ebmc_errort &)
+  {
+    messaget log{message_handler};
+    log.error() << "CONVERSION ERROR" << messaget::eom;
+    throw;
+  }
 }
 
 static void make_next_state(exprt &expr)

src/verilog/verilog_ebmc_language.h

@@ -36,6 +36,12 @@ class verilog_ebmc_languaget : public ebmc_languaget
   // produce the transition system, and return it
   std::optional<transition_systemt> transition_system() override;
 
+  /// Use synthesis instead of the conversion from the register-
+  /// transfer level representation. This is used by hw-cbmc, which
+  /// unwinds the module that is given on the command line, and hence
+  /// requires the transition relation of that module.
+  bool use_synthesis = false;
+
   /// a Verilog parse tree forest
   using parse_treet = verilog_parse_treet;
   using parse_treest = std::list<parse_treet>;