yosys/tests/proc/proc_dff.ys

read_verilog -formal <<EOT
// From https://github.com/YosysHQ/yosys/pull/4568#issuecomment-2313740948

module top(input clk, a, b, c, input [1:0] d, output reg [1:0] q);

always @(posedge clk, posedge a, posedge b, posedge c) begin
	if      (a) q <= '0;
	else if (b) q <= 2'b10;
	else if (c) q <= '0;
	else        q <= d;
end

always @* begin
	if      (a) assert(q == '0);
	else if (b) assert(q == 2'b10);
	else if (c) assert(q == '0);
end

endmodule
EOT

proc
select -assert-count 1 t:$dffsr
clk2fflogic
select -assert-count 3 t:$assert
sat -tempinduct -verify -prove-asserts

design -reset

read_verilog -formal <<EOT
// Tests aload combined with reset. The aload gets refactored into the set/reset
// logic
module top(input clk, rst, aload_n, input [1:0] l, d, output reg [1:0] q);

always @(posedge clk, posedge rst, negedge aload_n) begin
	if      (rst)      q <= '0;
	else if (!aload_n) q <= l;
	else               q <= d;
end

always @* begin
	if      (rst)      assert(q == '0);
	else if (!aload_n) assert(q == l);
end

endmodule
EOT

proc
select -assert-count 1 t:$dffsr
clk2fflogic
select -assert-count 2 t:$assert
sat -tempinduct -verify -prove-asserts

design -reset

read_verilog -formal <<EOT
// Tests combining of common reset signals
module top(input clk, rst_a, rst_b, rst_c, input [1:0] d, output reg [1:0] q);

always @(posedge clk, posedge rst_a, posedge rst_b, negedge rst_c) begin
	if      (rst_a)  q <= '1;
	else if (rst_b)  q <= '1;
	else if (!rst_c) q <= '1;
	else             q <= d;
end

always @* if (rst_a || rst_b || !rst_c) assert(q == '1);

endmodule

EOT

proc
select -assert-count 1 t:$adff
clk2fflogic
select -assert-count 1 t:$assert
sat -tempinduct -verify -prove-asserts

design -reset