Merge pull request #3674 from YosysHQ/fix_wide_case

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)

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();
+		unsigned select_width = inst->InputSize();
+		unsigned data_width = inst->OutputSize();
+		unsigned offset_data = 0;
+		unsigned offset_select = 0;
 
-		int offset_select = 0;
-		int offset_data = 0;
+		OperWideCaseSelector* selector = (OperWideCaseSelector*) inst->View();
 
-		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;
+		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));

tests/verific/.gitignore

@@ -0,0 +1,3 @@
+/*.log
+/*.out
+/run-test.mk

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
+

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

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

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

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