6 files changed, 78 insertions, 0 deletions

diff --git a/tests/verific/.gitignore b/tests/verific/.gitignore
new file mode 100644
index 000000000..b48f808a1
--- /dev/null
+++ b/tests/verific/.gitignore
@@ -0,0 +1,3 @@
+/*.log
+/*.out
+/run-test.mk
diff --git a/tests/verific/case.sv b/tests/verific/case.sv
new file mode 100644
index 000000000..ed8529b91
--- /dev/null
+++ b/tests/verific/case.sv
@@ -0,0 +1,28 @@
+module top (
+	input clk,
+	input [5:0] currentstate,
+	output reg [1:0] o
+	);
+	always @ (posedge clk)
+	begin
+		case (currentstate)
+			5'd1,5'd2, 5'd3: 
+				begin 
+					o <= 2'b01;
+				end	
+			5'd4:
+			  	begin
+					o <= 2'b10;
+				end
+			5'd5,5'd6,5'd7: 
+				begin
+					o <= 2'b11;
+				end
+			default :
+				begin
+					o <= 2'b00;
+				end
+		endcase
+	end
+endmodule
+
diff --git a/tests/verific/case.ys b/tests/verific/case.ys
new file mode 100644
index 000000000..a181b39cf
--- /dev/null
+++ b/tests/verific/case.ys
@@ -0,0 +1,16 @@
+verific -cfg db_abstract_case_statement_synthesis 0
+read -sv case.sv
+verific -import top 
+prep
+rename top gold
+
+verific -cfg db_abstract_case_statement_synthesis 1
+read -sv case.sv
+verific -import top 
+prep
+rename top gate
+
+miter -equiv -flatten -make_assert gold gate miter
+prep -top miter
+clk2fflogic
+sat -set-init-zero -tempinduct -prove-asserts -verify
diff --git a/tests/verific/range_case.sv b/tests/verific/range_case.sv
new file mode 100644
index 000000000..9843feafe
--- /dev/null
+++ b/tests/verific/range_case.sv
@@ -0,0 +1,11 @@
+module top(input clk, input signed [3:0] sel_w , output reg out);
+
+always @ (posedge clk)
+begin
+    case (sel_w) inside
+        [-4:3] : out <= 1'b1;
+        [4:5] : out <= 1'b0;
+    endcase
+end
+
+endmodule
diff --git a/tests/verific/range_case.ys b/tests/verific/range_case.ys
new file mode 100644
index 000000000..27afbbc17
--- /dev/null
+++ b/tests/verific/range_case.ys
@@ -0,0 +1,16 @@
+verific -cfg db_abstract_case_statement_synthesis 0
+read -sv range_case.sv
+verific -import top 
+proc
+rename top gold
+
+verific -cfg db_abstract_case_statement_synthesis 1
+read -sv range_case.sv
+verific -import top 
+proc
+rename top gate
+
+miter -equiv -flatten -make_assert gold gate miter
+prep -top miter
+clk2fflogic
+sat -set-init-zero -tempinduct -prove-asserts -verify
diff --git a/tests/verific/run-test.sh b/tests/verific/run-test.sh
new file mode 100755
index 000000000..2f91cf0fd
--- /dev/null
+++ b/tests/verific/run-test.sh
@@ -0,0 +1,4 @@
+#!/usr/bin/env bash
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts --bash