riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Check that there are not other solutions other than the first given

This commit is contained in:
Roland Coeurjoly 2024-07-04 12:35:00 +02:00 committed by Emily Schmidt
parent cb5f08364c
commit 73ed514623
1 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
tests/functional/single_cells/vcd_harness_smt.py
View File

@ -41,7 +41,7 @@ parsed_results = []
# Load and execute the SMT file
with open(smt_file_path, 'r') as smt_file:
for line in smt_file:
smt_io.write(line.strip())
smt_io.write(line.strip())
smt_io.check_sat()
# Read and parse the SMT file line by line
with open(smt_file_path, 'r') as smt_file:
@ -161,6 +161,17 @@ for step in range(num_steps):
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)
smt_io.p_close()