´SMT success only if simulation is equivalent

Author: RCoeurjoly

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."
 

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)