From febe7706a2013a834f1bcd1200a9ac9d997e79c4 Mon Sep 17 00:00:00 2001
From: Jeff Wang <jjj11x@gmail.com>
Date: Thu, 16 Jan 2020 12:03:27 -0500
Subject: [PATCH] simple enum test

---
 tests/svtypes/enum_simple.sv | 47 ++++++++++++++++++++++++++++++++++++
 tests/svtypes/enum_simple.ys |  5 ++++
 2 files changed, 52 insertions(+)
 create mode 100644 tests/svtypes/enum_simple.sv
 create mode 100644 tests/svtypes/enum_simple.ys

diff --git a/tests/svtypes/enum_simple.sv b/tests/svtypes/enum_simple.sv
new file mode 100644
index 000000000..0c3f55c34
--- /dev/null
+++ b/tests/svtypes/enum_simple.sv
@@ -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
index 000000000..79981657b
--- /dev/null
+++ b/tests/svtypes/enum_simple.ys
@@ -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
+
-- 
2.30.2