admin/retroSoC
1
0 Fork 0
mirror of https://github.com/retroSoC/retroSoC.git synced 2026-11-06 14:55:14 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: add BMC timeout for opipsram in formal.mk and corresponding test

Browse Source
This commit is contained in:
maksyuki committed 2026-09-02 08:01:54 +08:00
1 parent e0796271da
commit 63284cc913
3 files changed
+18 -3
Download Patch File Download Diff File Expand all files Collapse all files

No files matched your search

tests/test_script_tools.py
+10
View File
@@ -423,6 +423,16 @@ def test_formal_filelists_are_scoped_to_the_protocol_duts(tmp_path: Path) -> Non
assert ROOT / "rtl/mini/formal/opipsram_formal.sv" in opipsram.files
def test_opipsram_formal_keeps_full_depth_with_hosted_runner_budget() -> None:
formal_makefile = (ROOT / "rtl/mini/mk/formal.mk").read_text(encoding="utf-8")
assert re.search(r"^FORMAL_OPIPSRAM_DEPTH\s+\?= 40$", formal_makefile, re.MULTILINE)
assert re.search(r"^FORMAL_OPIPSRAM_BMC_DEPTH\s+\?= 40$", formal_makefile, re.MULTILINE)
assert re.search(r"^FORMAL_OPIPSRAM_TIMEOUT\s+\?= 300$", formal_makefile, re.MULTILINE)
assert re.search(r"^FORMAL_OPIPSRAM_BMC_TIMEOUT\s+\?= 600$", formal_makefile, re.MULTILINE)
assert "$(FORMAL_OPIPSRAM_BMC_TIMEOUT)s $(FORMAL_SBY)" in formal_makefile
def test_sysctrl_formal_properties_use_exported_user_core_shape() -> None:
design = (ROOT / "rtl/mini/formal/sysctrl_formal.sv").read_text(encoding="utf-8")
properties = (ROOT / "rtl/mini/formal/sysctrl_formal_props.sv").read_text(encoding="utf-8")