Formal equiv diff sat_alu.v

[alaindargelas]

Test yosys/tests/sat/alu.v ./run_formal_verif.sh test=sat_alu.v

Trimmed down test show the problem in the plugin:

This test fails as the implicit typespec of the parameter ALU_OP_SHR is a int_typespec with a range. It is not an array typespec, but somehow the plugin thinks it is an array. It is an int with a limited range of 4 bits.

module alu(
	input clk,
	input [7:0] A,
	input [3:0] operation,
    output reg [8:0] tmp
);
	localparam /*logic [3:0]*/ ALU_OP_SHR = 4'b1001;
	always @(posedge clk)
	begin
		case (operation)
			ALU_OP_SHR :
				tmp = { A[0], 1'b0, A[7:1]};
		endcase
	end
endmodule

This test pass as the explicit typespec is a logic_typespec with a range of 4 bits:

module alu(
	input clk,
	input [7:0] A,
	input [3:0] operation,
    output reg [8:0] tmp
);
	localparam logic [3:0]  ALU_OP_SHR = 4'b1001;
	always @(posedge clk)
	begin
		case (operation)
			ALU_OP_SHR :
				tmp = { A[0], 1'b0, A[7:1]};
		endcase
	end
endmodule