4 files changed, 87 insertions, 6 deletions
diff --git a/tests/sat/.gitignore b/tests/sat/.gitignore
index 397b4a762..8355de9dc 100644
--- a/tests/sat/.gitignore
+++ b/tests/sat/.gitignore
@@ -1 +1,2 @@
 *.log
+run-test.mk
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
diff --git a/tests/sat/run-test.sh b/tests/sat/run-test.sh
index 67e1beb23..74589dfeb 100755
--- a/tests/sat/run-test.sh
+++ b/tests/sat/run-test.sh
@@ -1,6 +1,4 @@
-#!/bin/bash
-set -e
-for x in *.ys; do
-	echo "Running $x.."
-	../../yosys -ql ${x%.ys}.log $x
-done
+#!/usr/bin/env bash
+set -eu
+source ../gen-tests-makefile.sh
+run_tests --yosys-scripts
diff --git a/tests/sat/sizebits.sv b/tests/sat/sizebits.sv
index d7ce2326e..87fa08f89 100644
--- a/tests/sat/sizebits.sv
+++ b/tests/sat/sizebits.sv
@@ -1,5 +1,6 @@
 module functions01;
 
+wire t;
 wire [5:2]x;
 wire [3:0]y[2:7];
 wire [3:0]z[7:2][2:9];
@@ -9,24 +10,84 @@ wire [3:0]z[7:2][2:9];
 //wire [$size(y)-1:0]y_size;
 //wire [$size(z)-1:0]z_size;
 
+assert property ($size(t) == 1);
 assert property ($size(x) == 4);
 assert property ($size({3{x}}) == 3*4);
 assert property ($size(y) == 6);
 assert property ($size(y, 1) == 6);
 assert property ($size(y, (1+1)) == 4);
+// This is unsupported at the moment
+//assert property ($size(y[2], 1) == 4);
+//assert property ($size(y[2][1], 1) == 1);
 
 assert property ($size(z) == 6);
 assert property ($size(z, 1) == 6);
 assert property ($size(z, 2) == 8);
 assert property ($size(z, 3) == 4);
+// This is unsupported at the moment
+assert property ($size(z[3], 1) == 8);
+assert property ($size(z[3][3], 1) == 4);
+//assert property ($size(z[3][3][3], 1) == 1);
 // This should trigger an error if enabled (it does).
 //assert property ($size(z, 4) == 4);
 
 //wire [$bits(x)-1:0]x_bits;
 //wire [$bits({x, x})-1:0]xx_bits;
 
+assert property ($bits(t) == 1);
 assert property ($bits(x) == 4);
 assert property ($bits(y) == 4*6);
 assert property ($bits(z) == 4*6*8);
 
+assert property ($high(x) == 5);
+assert property ($high(y) == 7);
+assert property ($high(y, 1) == 7);
+assert property ($high(y, (1+1)) == 3);
+
+assert property ($high(z) == 7);
+assert property ($high(z, 1) == 7);
+assert property ($high(z, 2) == 9);
+assert property ($high(z, 3) == 3);
+assert property ($high(z[3]) == 9);
+assert property ($high(z[3][3]) == 3);
+assert property ($high(z[3], 2) == 3);
+
+assert property ($low(x) == 2);
+assert property ($low(y) == 2);
+assert property ($low(y, 1) == 2);
+assert property ($low(y, (1+1)) == 0);
+
+assert property ($low(z) == 2);
+assert property ($low(z, 1) == 2);
+assert property ($low(z, 2) == 2);
+assert property ($low(z, 3) == 0);
+assert property ($low(z[3]) == 2);
+assert property ($low(z[3][3]) == 0);
+assert property ($low(z[3], 2) == 0);
+
+assert property ($left(x) == 5);
+assert property ($left(y) == 2);
+assert property ($left(y, 1) == 2);
+assert property ($left(y, (1+1)) == 3);
+
+assert property ($left(z) == 7);
+assert property ($left(z, 1) == 7);
+assert property ($left(z, 2) == 2);
+assert property ($left(z, 3) == 3);
+assert property ($left(z[3]) == 2);
+assert property ($left(z[3][3]) == 3);
+assert property ($left(z[3], 2) == 3);
+
+assert property ($right(x) == 2);
+assert property ($right(y) == 7);
+assert property ($right(y, 1) == 7);
+assert property ($right(y, (1+1)) == 0);
+
+assert property ($right(z) == 2);
+assert property ($right(z, 1) == 2);
+assert property ($right(z, 2) == 9);
+assert property ($right(z, 3) == 0);
+assert property ($right(z[3]) == 9);
+assert property ($right(z[3][3]) == 0);
+assert property ($right(z[3], 2) == 0);
 endmodule