Verilog: fix for case statements

This fixes the synthesis of case statements where the default label is not
the last.

Author: kroening

regression/verilog/case/mini-alu.desc

@@ -1,10 +1,8 @@
-KNOWNBUG
+CORE
 mini-alu.sv
 --module alu --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The "default:;" in the assertion block causes an invalid expression to be
-generated.

src/verilog/verilog_expr.h

@@ -1090,14 +1090,19 @@ inline verilog_case_baset &to_verilog_case_base(exprt &expr)
   return static_cast<verilog_case_baset &>(expr);
 }
 
-class verilog_case_itemt:public exprt
+class verilog_case_itemt : public binary_exprt
 {
 public:
-  verilog_case_itemt():exprt("case_item")
+  verilog_case_itemt(exprt value, verilog_statementt statement)
+    : binary_exprt(std::move(value), ID_case_item, std::move(statement))
   {
-    operands().resize(2);
   }
-  
+
+  bool is_default() const
+  {
+    return case_value().id() == ID_default;
+  }
+
   inline exprt &case_value()
   {
     return op0();
@@ -1117,19 +1122,23 @@ class verilog_case_itemt:public exprt
   {
     return to_verilog_statement(op1());
   }
+
+protected:
+  using binary_exprt::op0;
+  using binary_exprt::op1;
 };
 
 inline const verilog_case_itemt &to_verilog_case_item(const exprt &expr)
 {
   PRECONDITION(expr.id() == ID_case_item);
-  binary_exprt::check(expr);
+  verilog_case_itemt::check(expr);
   return static_cast<const verilog_case_itemt &>(expr);
 }
 
 inline verilog_case_itemt &to_verilog_case_item(exprt &expr)
 {
   PRECONDITION(expr.id() == ID_case_item);
-  binary_exprt::check(expr);
+  verilog_case_itemt::check(expr);
   return static_cast<verilog_case_itemt &>(expr);
 }
 

src/verilog/verilog_synthesis.cpp

@@ -2866,6 +2866,7 @@ void verilog_synthesist::synth_case(
   // we convert the rest to if-then-else
   exprt start;
   exprt *last_if=&start;
+  std::optional<verilog_statementt> default_case;
 
   for(unsigned i=1; i<statement.operands().size(); i++)
   {
@@ -2876,20 +2877,28 @@ void verilog_synthesist::synth_case(
       throw errort() << "expected case_item";
     }
 
-    if(e.operands().size()!=2)
+    auto &case_item = to_verilog_case_item(e);
+
+    // default?
+    if(case_item.is_default())
+      default_case = case_item.case_statement();
+    else
     {
-      throw errort().with_location(e.source_location())
-        << "case_item expected to have two operands";
-    }
+      exprt if_statement(ID_if);
+      if_statement.reserve_operands(3);
+      if_statement.add_to_operands(
+        synth_case_values(case_item.case_value(), case_operand));
+      if_statement.add_to_operands(case_item.case_statement());
 
-    exprt if_statement(ID_if);
-    if_statement.reserve_operands(3);
-    if_statement.add_to_operands(
-      synth_case_values(to_binary_expr(e).op0(), case_operand));
-    if_statement.add_to_operands(to_binary_expr(e).op1());
+      last_if->add_to_operands(std::move(if_statement));
+      last_if = &last_if->operands().back();
+    }
+  }
 
-    last_if->add_to_operands(std::move(if_statement));
-    last_if=&last_if->operands().back();
+  if(default_case.has_value())
+  {
+    // Attach the 'default' to the final 'if' as 'else'
+    last_if->add_to_operands(std::move(default_case.value()));
   }
 
   // synthesize the new if-then-else