From 6b3d9c608c5c31fc19f5e8a39d4f9d6ce326c2a8 Mon Sep 17 00:00:00 2001
From: Roland Coeurjoly <rolandcoeurjoly@gmail.com>
Date: Mon, 8 Jul 2024 18:29:58 +0200
Subject: [PATCH] Check the existance of a different set of outputs. No need
 for (push 1) nor (pop 1)

---
 .../single_cells/rtlil/multiple_outputs.il    | 69 +++++++++++++++++++
 .../single_cells/vcd_harness_smt.py           | 28 ++++----
 2 files changed, 82 insertions(+), 15 deletions(-)
 create mode 100644 tests/functional/single_cells/rtlil/multiple_outputs.il

diff --git a/tests/functional/single_cells/rtlil/multiple_outputs.il b/tests/functional/single_cells/rtlil/multiple_outputs.il
new file mode 100644
index 00000000000..5e9141a20ad
--- /dev/null
+++ b/tests/functional/single_cells/rtlil/multiple_outputs.il
@@ -0,0 +1,69 @@
+# Generated by Yosys 0.40+7 (git sha1 cc795a3f5, g++ 13.2.0 -Og -fPIC)
+autoidx 5
+attribute \cells_not_processed 1
+attribute \src "multiple_outputs.v:1.1-15.10"
+module \gold
+  attribute \src "multiple_outputs.v:11.12-11.20"
+  wire $and$multiple_outputs.v:11$2_Y
+  attribute \src "multiple_outputs.v:10.12-10.14"
+  wire $not$multiple_outputs.v:10$1_Y
+  attribute \src "multiple_outputs.v:12.12-12.20"
+  wire $or$multiple_outputs.v:12$3_Y
+  attribute \src "multiple_outputs.v:13.12-13.20"
+  wire $xor$multiple_outputs.v:13$4_Y
+  attribute \src "multiple_outputs.v:2.16-2.17"
+  wire input 1 \a
+  attribute \src "multiple_outputs.v:3.17-3.18"
+  wire output 2 \b
+  attribute \src "multiple_outputs.v:4.17-4.18"
+  wire output 3 \c
+  attribute \src "multiple_outputs.v:5.17-5.18"
+  wire output 4 \d
+  attribute \src "multiple_outputs.v:6.17-6.18"
+  wire output 5 \e
+  attribute \src "multiple_outputs.v:11.12-11.20"
+  cell $and $and$multiple_outputs.v:11$2
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 1
+    parameter \B_SIGNED 0
+    parameter \B_WIDTH 1
+    parameter \Y_WIDTH 1
+    connect \A \a
+    connect \B 1'1
+    connect \Y $and$multiple_outputs.v:11$2_Y
+  end
+  attribute \src "multiple_outputs.v:10.12-10.14"
+  cell $not $not$multiple_outputs.v:10$1
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 1
+    parameter \Y_WIDTH 1
+    connect \A \a
+    connect \Y $not$multiple_outputs.v:10$1_Y
+  end
+  attribute \src "multiple_outputs.v:12.12-12.20"
+  cell $or $or$multiple_outputs.v:12$3
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 1
+    parameter \B_SIGNED 0
+    parameter \B_WIDTH 1
+    parameter \Y_WIDTH 1
+    connect \A \a
+    connect \B 1'0
+    connect \Y $or$multiple_outputs.v:12$3_Y
+  end
+  attribute \src "multiple_outputs.v:13.12-13.20"
+  cell $xor $xor$multiple_outputs.v:13$4
+    parameter \A_SIGNED 0
+    parameter \A_WIDTH 1
+    parameter \B_SIGNED 0
+    parameter \B_WIDTH 1
+    parameter \Y_WIDTH 1
+    connect \A \a
+    connect \B 1'1
+    connect \Y $xor$multiple_outputs.v:13$4_Y
+  end
+  connect \b $not$multiple_outputs.v:10$1_Y
+  connect \c $and$multiple_outputs.v:11$2_Y
+  connect \d $or$multiple_outputs.v:12$3_Y
+  connect \e $xor$multiple_outputs.v:13$4_Y
+end
diff --git a/tests/functional/single_cells/vcd_harness_smt.py b/tests/functional/single_cells/vcd_harness_smt.py
index 88973eae0d1..95947748ffe 100644
--- a/tests/functional/single_cells/vcd_harness_smt.py
+++ b/tests/functional/single_cells/vcd_harness_smt.py
@@ -139,9 +139,6 @@ def set_step(inputs, step):
     smt_io.p_close()
     sys.exit(1)
 
-value = smt_io.get(f'(Y test_outputs_step_n0)')
-print(f"  Y: {value}")
-
 # Store signal values
 signals = {name: [] for name in list(inputs.keys()) + list(outputs.keys())}
 # Retrieve and print values for each state
@@ -151,6 +148,8 @@ def hex_to_bin(value):
         bin_value = bin(int(hex_value, 16))[2:]  # Convert to binary and remove the '0b' prefix
         return f'b{bin_value.zfill(len(hex_value) * 4)}'  # Add 'b' prefix and pad with zeros
     return value
+
+combined_assertions = []
 for step in range(num_steps):
     print(f"Values for step {step + 1}:")
     for input_name, width in inputs.items():
@@ -163,18 +162,17 @@ def hex_to_bin(value):
         value = hex_to_bin(value[1:])
         print(f"  {output_name}: {value}")
         signals[output_name].append((step, value))
-        smt_io.write(f'(push 1)')
-        smt_io.write(f'(assert (not (= ({output_name} test_outputs_step_n{step}) #{value})))')
-        result = smt_io.check_sat(["unsat"])
-        if result != 'unsat':
-            smt_io.p_close()
-            sys.exit(1)
-        smt_io.write(f'(pop 1)')
-        result = smt_io.check_sat(["sat"])
-        if result != 'sat':
-            smt_io.p_close()
-            sys.exit(1)
-        
+        combined_assertions.append(f'(= ({output_name} test_outputs_step_n{step}) #{value})')
+# Create a single assertion covering all timesteps
+combined_condition = " ".join(combined_assertions)
+smt_io.write(f'(assert (not (and {combined_condition})))')
+
+# Check the combined assertion
+result = smt_io.check_sat(["unsat"])
+if result != 'unsat':
+    smt_io.p_close()
+    sys.exit(1)
+
 smt_io.p_close()
 
 def write_vcd(filename, signals, timescale='1 ns', date='today'):