From 3c029fad504fc4a7a15011e25c5da47b781d574b Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 16 Nov 2024 11:26:20 +0000
Subject: [PATCH 1/2] SVA: typechecking for sequence concatenation

---
 src/verilog/verilog_typecheck_expr.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index df419cec..178bfd7e 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -3064,6 +3064,15 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_sequence_concatenation) // a ##b c
+  {
+    expr.type() = bool_typet();
+    convert_expr(expr.op0());
+    make_boolean(expr.op0());
+    convert_expr(expr.op1());
+    make_boolean(expr.op1());
+    return std::move(expr);
+  }
   else if(
     expr.id() == ID_sva_sequence_intersect ||
     expr.id() == ID_sva_sequence_throughout ||
@@ -3352,7 +3361,7 @@ exprt verilog_typecheck_exprt::convert_trinary_expr(ternary_exprt expr)
     expr.type()=expr.op1().type();
     return std::move(expr);
   }
-  else if(expr.id()==ID_sva_cycle_delay) // #[1:2] something
+  else if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
   {
     expr.type()=bool_typet();
     convert_expr(expr.op0());

From a9e8922ee62aaf29d627fba74bd34f6b0c97709f Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 16 Nov 2024 11:47:07 +0000
Subject: [PATCH 2/2] Verilog: typechecking for remaining binary expressions

---
 src/verilog/verilog_typecheck_expr.cpp | 78 +++++++++++++++++++-------
 1 file changed, 57 insertions(+), 21 deletions(-)

diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 178bfd7e..64143c4c 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -3076,7 +3076,8 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(
     expr.id() == ID_sva_sequence_intersect ||
     expr.id() == ID_sva_sequence_throughout ||
-    expr.id() == ID_sva_sequence_within)
+    expr.id() == ID_sva_sequence_within ||
+    expr.id() == ID_sva_sequence_first_match)
   {
     auto &binary_expr = to_binary_expr(expr);
 
@@ -3206,44 +3207,79 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     expr.type() = bool_typet{};
     return std::move(expr);
   }
-  else
+  else if(
+    expr.id() == ID_plus || expr.id() == ID_minus || expr.id() == ID_mult ||
+    expr.id() == ID_power)
   {
-    // type is guessed for now
-    // hopefully propagate_type will fix it
-
-    Forall_operands(it, expr)
-      convert_expr(*it);
+    for(auto &op : expr.operands())
+      convert_expr(op);
 
     tc_binary_expr(expr);
 
-    if(expr.id()==ID_plus ||
-       expr.id()==ID_minus ||
-       expr.id()==ID_mult ||
-       expr.id()==ID_power)
-      no_bool_ops(expr);
+    no_bool_ops(expr);
 
-    expr.type()=expr.op0().type();
+    expr.type() = expr.op0().type();
+    return std::move(expr);
+  }
+  else if(
+    expr.id() == ID_bitand || expr.id() == ID_bitor || expr.id() == ID_bitxor ||
+    expr.id() == ID_bitxnor || expr.id() == ID_bitnand ||
+    expr.id() == ID_bitnor)
+  {
+    for(auto &op : expr.operands())
+      convert_expr(op);
 
-    // check Boolean operators
+    tc_binary_expr(expr);
+
+    expr.type() = expr.op0().type();
 
-    if(expr.type().id()==ID_bool)
+    // Boolean?
+    if(expr.type().id() == ID_bool)
     {
-      if(expr.id()==ID_bitand)
+      if(expr.id() == ID_bitand)
         expr.id(ID_and);
-      else if(expr.id()==ID_bitor)
+      else if(expr.id() == ID_bitor)
         expr.id(ID_or);
-      else if(expr.id()==ID_bitxor)
+      else if(expr.id() == ID_bitxor)
         expr.id(ID_xor);
-      else if(expr.id()==ID_bitxnor)
+      else if(expr.id() == ID_bitxnor)
         expr.id(ID_equal);
-      else if(expr.id()==ID_bitnand)
+      else if(expr.id() == ID_bitnand)
         expr.id(ID_nand);
-      else if(expr.id()==ID_bitnor)
+      else if(expr.id() == ID_bitnor)
         expr.id(ID_nor);
     }
 
     return std::move(expr);
   }
+  else if(
+    expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_xor ||
+    expr.id() == ID_xnor || expr.id() == ID_nand || expr.id() == ID_nor)
+  {
+    for(auto &op : expr.operands())
+    {
+      convert_expr(op);
+      make_boolean(op);
+    }
+
+    tc_binary_expr(expr);
+
+    expr.type() = expr.op0().type();
+
+    return std::move(expr);
+  }
+  else if(expr.id() == ID_verilog_value_range)
+  {
+    for(auto &op : expr.operands())
+      convert_expr(op);
+    expr.type() = expr.op0().type();
+    return std::move(expr);
+  }
+  else
+  {
+    throw errort().with_location(expr.source_location())
+      << "no conversion for binary expression " << expr.id();
+  }
 }
 
 /*******************************************************************\