From e8822870d7d1ae1be966bc38c834bd80d36c6a16 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 24 Dec 2023 19:50:29 +0000
Subject: [PATCH] Verilog: add symbols below generate-if

---
 regression/verilog/generate/generate-if1.desc |  6 +++
 regression/verilog/generate/generate-if1.v    | 18 ++++++++
 .../verilog/generate/generate-inst1.desc      |  2 +-
 src/verilog/verilog_interfaces.cpp            | 43 +++++++++++++++++++
 src/verilog/verilog_typecheck.h               |  2 +
 5 files changed, 70 insertions(+), 1 deletion(-)
 create mode 100644 regression/verilog/generate/generate-if1.desc
 create mode 100644 regression/verilog/generate/generate-if1.v

diff --git a/regression/verilog/generate/generate-if1.desc b/regression/verilog/generate/generate-if1.desc
new file mode 100644
index 000000000..77e29f71c
--- /dev/null
+++ b/regression/verilog/generate/generate-if1.desc
@@ -0,0 +1,6 @@
+CORE
+generate-if1.v
+--module main --bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/generate/generate-if1.v b/regression/verilog/generate/generate-if1.v
new file mode 100644
index 000000000..29132cb7b
--- /dev/null
+++ b/regression/verilog/generate/generate-if1.v
@@ -0,0 +1,18 @@
+module main;
+
+  parameter MAX = 'd1;
+  parameter something = 1;
+
+  wire [MAX-1:0] my_wire;
+
+  generate
+    if(something) begin
+      genvar i;
+      for (i = 0; i < MAX; i = i + 1)
+        assign my_wire[i] = 1;
+    end
+  endgenerate
+
+  always assert p1: my_wire == 1;
+
+endmodule
diff --git a/regression/verilog/generate/generate-inst1.desc b/regression/verilog/generate/generate-inst1.desc
index c375b9896..0985854e0 100644
--- a/regression/verilog/generate/generate-inst1.desc
+++ b/regression/verilog/generate/generate-inst1.desc
@@ -1,4 +1,4 @@
-CORE
+KNOWNBUG
 generate-inst1.v
 
 ^EXIT=10$
diff --git a/src/verilog/verilog_interfaces.cpp b/src/verilog/verilog_interfaces.cpp
index fb84149e1..3b16db9bd 100644
--- a/src/verilog/verilog_interfaces.cpp
+++ b/src/verilog/verilog_interfaces.cpp
@@ -722,6 +722,45 @@ void verilog_typecheckt::interface_generate_block(
 
 /*******************************************************************\
 
+Function: verilog_typecheckt::interface_generate_for
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheckt::interface_generate_for(
+  const verilog_generate_fort &generate_for)
+{
+  interface_module_item(generate_for.body());
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheckt::interface_generate_if
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheckt::interface_generate_if(
+  const verilog_generate_ift &generate_if)
+{
+  interface_module_item(generate_if.then_case());
+
+  if(generate_if.has_else_case())
+    interface_module_item(generate_if.else_case());
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheckt::interface_module_item
 
   Inputs:
@@ -757,6 +796,10 @@ void verilog_typecheckt::interface_module_item(
     interface_statement(to_verilog_initial(module_item).statement());
   else if(module_item.id()==ID_generate_block)
     interface_generate_block(to_verilog_generate_block(module_item));
+  else if(module_item.id() == ID_generate_if)
+    interface_generate_if(to_verilog_generate_if(module_item));
+  else if(module_item.id() == ID_generate_for)
+    interface_generate_for(to_verilog_generate_for(module_item));
 }
 
 /*******************************************************************\
diff --git a/src/verilog/verilog_typecheck.h b/src/verilog/verilog_typecheck.h
index d2816ae4c..ffd4ac22c 100644
--- a/src/verilog/verilog_typecheck.h
+++ b/src/verilog/verilog_typecheck.h
@@ -120,6 +120,8 @@ class verilog_typecheckt:
   void interface_module_item(const class verilog_module_itemt &);
   void interface_block(const class verilog_blockt &);
   void interface_generate_block(const class verilog_generate_blockt &);
+  void interface_generate_for(const verilog_generate_fort &);
+  void interface_generate_if(const verilog_generate_ift &);
   void interface_statement(const class verilog_statementt &);
   void interface_function_or_task(const class verilog_declt &);