From 0c6d0d4b5dc7c0b19bcca3f63a95b97a9df703d9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Marcelina=20Ko=C5=9Bcielnicka?= <mwk@0x04.net>
Date: Mon, 20 Jul 2020 22:49:30 +0200
Subject: satgen: Add support for dffe, sdff, sdffe, sdffce cells.

---
 tests/sat/dff.ys | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)
 create mode 100644 tests/sat/dff.ys

(limited to 'tests/sat')

diff --git a/tests/sat/dff.ys b/tests/sat/dff.ys
new file mode 100644
index 000000000..ba3625871
--- /dev/null
+++ b/tests/sat/dff.ys
@@ -0,0 +1,21 @@
+# Ensure all sync-only DFFs have usable SAT models.
+
+read_verilog -icells <<EOT
+
+module top(...);
+
+input C, D, R, E;
+output [4:0] Q;
+
+\$dff #(.WIDTH(1), .CLK_POLARITY(1'b1)) ff0 (.CLK(C), .D(D), .Q(Q[0]));
+\$dffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .EN_POLARITY(1'b1)) ff1 (.CLK(C), .D(D), .EN(E), .Q(Q[1]));
+\$sdff #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0)) ff2 (.CLK(C), .D(D), .SRST(R), .Q(Q[2]));
+\$sdffe #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff3 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[3]));
+\$sdffce #(.WIDTH(1), .CLK_POLARITY(1'b1), .SRST_POLARITY(1'b1), .SRST_VALUE(1'b0), .EN_POLARITY(1'b1)) ff4 (.CLK(C), .D(D), .EN(E), .SRST(R), .Q(Q[4]));
+
+endmodule
+
+EOT
+
+# This ensures that 1) coarse cells have SAT models, 2) fine cells have SAT models, 3) they're equivalent
+equiv_opt -assert simplemap
-- 
cgit v1.2.3