simple enum test
authorJeff Wang <jjj11x@gmail.com>
Thu, 16 Jan 2020 17:03:27 +0000 (12:03 -0500)
committerJeff Wang <jeffrey.wang@ll.mit.edu>
Thu, 16 Jan 2020 23:09:03 +0000 (18:09 -0500)
tests/svtypes/enum_simple.sv [new file with mode: 0644]
tests/svtypes/enum_simple.ys [new file with mode: 0644]

diff --git a/tests/svtypes/enum_simple.sv b/tests/svtypes/enum_simple.sv
new file mode 100644 (file)
index 0000000..0c3f55c
--- /dev/null
@@ -0,0 +1,47 @@
+
+module enum_simple(input clk, input rst);
+
+       enum {s0, s1, s2, s3} test_enum;
+       typedef enum logic [1:0] {
+               ts0, ts1, ts2, ts3
+       } states_t;
+       (states_t) state;
+       (states_t) enum_const = s1;
+
+       always @(posedge clk) begin
+               if (rst) begin
+                       test_enum <= s3;
+                       state <= ts0;
+               end else begin
+                       //test_enum
+                       if (test_enum == s0)
+                               test_enum <= s1;
+                       else if (test_enum == s1)
+                               test_enum <= s2;
+                       else if (test_enum == s2)
+                               test_enum <= s3;
+                       else if (test_enum == s3)
+                               test_enum <= s0;
+                       else
+                               assert(1'b0); //should be unreachable
+
+                       //state
+                       if (state == ts0)
+                               state <= ts1;
+                       else if (state == ts1)
+                               state <= ts2;
+                       else if (state == ts2)
+                               state <= ts0;
+                       else
+                               assert(1'b0); //should be unreachable
+               end
+       end
+
+       always @(*) begin
+               assert(state != 2'h3);
+               assert(s0 == '0);
+               assert(ts0 == '0);
+               assert(enum_const == s1);
+       end
+
+endmodule
diff --git a/tests/svtypes/enum_simple.ys b/tests/svtypes/enum_simple.ys
new file mode 100644 (file)
index 0000000..7998165
--- /dev/null
@@ -0,0 +1,5 @@
+
+read_verilog -sv enum_simple.sv
+hierarchy; proc; opt
+sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts -show-all
+