´SMT success only if simulation is equivalent

This commit is contained in:
Roland Coeurjoly 2024-07-03 17:07:50 +02:00 committed by Emily Schmidt
parent 9700df50d6
commit cb5f08364c
2 changed files with 4 additions and 1 deletions

View File

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

View File

@ -133,6 +133,9 @@ for command in smt_commands:
# 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)