From 73e45d29d699d4894fcd0f4739744290a7a04373 Mon Sep 17 00:00:00 2001
From: Gary Wong <gtw@gnu.org>
Date: Sat, 24 May 2025 08:32:58 -0600
Subject: [PATCH] Add semantic test cases for SystemVerilog
 priority/unique/unique0 "if".

The tests/verilog/*_if_enc.ys scripts instantiate simple encoder
modules, both with and without the SystemVerilog priority/unique/unique0
keywords, and check for consistency between the two for the subset
of inputs where the priority/unique/unique0 "if" result is
well-defined.

These tests vacuously succeed at the moment, since priority/unique
keywords are silently ignored and therefore the generated logic is
trivially identical.  But the test cases will be capable of detecting
certain types of unsound optimisation if priority/unique handling is
introduced later.
---
 tests/verilog/priority_if_enc.ys | 41 ++++++++++++++++++++++++++++++++
 tests/verilog/unique0_if_enc.ys  | 41 ++++++++++++++++++++++++++++++++
 tests/verilog/unique_if_enc.ys   | 41 ++++++++++++++++++++++++++++++++
 3 files changed, 123 insertions(+)
 create mode 100644 tests/verilog/priority_if_enc.ys
 create mode 100644 tests/verilog/unique0_if_enc.ys
 create mode 100644 tests/verilog/unique_if_enc.ys

diff --git a/tests/verilog/priority_if_enc.ys b/tests/verilog/priority_if_enc.ys
new file mode 100644
index 000000000..7ca09cad7
--- /dev/null
+++ b/tests/verilog/priority_if_enc.ys
@@ -0,0 +1,41 @@
+logger -expect log "SAT proof finished - no model found: SUCCESS" 1
+
+read_verilog -sv <<EOF
+// A somewhat contrived model of an encoder, relying on SystemVerilog's
+// strong "if" semantics to guarantee priority encoder behaviour.
+module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// Almost the same thing, but by using "priority if" we introduce
+// "don't care" states, essentially conveying permission to synthesise
+// a simple encoder instead.
+module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        priority if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// A simple test bench to detect mismatches between the two encoders.
+module compare_encoders( input [ 2:0 ] x, output ok );
+    wire [ 1:0 ] encout;
+    wire [ 1:0 ] dutout;
+    encoder e( x, encout );
+    dut d( x, dutout );
+    // The "priority if" above assumes $countones( x ) > 0.
+    assign ok = encout == dutout || !$countones( x );
+endmodule
+EOF
+
+synth -flatten -top compare_encoders
+sat -prove ok 1
diff --git a/tests/verilog/unique0_if_enc.ys b/tests/verilog/unique0_if_enc.ys
new file mode 100644
index 000000000..e0384067d
--- /dev/null
+++ b/tests/verilog/unique0_if_enc.ys
@@ -0,0 +1,41 @@
+logger -expect log "SAT proof finished - no model found: SUCCESS" 1
+
+read_verilog -sv <<EOF
+// A somewhat contrived model of an encoder, relying on SystemVerilog's
+// strong "if" semantics to guarantee priority encoder behaviour.
+module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// Almost the same thing, but by using "unique0 if" we introduce
+// "don't care" states, essentially conveying permission to synthesise
+// a simple encoder instead.
+module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        unique0 if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// A simple test bench to detect mismatches between the two encoders.
+module compare_encoders( input [ 2:0 ] x, output ok );
+    wire [ 1:0 ] encout;
+    wire [ 1:0 ] dutout;
+    encoder e( x, encout );
+    dut d( x, dutout );
+    // The "unique0 if" above assumes $onehot0( x ).
+    assign ok = encout == dutout || !$onehot0( x );
+endmodule
+EOF
+
+synth -flatten -top compare_encoders
+sat -prove ok 1
diff --git a/tests/verilog/unique_if_enc.ys b/tests/verilog/unique_if_enc.ys
new file mode 100644
index 000000000..c188d84fe
--- /dev/null
+++ b/tests/verilog/unique_if_enc.ys
@@ -0,0 +1,41 @@
+logger -expect log "SAT proof finished - no model found: SUCCESS" 1
+
+read_verilog -sv <<EOF
+// A somewhat contrived model of an encoder, relying on SystemVerilog's
+// strong "if" semantics to guarantee priority encoder behaviour.
+module encoder( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// Almost the same thing, but by using "unique if" we introduce
+// "don't care" states, essentially conveying permission to synthesise
+// a simple encoder instead.
+module dut( input [ 2:0 ] x, output reg [ 1:0 ] y );
+    always_comb begin
+        y = 2'b00;
+
+        unique if( x[ 2 ] ) y = 2'b11;
+        else if( x[ 1 ] ) y = 2'b10;
+        else if( x[ 0 ] ) y = 2'b01;
+    end
+endmodule
+
+// A simple test bench to detect mismatches between the two encoders.
+module compare_encoders( input [ 2:0 ] x, output ok );
+    wire [ 1:0 ] encout;
+    wire [ 1:0 ] dutout;
+    encoder e( x, encout );
+    dut d( x, dutout );
+    // The "unique if" above assumes $onehot( x ).
+    assign ok = encout == dutout || !$onehot( x );
+endmodule
+EOF
+
+synth -flatten -top compare_encoders
+sat -prove ok 1