Merge branch 'main' into nella/latch-toggle

tests/proc/proc_dlatch.ys

@@ -0,0 +1,133 @@
+read_verilog -formal <<EOT
+module top(input g, rn, d, output reg q);
+	always @* if (~rn) q <= 0; else if (g) q <= d;
+	always @* begin
+		if      (~rn) assert(q == 0);
+		else if (g)   assert(q == d);
+	end
+endmodule
+EOT
+
+proc
+select -assert-count 1 t:$adlatch
+select -assert-count 0 t:$dlatch
+select -assert-count 0 t:$dlatchsr
+
+simplemap
+select -assert-count 1 t:$_DLATCH_PN0_
+clk2fflogic
+sat -tempinduct -verify -prove-asserts
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input gn, rn, d, output reg q);
+	always @* if (rn==0) q <= 0; else if (gn==0) q <= d;
+	always @* begin
+		if      (rn==0)  assert(q == 0);
+		else if (gn==0)  assert(q == d);
+	end
+endmodule
+EOT
+
+proc
+select -assert-count 1 t:$adlatch
+simplemap
+select -assert-count 1 t:$_DLATCH_NN0_
+clk2fflogic
+sat -tempinduct -verify -prove-asserts
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input g, sn, d, output reg q);
+	always @* if (~sn) q <= 1; else if (g) q <= d;
+	always @* begin
+		if      (~sn) assert(q == 1);
+		else if (g)   assert(q == d);
+	end
+endmodule
+EOT
+
+proc
+select -assert-count 1 t:$adlatch
+simplemap
+select -assert-count 1 t:$_DLATCH_PN1_
+clk2fflogic
+sat -tempinduct -verify -prove-asserts
+
+design -reset
+
+read_verilog -formal <<EOT
+module top(input g, sn, rn, d, output reg q);
+	always @* if (~rn) q <= 0; else if (~sn) q <= 1; else if (g) q <= d;
+	always @* begin
+		if      (~rn) assert(q == 0);
+		else if (~sn) assert(q == 1);
+		else if (g)   assert(q == d);
+	end
+endmodule
+EOT
+
+proc
+select -assert-count 0 t:$adlatch
+select -assert-count 0 t:$dlatchsr
+select -assert-count 1 t:$dlatch
+clk2fflogic
+sat -tempinduct -verify -prove-asserts
+
+design -reset
+
+read_verilog <<EOT
+module top(input g, d, output reg q);
+	always @* if (g) q <= d;
+endmodule
+EOT
+
+proc
+select -assert-count 1 t:$dlatch
+select -assert-count 0 t:$adlatch
+
+design -reset
+
+read_verilog -formal <<EOT
+module gold(input g, rn, d, zero, output reg q);
+	always @* if (~rn | g) q <= (~rn ? zero : d);
+	always @* assume(zero == 1'b0);
+endmodule
+module gate(input g, rn, d, zero, output reg q);
+	always @* if (~rn) q <= 1'b0; else if (g) q <= d;
+endmodule
+EOT
+
+proc
+select -assert-count 1 -module gold t:$dlatch
+select -assert-count 1 -module gate t:$adlatch
+select -clear
+equiv_make gold gate equiv
+hierarchy -top equiv
+clk2fflogic
+equiv_induct -set-assumes
+equiv_status -assert
+
+design -reset
+
+read_verilog -formal <<EOT
+module gold(input g, sn, d, one, output reg q);
+	always @* if (~sn | g) q <= (~sn ? one : d);
+	always @* assume(one == 1'b1);
+endmodule
+module gate(input g, sn, d, one, output reg q);
+	always @* if (~sn) q <= 1'b1; else if (g) q <= d;
+endmodule
+EOT
+
+proc
+select -assert-count 1 -module gold t:$dlatch
+select -assert-count 1 -module gate t:$adlatch
+select -clear
+equiv_make gold gate equiv
+hierarchy -top equiv
+clk2fflogic
+equiv_induct -set-assumes
+equiv_status -assert

tests/proc/rmdead_case_x.ys

@@ -0,0 +1,40 @@
+# https://github.com/YosysHQ/yosys/issues/5979
+
+read_verilog -sv << EOF
+module top (
+	input wire [1:0] sel,
+	input wire [3:0] a,
+	input wire [3:0] b,
+	output reg [3:0] y
+);
+	always @* begin
+		case (sel)
+			2'b1x: y = a;
+			2'b10: y = b;
+			default: y = a;
+		endcase
+	end
+endmodule
+
+module gold (
+	input wire [1:0] sel,
+	input wire [3:0] a,
+	input wire [3:0] b,
+	output reg [3:0] y
+);
+	always @* begin
+		if (sel == 2'b10) y = b;
+		else y = a;
+	end
+endmodule
+EOF
+
+proc
+opt -full
+
+select -assert-count 1 top/o:y %ci* top/i:b %i
+
+equiv_make gold top equiv
+cd equiv
+equiv_simple
+equiv_status -assert

tests/proc/yosys_latch.sv

@@ -0,0 +1,11 @@
+module yosys_latch (
+	input logic dlatch_p_d, input logic dlatch_p_g, output logic dlatch_p_q,
+	input logic dlatch_n_d, input logic dlatch_n_gn, output logic dlatch_n_q,
+	input logic dlatch_pn0_d, input logic dlatch_pn0_rn, input logic dlatch_pn0_g, output logic dlatch_pn0_q,
+	input logic dlatch_nn0_d, input logic dlatch_nn0_rn, input logic dlatch_nn0_gn, output logic dlatch_nn0_q
+);
+	always_latch if (dlatch_p_g) dlatch_p_q <= dlatch_p_d;
+	always_latch if (~dlatch_n_gn) dlatch_n_q <= dlatch_n_d;
+	always_latch if (~dlatch_pn0_rn) dlatch_pn0_q <= 1'b0; else if (dlatch_pn0_g) dlatch_pn0_q <= dlatch_pn0_d;
+	always @* if (dlatch_nn0_rn == 1'b0) dlatch_nn0_q <= 1'b0; else if (dlatch_nn0_gn == 1'b0) dlatch_nn0_q <= dlatch_nn0_d;
+endmodule

tests/proc/yosys_latch.ys

@@ -0,0 +1,20 @@
+# https://github.com/YosysHQ/yosys/issues/5910
+
+read_verilog -sv yosys_latch.sv
+hierarchy -check -top yosys_latch
+proc
+design -save gold
+opt
+select -assert-count 2 t:$adlatch
+select -assert-count 2 t:$dlatch
+simplemap
+opt_clean
+select -assert-count 1 t:$_DLATCH_P_
+select -assert-count 1 t:$_DLATCH_N_
+select -assert-count 1 t:$_DLATCH_PN0_
+select -assert-count 1 t:$_DLATCH_NN0_
+select -assert-count 4 t:*
+design -load gold
+equiv_opt -assert -multiclock simplemap
+
+design -reset