Merge pull request #3674 from YosysHQ/fix_wide_case

8 files changed, 123 insertions, 14 deletions

diff --git a/Makefile b/Makefile
index 43b90355b..645b5103f 100644
--- a/Makefile
+++ b/Makefile
@@ -837,6 +837,9 @@ ABCOPT=""
 endif
 
 test: $(TARGETS) $(EXTRA_TARGETS)
+ifeq ($(ENABLE_VERIFIC),1)
+	+cd tests/verific && bash run-test.sh $(SEEDOPT)
+endif
 	+cd tests/simple && bash run-test.sh $(SEEDOPT)
 	+cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT)
 	+cd tests/hana && bash run-test.sh $(SEEDOPT)
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index c1e9fc7d0..ab3e55427 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1043,21 +1043,49 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 		sw->signal = sig_select;
 		current_case->switches.push_back(sw);
 
-		int select_width = inst->InputSize();
-		int data_width = inst->OutputSize();
-		int select_num = inst->Input1Size() / inst->InputSize();
-
-		int offset_select = 0;
-		int offset_data = 0;
-
-		for (int i = 0; i < select_num; i++) {
-			RTLIL::CaseRule *cs = new RTLIL::CaseRule;
-			cs->compare.push_back(sig_select_values.extract(offset_select, select_width));
-			cs->actions.push_back(SigSig(sig_out_val, sig_data_values.extract(offset_data, data_width)));
-			sw->cases.push_back(cs);
-			
-			offset_select += select_width;
+		unsigned select_width = inst->InputSize();
+		unsigned data_width = inst->OutputSize();
+		unsigned offset_data = 0;
+		unsigned offset_select = 0;
+
+		OperWideCaseSelector* selector = (OperWideCaseSelector*) inst->View();
+
+		for (unsigned i = 0 ; i < selector->GetNumBranches() ; ++i) {
+
+			SigSig action(sig_out_val, sig_data_values.extract(offset_data, data_width));
 			offset_data += data_width;
+
+			for (unsigned j = 0 ; j < selector->GetNumConditions(i) ; ++j) {
+				Array left_bound, right_bound ;
+				selector->GetCondition(i, j, &left_bound, &right_bound);
+			
+				SigSpec sel_left = sig_select_values.extract(offset_select, select_width);
+				offset_select += select_width;
+
+				if (right_bound.Size()) {
+					SigSpec sel_right = sig_select_values.extract(offset_select, select_width);
+					offset_select += select_width;
+
+					log_assert(sel_right.is_fully_const() && sel_right.is_fully_def());
+					log_assert(sel_left.is_fully_const() && sel_right.is_fully_def());
+
+					int32_t left = sel_left.as_int();
+					int32_t right = sel_right.as_int();
+					int width = sel_left.size();
+
+					for (int32_t i = right; i<left; i++) {
+						RTLIL::CaseRule *cs = new RTLIL::CaseRule;
+						cs->compare.push_back(RTLIL::Const(i,width));
+						cs->actions.push_back(action);
+						sw->cases.push_back(cs);
+					}
+				}
+
+				RTLIL::CaseRule *cs = new RTLIL::CaseRule;
+				cs->compare.push_back(sel_left);
+				cs->actions.push_back(action);
+				sw->cases.push_back(cs);
+			}
 		}
 		RTLIL::CaseRule *cs_default = new RTLIL::CaseRule;
 		cs_default->actions.push_back(SigSig(sig_out_val, sig_data_default));
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