Added ranged case check

This commit is contained in:
Miodrag Milanovic 2023-02-23 15:04:31 +01:00
parent 53a4f0fb56
commit d8cefec169
2 changed files with 27 additions and 0 deletions

View File

@ -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

View File

@ -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