From c3fbdc609ddef9cbddfdadaeb6ffb56beffc127f Mon Sep 17 00:00:00 2001 From: Roland Coeurjoly Date: Wed, 3 Jul 2024 17:07:50 +0200 Subject: [PATCH] =?UTF-8?q?=C2=B4SMT=20success=20only=20if=20simulation=20?= =?UTF-8?q?is=20equivalent?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- tests/functional/single_cells/run-test.sh | 1 - tests/functional/single_cells/vcd_harness_smt.py | 4 ++++ 2 files changed, 4 insertions(+), 1 deletion(-) diff --git a/tests/functional/single_cells/run-test.sh b/tests/functional/single_cells/run-test.sh index 67358639bf2..11ff1b5ce0b 100755 --- a/tests/functional/single_cells/run-test.sh +++ b/tests/functional/single_cells/run-test.sh @@ -54,7 +54,6 @@ run_smt_test() { # TODO: which SMT solver should be run? if z3 "${base_name}.smt2"; then echo "SMT file ${base_name}.smt2 is valid ." - smt_successful_files["$rtlil_file"]="Success" if python3 vcd_harness_smt.py "${base_name}.smt2"; then echo "Python script generated VCD file for $rtlil_file successfully." diff --git a/tests/functional/single_cells/vcd_harness_smt.py b/tests/functional/single_cells/vcd_harness_smt.py index a44bf4570c9..5d8c735a6c1 100644 --- a/tests/functional/single_cells/vcd_harness_smt.py +++ b/tests/functional/single_cells/vcd_harness_smt.py @@ -133,6 +133,9 @@ def set_step(inputs, step): # smt_io.setup() result = smt_io.check_sat() print(f'SAT result: {result}') +if result != 'sat': + smt_io.p_close() + sys.exit(1) value = smt_io.get(f'(Y test_outputs_step_n0)') print(f" Y: {value}") @@ -197,3 +200,4 @@ def write_vcd(filename, signals, timescale='1 ns', date='today'): # Write the VCD file write_vcd(smt_file_path + '.vcd', signals) +sys.exit(0)