mirror of
https://github.com/YosysHQ/yosys
synced 2026-05-22 18:09:41 +00:00
Fix functional tests
This commit is contained in:
parent
15e09163cd
commit
2b3f4c37f5
2 changed files with 5 additions and 2 deletions
|
|
@ -5,10 +5,12 @@ YOSYS ?= $(BUILD_DIR)/yosys
|
||||||
ABC ?= $(BUILD_DIR)/yosys-abc
|
ABC ?= $(BUILD_DIR)/yosys-abc
|
||||||
YOSYS_FILTERLIB ?= $(BUILD_DIR)/yosys-filterlib
|
YOSYS_FILTERLIB ?= $(BUILD_DIR)/yosys-filterlib
|
||||||
YOSYS_CONFIG ?= $(BUILD_DIR)/yosys-config
|
YOSYS_CONFIG ?= $(BUILD_DIR)/yosys-config
|
||||||
|
YOSYS_SMTBMC ?= $(BUILD_DIR)/yosys-smtbmc
|
||||||
YOSYS_MAX_THREADS ?= 4
|
YOSYS_MAX_THREADS ?= 4
|
||||||
|
|
||||||
export YOSYS
|
export YOSYS
|
||||||
export YOSYS_CONFIG
|
export YOSYS_CONFIG
|
||||||
|
export YOSYS_SMTBMC
|
||||||
export ABC
|
export ABC
|
||||||
export YOSYS_MAX_THREADS
|
export YOSYS_MAX_THREADS
|
||||||
|
|
||||||
|
|
|
||||||
|
|
@ -1,3 +1,4 @@
|
||||||
|
import os
|
||||||
import json
|
import json
|
||||||
import shutil
|
import shutil
|
||||||
import subprocess
|
import subprocess
|
||||||
|
|
@ -21,7 +22,7 @@ def write_smt2(tmp_path, verilog_text):
|
||||||
vfile = tmp_path / "design.v"
|
vfile = tmp_path / "design.v"
|
||||||
smt2 = tmp_path / "design.smt2"
|
smt2 = tmp_path / "design.smt2"
|
||||||
vfile.write_text(verilog_text)
|
vfile.write_text(verilog_text)
|
||||||
run([base_path / "yosys", "-Q", "-p",
|
run([os.environ.get("YOSYS", "../../yosys"), "-Q", "-p",
|
||||||
f"read_verilog {vfile}; prep -top top; write_smt2 {smt2}"])
|
f"read_verilog {vfile}; prep -top top; write_smt2 {smt2}"])
|
||||||
return smt2
|
return smt2
|
||||||
|
|
||||||
|
|
@ -61,7 +62,7 @@ def write_yw(yw_path, signals, bits):
|
||||||
def run_smtbmc(smt2_path, yw_path):
|
def run_smtbmc(smt2_path, yw_path):
|
||||||
"""Run yosys-smtbmc on the SMT2 file with a witness trace."""
|
"""Run yosys-smtbmc on the SMT2 file with a witness trace."""
|
||||||
cmd = [
|
cmd = [
|
||||||
base_path / "yosys-smtbmc",
|
os.environ.get("YOSYS_SMTBMC", "../../yosys-smtbmc"),
|
||||||
"-s", "z3",
|
"-s", "z3",
|
||||||
"-m", "top",
|
"-m", "top",
|
||||||
"--check-witness",
|
"--check-witness",
|
||||||
|
|
|
||||||
Loading…
Add table
Add a link
Reference in a new issue