sv: carry over global typedefs from previous files

This breaks the ability to use a global typename as a standard
identifier in a subsequent input file. This is otherwise backwards
compatible, including for sources which previously included conflicting
typedefs in each input file.

diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index e2aecd99bac0f2ffd3d50459f257536af97893b8..5907707c8c7d972d3f3e42debb2125f43ee9e64b 100644 (file)
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -61,8 +61,11 @@ static void add_package_types(dict<std::string, AST::AstNode *> &user_types, std
                        }
                }
        }
-       user_type_stack.clear();
-       user_type_stack.push_back(new UserTypeMap());
+
+       // carry over typedefs from previous files, but allow them to be overridden
+       // note that these type maps are currently never reclaimed
+       if (user_type_stack.empty() || !user_type_stack.back()->empty())
+               user_type_stack.push_back(new UserTypeMap());
 }
 
 struct VerilogFrontend : public Frontend {

diff --git a/tests/verilog/typedef_across_files.ys b/tests/verilog/typedef_across_files.ys
new file mode 100644 (file)
index 0000000..ca9bba7
--- /dev/null
+++ b/tests/verilog/typedef_across_files.ys
@@ -0,0 +1,23 @@
+read_verilog -sv <<EOF
+typedef logic T;
+EOF
+
+read_verilog -sv <<EOF
+typedef T [3:0] S;
+EOF
+
+read_verilog -sv <<EOF
+module top;
+    T t;
+    S s;
+    always @* begin
+        assert ($bits(t) == 1);
+        assert ($bits(s) == 4);
+    end
+endmodule
+EOF
+
+proc
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all

diff --git a/tests/verilog/typedef_legacy_conflict.ys b/tests/verilog/typedef_legacy_conflict.ys
new file mode 100644 (file)
index 0000000..8dff4ec
--- /dev/null
+++ b/tests/verilog/typedef_legacy_conflict.ys
@@ -0,0 +1,37 @@
+read_verilog -sv <<EOF
+typedef logic T;
+typedef T [3:0] S;
+EOF
+
+read_verilog -sv <<EOF
+module example;
+    // S and T refer to the definitions from the first file
+    T t;
+    S s;
+    always @* begin
+        assert ($bits(t) == 1);
+        assert ($bits(s) == 4);
+    end
+endmodule
+
+typedef byte T;
+typedef T S;
+
+module top;
+    // S and T refer to the most recent overrides
+    T t;
+    S s;
+    always @* begin
+        assert ($bits(t) == 8);
+        assert ($bits(s) == 8);
+    end
+    example e();
+endmodule
+EOF
+
+hierarchy
+proc
+flatten
+opt -full
+select -module top
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all