From 8206951f77a95f0d7818d98aaf3e577a7aff5fae Mon Sep 17 00:00:00 2001
From: George Rennie <georgerennie@gmail.com>
Date: Wed, 28 Aug 2024 16:24:47 +0100
Subject: [PATCH] proc_dff: add tests

---
 tests/proc/proc_dff.ys | 80 ++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 80 insertions(+)
 create mode 100644 tests/proc/proc_dff.ys

diff --git a/tests/proc/proc_dff.ys b/tests/proc/proc_dff.ys
new file mode 100644
index 000000000..1b719da36
--- /dev/null
+++ b/tests/proc/proc_dff.ys
@@ -0,0 +1,80 @@
+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