mirror of
https://github.com/retroSoC/retroSoC.git
synced 2026-11-04 22:32:36 +00:00
feat(spi): add standalone SPI-P1 core and verification
Implement SPI-P1 from docs/ip/spi.md with a PCLK master, registered APB responses, packed 8x32 TX/RX FIFOs, finite quotas and retained-session abort/recovery. Add the handwritten SVH/C register mirror and private source, credit and GPIO qualification interfaces. Add independent pin timing and data checks, malformed-waveform negatives, FIFO stall/resume and phase-safe abort cases. Provide isolated lint, simulation, compositional formal, synthesis, netlist and observational STA flows with source-bound artifacts and tool-component fingerprints. Validation on the reviewed worktree: 2085 pytest tests passed and one optional pypdf test skipped; both RTL simulators, fresh depth-192 BMC and cover, and ICS55/IHP130 block synthesis and netlist simulation passed. Formatting, style/readiness, Ruff and regression dry-runs passed. SPI remains outside product filelists with DMA capability disabled. SPI-P2/P3 integration, full-product regression closure and physical/IO qualification remain pending; no phase acceptance or policy change.
This commit is contained in:
29 files changed
+3654
No files matched your search
@@ -0,0 +1,496 @@
|
||||
#!/usr/bin/env python3
|
||||
"""Standalone SPI-P1 flows; no product integration or qualification promotion."""
|
||||
from __future__ import annotations
|
||||
|
||||
import argparse
|
||||
import hashlib
|
||||
import json
|
||||
import os
|
||||
import re
|
||||
from pathlib import Path
|
||||
import shutil
|
||||
import subprocess
|
||||
import sys
|
||||
import tarfile
|
||||
|
||||
ROOT = Path(__file__).resolve().parents[1]
|
||||
sys.path.insert(0, str(ROOT))
|
||||
from scripts.check_simulation import DEFAULT_FAILURE # noqa: E402
|
||||
from scripts.setup_helpers import atomic_write # noqa: E402
|
||||
from scripts.yosys_period import period_ps # noqa: E402
|
||||
|
||||
COMMON = ROOT / "rtl/managed/clusterip/common/rtl"
|
||||
IP = ROOT / "rtl/ip/serial"
|
||||
TOP = "apb4_spi_block_top"
|
||||
WRAPPER = ROOT / f"physical/smoke/syn/yosys/{TOP}.sv"
|
||||
SOURCES = [COMMON / "interface/apb4_if.sv", COMMON / "utils/register.sv",
|
||||
ROOT / "rtl/ip/util/soc_common_fifo.sv",
|
||||
*[IP / f"{name}.sv" for name in (
|
||||
"spi_pkg", "spi_ctrl_if", "spi_gpio_guard", "spi_phase_ctrl",
|
||||
"spi_word_packer", "spi_master_core", "spi_reg", "apb4_spi")], WRAPPER]
|
||||
INCLUDES = [COMMON, COMMON / "utils", IP, ROOT / "tests/rtl"]
|
||||
CASES = ("spi_pin_checker_tb", "spi_core_tb", "spi_apb_tb", "spi_lifecycle_tb", "spi_packer_tb")
|
||||
TOOL_INPUT_SCHEMA = 2
|
||||
|
||||
|
||||
def digest(path: Path) -> str:
|
||||
return hashlib.sha256(path.read_bytes()).hexdigest()
|
||||
|
||||
|
||||
def dump(path: Path, data: dict) -> None:
|
||||
atomic_write(path, json.dumps(data, indent=2, sort_keys=True) + "\n")
|
||||
|
||||
|
||||
def inputs() -> dict[str, str]:
|
||||
files = set(SOURCES) | {COMMON / "utils/fifo.sv", COMMON / "config.svh", IP / "spi_define.svh",
|
||||
ROOT / "Makefile", ROOT / "scripts/spi_p1.py", ROOT / "scripts/run_flow.py",
|
||||
ROOT / "scripts/check_simulation.py", ROOT / "dependencies/dependencies.lock.json",
|
||||
ROOT / "docs/ip/spi.md", ROOT / "configs/ci/ics55-tiny.mk",
|
||||
ROOT / "rtl/tiny/integration/clock_reset_domains.json",
|
||||
ROOT / "scripts/bitwuzla_smt2.py", ROOT / "scripts/yosys_period.py",
|
||||
ROOT / "configs/ci/ihp130-tiny.mk", ROOT / "crt/include/retrosoc/hal/spi_regs.h"}
|
||||
for pattern in ("tests/rtl/spi_*", "tests/test_spi*", "physical/smoke/sta/opensta/spi_block.*",
|
||||
"physical/smoke/syn/yosys/script/*"):
|
||||
files.update(ROOT.glob(pattern))
|
||||
return {str(p.relative_to(ROOT)): digest(p) for p in sorted(files) if p.is_file()}
|
||||
|
||||
|
||||
def yosys_json(path: Path) -> dict:
|
||||
"""Remove only Yosys tee timestamp prefixes, preserving the raw artifact."""
|
||||
return json.loads(re.sub(r'^\[\d+\.\d+\]\s?', '', path.read_text(), flags=re.M))
|
||||
|
||||
|
||||
def formal_model_counts(content: str, mode: str) -> dict:
|
||||
counts = {kind: len(re.findall(rf'^; yosys-smt2-{kind}\b', content, re.M))
|
||||
for kind in ('assert', 'assume', 'cover')}
|
||||
required = 'cover' if mode == 'cover' else 'assert'
|
||||
if counts[required] == 0:
|
||||
raise ValueError(f'formal model has no active {required} properties')
|
||||
return counts
|
||||
|
||||
|
||||
def cover_witness_steps(directory: Path, minimum: int = 193) -> int:
|
||||
lengths = [len(json.loads(p.read_text())['steps']) for p in directory.glob('trace*.yw')]
|
||||
if not lengths or max(lengths) < minimum:
|
||||
raise ValueError('formal cover lacks a witness for the complete 192-cycle window')
|
||||
return max(lengths)
|
||||
|
||||
|
||||
def require_pass(content: str, result: dict, marker: str) -> None:
|
||||
if result.get("status") != "passed" or result.get("exit_code") != 0:
|
||||
raise ValueError("command did not pass")
|
||||
if content.count(marker) != 1 or DEFAULT_FAILURE.search(content):
|
||||
raise ValueError("missing/duplicate success or forbidden error marker")
|
||||
|
||||
|
||||
def checked_record(path: Path, source: dict) -> dict:
|
||||
data = json.loads(path.read_text())
|
||||
if data.get('tool_input_schema') != TOOL_INPUT_SCHEMA:
|
||||
raise ValueError(f'incomplete historical tool inventory: {path}')
|
||||
if data.get("status") != "passed" or data.get("source") != source:
|
||||
raise ValueError(f"incomplete or stale SPI evidence: {path}")
|
||||
pdk = data['manifest']['configuration']['PDK']
|
||||
if data.get('external_inputs') != external_inputs(pdk):
|
||||
raise ValueError(f'changed or incomplete SPI tool/input inventory: {path}')
|
||||
for name, value in data["artifacts"].items():
|
||||
if digest(Path(name)) != value:
|
||||
raise ValueError(f"changed SPI artifact: {name}")
|
||||
for name, value in data.get('external_inputs', {}).items():
|
||||
if digest(Path(name)) != value:
|
||||
raise ValueError(f'changed SPI external input: {name}')
|
||||
return data
|
||||
|
||||
|
||||
def execute(directory: Path, name: str, command: list[str], timeout: int = 300,
|
||||
environment: dict | None = None) -> tuple[dict, str]:
|
||||
log, result = directory / f"{name}.log", directory / f"{name}.json"
|
||||
args = [sys.executable, str(ROOT / "scripts/run_flow.py"), "--tool", name,
|
||||
"--log", str(log), "--result", str(result), "--cwd", str(ROOT)]
|
||||
for key, value in (environment or {}).items():
|
||||
args += ["--env", f"{key}={value}"]
|
||||
args += ["--", "timeout", "--foreground", "--kill-after=5s", f"{timeout}s", *command]
|
||||
completed = subprocess.run(args, cwd=ROOT, check=False)
|
||||
data = json.loads(result.read_text())
|
||||
if completed.returncode != 0 or data.get("exit_code") != 0 or data.get('status') != 'passed':
|
||||
raise RuntimeError(f"{name} failed; see {log}")
|
||||
if re.search(r'(?im)^Error:', log.read_text(errors='replace')):
|
||||
raise RuntimeError(f'{name} reported a tool error; see {log}')
|
||||
return data, log.read_text(errors="replace")
|
||||
|
||||
|
||||
def verilator_config(directory: Path) -> str:
|
||||
path = directory / "common.vlt"
|
||||
atomic_write(path, "`verilator_config\n"
|
||||
f'lint_off -rule DECLFILENAME -file "{COMMON}/utils/register.sv"\n'
|
||||
f'lint_off -rule UNUSEDSIGNAL -file "{COMMON}/interface/apb4_if.sv"\n')
|
||||
return str(path)
|
||||
|
||||
|
||||
def simulate(directory: Path, simulator: str, top: str, jobs: int,
|
||||
netlist: Path | None = None, models: list[Path] | None = None) -> None:
|
||||
extra = [ROOT / "tests/rtl/spi_pin_bfm.sv", ROOT / f"tests/rtl/{top}.sv"]
|
||||
defines = [f"-I{p}" for p in INCLUDES]
|
||||
model = directory / top
|
||||
if netlist is not None:
|
||||
adapter = netlist_adapter(netlist, directory)
|
||||
command = ["iverilog", "-g2012", "-gno-specify", "-s", top, "-o", str(model),
|
||||
'-DSPI_DUT=spi_netlist_adapter', *defines,
|
||||
*map(str, (models or []) + [netlist, adapter] + extra)]
|
||||
elif simulator == "VERILATOR":
|
||||
command = ["verilator", "--binary", "--timing", "--timescale", "1ns/1ps",
|
||||
verilator_config(directory), "--assert", "-j", str(jobs),
|
||||
"--top-module", top, "--Mdir", str(directory / f"obj-{top}"),
|
||||
"-o", str(model), *defines, *map(str, SOURCES + extra)]
|
||||
else:
|
||||
converted = directory / f"{top}.v"
|
||||
conversion = subprocess.run(["sv2v", *defines, *map(str, SOURCES + extra)],
|
||||
capture_output=True, text=True, timeout=180, check=False)
|
||||
atomic_write(directory / f"{top}-sv2v.log", conversion.stderr)
|
||||
if conversion.returncode:
|
||||
raise RuntimeError(conversion.stderr)
|
||||
atomic_write(converted, '`timescale 1ns/1ps\n' + conversion.stdout)
|
||||
command = ["iverilog", "-g2012", "-s", top, "-o", str(model), str(converted)]
|
||||
execute(directory, f"{top}-compile", command, environment={"CCACHE_DISABLE": "1"})
|
||||
launch = [str(model)] if simulator == "VERILATOR" and netlist is None else ["vvp", str(model)]
|
||||
result, log = execute(directory, top, launch, timeout=600)
|
||||
require_pass(log, result, f"SPI_P1_PASS {top}")
|
||||
|
||||
|
||||
def synth(directory: Path, pdk: str) -> None:
|
||||
period = period_ps(json.loads((ROOT / 'rtl/tiny/integration/clock_reset_domains.json').read_text()),
|
||||
'peripheral')
|
||||
for name in ("out", "tmp", "rpt"):
|
||||
(directory / name).mkdir()
|
||||
filelist = directory / "source.fl"
|
||||
atomic_write(filelist, "\n".join([*[f"+incdir+{p}" for p in INCLUDES],
|
||||
*map(str, SOURCES)]) + "\n")
|
||||
execute(directory, "yosys", ["yosys", "-t", "--perffile", str(directory / "yosys-perf.json"),
|
||||
"-c", str(ROOT / "physical/smoke/syn/yosys/script/synth.tcl")], 10800, {
|
||||
"PDK": pdk, "SOC": "TINY", "SYNTH_RECIPE": "balanced", "HAVE_SRAM_MACRO": "NO",
|
||||
"YOSYS_TARGET_PERIOD_PS": str(period), "SRAM_SIZE_KIB": '128',
|
||||
"SV_FLIST": str(filelist), "TOP_DESIGN": TOP,
|
||||
"PROJ_NAME": TOP, "WORK": str(directory / "tmp"), "BUILD": str(directory / "out"),
|
||||
"REPORTS": str(directory / "rpt"), "NETLIST": str(directory / "out/netlist.v"),
|
||||
"CONFIG": str(directory / "out/config"), "YOSYS_KEEP_HIER_INST": "",
|
||||
"YOSYS_REPORT_INSTS": "", "YOSYS_FLATTEN_HIER": "1"})
|
||||
mapped = json.loads((directory / 'out/netlist.v.json').read_text())['modules'][TOP]
|
||||
cells = [cell['type'] for cell in mapped['cells'].values()]
|
||||
if any(not (c.startswith('sg13g2_') if pdk == 'IHP130' else c.endswith('H7R')) for c in cells):
|
||||
raise ValueError('foreign, unresolved or macro cell in SPI block netlist')
|
||||
generic = (directory / f'rpt/{TOP}_generic.rpt').read_text()
|
||||
if '$dlatch' in generic.lower() or '$_dlatch' in generic.lower():
|
||||
raise ValueError('SPI inferred latch')
|
||||
check = (directory / f'rpt/{TOP}_synth.rpt').read_text()
|
||||
if 'Found and reported 0 problems.' not in check:
|
||||
raise ValueError('SPI netlist structural check did not pass')
|
||||
memory = yosys_json(directory / f'rpt/{TOP}_pre_memory.json')['modules']
|
||||
fifo_bits = {name: item.get('num_memory_bits', 0) for name, item in memory.items()
|
||||
if 'u_tx_fifo' in name or 'u_rx_fifo' in name}
|
||||
if sorted(fifo_bits.values()) != [256, 256]:
|
||||
raise ValueError(f'SPI FIFO storage mapping differs: {fifo_bits}')
|
||||
area = yosys_json(directory / f'rpt/{TOP}_area.json')['design']['area']
|
||||
dump(directory / 'mapping.json', {'top': TOP, 'pdk': pdk, 'period_ps': period,
|
||||
'cells': len(cells), 'area': area, 'fifo_bits': fifo_bits, 'sram_macros': 0})
|
||||
|
||||
|
||||
def netlist_adapter(netlist: Path, directory: Path) -> Path:
|
||||
ports = json.loads(Path(str(netlist) + '.json').read_text())['modules'][TOP]['ports']
|
||||
groups = {}
|
||||
connections = []
|
||||
for name, value in ports.items():
|
||||
match = re.fullmatch(r'(.*?)(?:__v(\d+)|_(\d+)_|\[(\d+)\])', name)
|
||||
if match:
|
||||
base = match[1]
|
||||
index = int(next(v for v in match.groups()[1:] if v is not None))
|
||||
group = groups.setdefault(base, {'direction': value['direction'], 'indices': []})
|
||||
if group['direction'] != value['direction'] or len(value['bits']) != 1:
|
||||
raise ValueError('invalid split-port direction/width')
|
||||
group['indices'].append(index)
|
||||
target = f'{base}[{index}]'
|
||||
else:
|
||||
base = name
|
||||
groups[base] = {'direction': value['direction'], 'indices': list(range(len(value['bits'])))}
|
||||
target = name
|
||||
escaped = f'\\{name} ' if not re.fullmatch(r'[A-Za-z_]\w*', name) else name
|
||||
connections.append(f'.{escaped}({target})')
|
||||
declarations = []
|
||||
for name, value in groups.items():
|
||||
indices = sorted(value['indices'])
|
||||
if indices != list(range(len(indices))):
|
||||
raise ValueError('noncontiguous split port')
|
||||
width = '' if len(indices) == 1 else f'[{len(indices)-1}:0] '
|
||||
declarations.append(f'{value["direction"]} wire {width}{name}')
|
||||
path = directory / 'adapter.v'
|
||||
atomic_write(path, 'module spi_netlist_adapter(\n' + ',\n'.join(declarations) + ');\n' +
|
||||
f'{TOP} u_mapped(\n' + ',\n'.join(connections) + ');\nendmodule\n')
|
||||
return path
|
||||
|
||||
|
||||
def technology(pdk: str) -> tuple[Path, list[Path]]:
|
||||
if pdk == "ICS55":
|
||||
return (ROOT / ".cache/retrosoc/pdk/ics55/ics55_h7cr_ss.lib",
|
||||
[ROOT / ".cache/retrosoc/pdk/ics55/ics55_h7cr_functional.v"])
|
||||
base = ROOT / "physical/pdk/IHP-Open-PDK/ihp-sg13g2/libs.ref/sg13g2_stdcell"
|
||||
return base / "lib/sg13g2_stdcell_slow_1p08V_125C.lib", [
|
||||
base / "verilog/sg13g2_udp.v", base / "verilog/sg13g2_stdcell.v"]
|
||||
|
||||
|
||||
def tool_path(name: str) -> Path:
|
||||
executable = shutil.which(name)
|
||||
if executable is None:
|
||||
raise ValueError(f'missing SPI tool: {name}')
|
||||
return Path(executable).resolve()
|
||||
|
||||
|
||||
def python_tool_directory(executable: Path, required: tuple[str, ...]) -> Path:
|
||||
"""Resolve the installed search order used by SBY/yosys-smtbmc."""
|
||||
candidates = [executable.parent / 'share/python3',
|
||||
executable.parent.parent / 'share/yosys/python3']
|
||||
# A script-directory module would take precedence over the installed tree.
|
||||
if any((executable.parent / name).exists() for name in required):
|
||||
raise ValueError(f'shadowed Python tool module beside {executable}')
|
||||
selected = next((p for p in candidates if (p / required[0]).is_file()), None)
|
||||
if selected is None or any(not (selected / name).is_file() for name in required):
|
||||
raise ValueError(f'incomplete Python tool installation: {executable}')
|
||||
return selected
|
||||
|
||||
|
||||
def proof_tool_components(executables: dict[str, Path]) -> dict[str, str]:
|
||||
"""Hash the actual helper programs and installed tool data, excluding caches."""
|
||||
yosys = executables['yosys']
|
||||
for name in ('yosys-smtbmc', 'yosys-abc'):
|
||||
if executables[name] != (yosys.parent / name).resolve():
|
||||
raise ValueError(f'mixed Yosys installation: {name}')
|
||||
sby_modules = python_tool_directory(executables['sby'], (
|
||||
'sby_core.py', 'sby_engine_smtbmc.py', 'sby_cmdline.py', 'sby_mode_bmc.py',
|
||||
'sby_mode_cover.py', 'sby_mode_prove.py', 'sby_design.py', 'sby_jobserver.py', 'sby_status.py'))
|
||||
yosys_modules = python_tool_directory(executables['yosys-smtbmc'], ('smtio.py', 'ywio.py'))
|
||||
paths = set(executables.values())
|
||||
for directory in (yosys.parent, yosys.parent.parent / 'share/yosys', sby_modules, yosys_modules):
|
||||
paths.update(p for p in directory.rglob('*') if p.is_file()
|
||||
and '__pycache__' not in p.parts and p.suffix not in ('.pyc', '.pyo'))
|
||||
return {str(p): digest(p) for p in sorted(paths)}
|
||||
|
||||
|
||||
def proof_environment() -> dict[str, str]:
|
||||
# Eliminate user PYTHONPATH/site-module overrides; the scripts append their
|
||||
# fingerprinted installation paths. Keep the active pinned venv interpreter.
|
||||
return {'PYTHONPATH': '', 'PYTHONNOUSERSITE': '1', 'PYTHONDONTWRITEBYTECODE': '1'}
|
||||
|
||||
|
||||
def external_inputs(pdk: str) -> dict[str, str]:
|
||||
slow, models = technology(pdk)
|
||||
typical = Path(str(slow).replace('_ss.lib', '_tt.lib').replace(
|
||||
'_slow_1p08V_125C.lib', '_typ_1p20V_25C.lib'))
|
||||
paths = [slow, typical, *models]
|
||||
if pdk == 'ICS55':
|
||||
paths += [ROOT / '.cache/retrosoc/sources/ics55_ecos_pll/lib/PLL_TOP_typ.lib',
|
||||
ROOT / 'physical/pdk/icsprout55-pdk/IP/IO/ICsprout_55LLULP1233_IO_251013/liberty/ICSIOA_N55_3P3_tt_1p2_3p3_25c.lib']
|
||||
else:
|
||||
paths += [ROOT / 'physical/pdk/IHP-Open-PDK/ihp-sg13g2/libs.ref/sg13g2_io/lib/sg13g2_io_typ_1p2V_3p3V_25C.lib']
|
||||
executables = {name: tool_path(name) for name in (
|
||||
'verilator', 'iverilog', 'vvp', 'sv2v', 'yosys', 'yosys-smtbmc',
|
||||
'yosys-abc', 'sta', 'sby', 'bitwuzla', 'python3')}
|
||||
paths.append(Path(sys.executable).resolve())
|
||||
venv_config = Path(sys.prefix) / 'pyvenv.cfg'
|
||||
if venv_config.is_file():
|
||||
paths.append(venv_config)
|
||||
return {**{str(p): digest(p) for p in paths}, **proof_tool_components(executables)}
|
||||
|
||||
|
||||
def reuse_formal_task(previous: Path, directory: Path, label: str, mode: str,
|
||||
external: dict) -> dict[str, str]:
|
||||
"""Reuse an intact successful subtask, never the failed enclosing campaign."""
|
||||
original = previous / 'record.json'
|
||||
record = json.loads(original.read_text())
|
||||
if record.get('tool_input_schema') != TOOL_INPUT_SCHEMA:
|
||||
raise ValueError('historical proof lacks complete tool-component fingerprints')
|
||||
if record.get('phase') != 'SPI-P1' or record.get('stage') != 'formal':
|
||||
raise ValueError('not SPI-P1 formal evidence')
|
||||
if record.get('external_inputs') != external:
|
||||
raise ValueError('formal tools or external inputs changed')
|
||||
# Driver/Make/test changes may affect orchestration, but never the model,
|
||||
# solver adapter, dependency lock or any other proof-producing source.
|
||||
orchestration = {'Makefile', 'scripts/spi_p1.py', 'tests/test_spi_p1.py'}
|
||||
old_source = {k: v for k, v in record['source'].items() if k not in orchestration}
|
||||
new_source = {k: v for k, v in inputs().items() if k not in orchestration}
|
||||
if old_source != new_source:
|
||||
raise ValueError('formal source inputs changed')
|
||||
artifacts = record['artifacts']
|
||||
required = [previous / f'{label}{suffix}' for suffix in ('.v', '.sby', '.json', '.log')]
|
||||
required += [previous / label / name for name in
|
||||
('status', 'config.sby', 'src/design.v', 'model/design_smt2.smt2')]
|
||||
if any(str(p) not in artifacts for p in required):
|
||||
raise ValueError('formal producer artifact missing from original inventory')
|
||||
for name, value in {**artifacts, **external}.items():
|
||||
if digest(Path(name)) != value:
|
||||
raise ValueError(f'changed formal producer input/artifact: {name}')
|
||||
result = json.loads((previous / f'{label}.json').read_text())
|
||||
if result.get('status') != 'passed' or result.get('exit_code') != 0:
|
||||
raise ValueError('formal subtask command failed')
|
||||
if (previous / label / 'status').read_text().split()[0] != 'PASS':
|
||||
raise ValueError('formal subtask did not pass')
|
||||
model = directory / f'{label}.v'
|
||||
if any(digest(p) != digest(model) for p in
|
||||
(previous / f'{label}.v', previous / label / 'src/design.v')):
|
||||
raise ValueError('formal model differs from actual consumed model')
|
||||
|
||||
def normalized_config(path: Path, design: Path) -> str:
|
||||
content = path.read_text()
|
||||
line = f'design.v {design}\n'
|
||||
if content.count(line) != 1:
|
||||
raise ValueError('unexpected formal model mapping')
|
||||
return content.replace(line, f'design.v SHA256:{digest(design)}\n')
|
||||
|
||||
candidate = normalized_config(directory / f'{label}.sby', model)
|
||||
for config in (previous / f'{label}.sby', previous / label / 'config.sby'):
|
||||
if normalized_config(config, previous / f'{label}.v') != candidate:
|
||||
raise ValueError('formal configuration changed')
|
||||
counts = formal_model_counts((previous / label / 'model/design_smt2.smt2').read_text(), mode)
|
||||
dump(directory / f'{label}-properties.json', counts)
|
||||
dump(directory / f'{label}-reuse.json', {
|
||||
'status': 'passed', 'original_record': str(original), 'original_record_sha256': digest(original),
|
||||
'producer_source': record['source'], 'producer_manifest': record['manifest'],
|
||||
'producer_result': result, 'model_sha256': digest(model),
|
||||
'validation': 'identical consumed model, configuration, inputs and intact artifacts',
|
||||
'phase_accepted': False})
|
||||
return {**artifacts, str(original): digest(original)}
|
||||
|
||||
|
||||
def formal(directory: Path, external: dict, retained: dict,
|
||||
previous: Path | None = None) -> None:
|
||||
sources = SOURCES + [ROOT / "tests/rtl/spi_formal.sv", ROOT / "tests/rtl/spi_formal_props.sv"]
|
||||
solver = shutil.which('bitwuzla')
|
||||
if solver is None:
|
||||
raise ValueError('missing locked Bitwuzla solver')
|
||||
bindir = directory / 'bin'
|
||||
bindir.mkdir()
|
||||
wrapper = bindir / 'bitwuzla'
|
||||
wrapper.symlink_to(ROOT / 'scripts/bitwuzla_smt2.py')
|
||||
for label, mode, depth in [('prove', 'prove', 32), ('register', 'prove', 32),
|
||||
('bmc', 'bmc', 192), ('cover', 'cover', 320)]:
|
||||
defines = [] if mode == 'prove' else ['-DSPI_FORMAL_BOUNDED']
|
||||
if label == 'register':
|
||||
defines = ['-DSPI_FORMAL_REGISTER']
|
||||
converted = subprocess.run(['sv2v', '-E', 'Assert', '-DFORMAL', '-DSV_ASSRT_DISABLE', *defines,
|
||||
*[f'-I{p}' for p in INCLUDES], *map(str, sources)],
|
||||
capture_output=True, text=True, timeout=180, check=True)
|
||||
design = directory / f'{label}.v'
|
||||
for keyword in (('assert', 'cover') if mode == 'cover' else ('assert',)):
|
||||
if not re.search(rf'\b{keyword}\s*\(', converted.stdout):
|
||||
raise ValueError(f'formal conversion removed {keyword} properties')
|
||||
atomic_write(design, converted.stdout)
|
||||
atomic_write(directory / f'{label}-sv2v.log', converted.stderr)
|
||||
config = directory / f'{label}.sby'
|
||||
task_timeout = 1200 if mode == 'bmc' else 600
|
||||
# The mandatory depth-192 cover witnesses satisfiable assumptions for
|
||||
# the whole BMC window; avoid a redundant presat query at every step.
|
||||
engine = 'smtbmc --nopresat bitwuzla' if mode == 'bmc' else 'smtbmc --presat --nounroll bitwuzla'
|
||||
waveform = 'vcd off\n' if mode == 'cover' else ''
|
||||
atomic_write(config, f'[options]\nmode {mode}\ndepth {depth}\ntimeout {task_timeout}\n{waveform}'
|
||||
f'\n[engines]\n{engine}\n\n[script]\n'
|
||||
'read_verilog -formal -sv design.v\nprep -top spi_formal\nasync2sync\ndffunmap\n'
|
||||
f'\n[files]\ndesign.v {design}\n')
|
||||
if previous is not None and mode != 'cover':
|
||||
retained.update(reuse_formal_task(previous, directory, label, mode, external))
|
||||
continue
|
||||
execute(directory, label, [str(tool_path('sby')), '--yosys', str(tool_path('yosys')),
|
||||
'--smtbmc', str(tool_path('yosys-smtbmc')), '--abc', str(tool_path('yosys-abc')),
|
||||
'-d', str(directory / label), str(config)], task_timeout + 60,
|
||||
{**proof_environment(), 'PATH': f'{bindir}:{os.environ["PATH"]}',
|
||||
'RETROSOC_BITWUZLA': solver})
|
||||
if (directory / label / 'status').read_text().split()[0] != 'PASS':
|
||||
raise ValueError(f'formal {mode} did not pass')
|
||||
counts = formal_model_counts((directory / label / 'model/design_smt2.smt2').read_text(), mode)
|
||||
dump(directory / f'{label}-properties.json', counts)
|
||||
if mode == 'cover':
|
||||
steps = cover_witness_steps(directory / mode / 'engine_0')
|
||||
dump(directory / 'nonvacuity.json', {'bmc_depth': 192, 'witness_steps': steps})
|
||||
|
||||
|
||||
def main() -> int:
|
||||
parser = argparse.ArgumentParser(description=__doc__)
|
||||
parser.add_argument("stage", choices=("lint", "rtl", "formal", "synth", "netsim", "sta", "report"))
|
||||
parser.add_argument("--variant-root", type=Path, required=True)
|
||||
parser.add_argument("--pdk", choices=("ICS55", "IHP130"), required=True)
|
||||
parser.add_argument("--simulator", choices=("VERILATOR", "IVERILOG"), default="VERILATOR")
|
||||
parser.add_argument("--jobs", type=int, default=4)
|
||||
parser.add_argument('--common-variant-root', type=Path)
|
||||
parser.add_argument('--formal-reuse-root', type=Path,
|
||||
help='original formal stage; reuse only identical successful subtasks')
|
||||
args = parser.parse_args()
|
||||
variant = args.variant_root.resolve()
|
||||
variant.relative_to(ROOT / "build")
|
||||
manifest = json.loads((variant / "meta/manifest.json").read_text())
|
||||
if manifest["configuration"]["SOC"] != "TINY" or manifest["configuration"]["PDK"] != args.pdk:
|
||||
raise ValueError("profile/PDK mismatch")
|
||||
phase = variant / "meta/spi-p1"
|
||||
suffix = args.stage + (f"-{args.simulator.lower()}" if args.stage == "rtl" else "")
|
||||
directory = phase / suffix
|
||||
source = inputs()
|
||||
retained = {}
|
||||
previous = args.formal_reuse_root.resolve() if args.formal_reuse_root else None
|
||||
if previous is not None:
|
||||
previous.relative_to(ROOT / 'build')
|
||||
if args.stage != 'formal':
|
||||
raise ValueError('formal reuse is valid only for the formal stage')
|
||||
if directory.exists():
|
||||
raise ValueError(f"existing attempt: {directory}; use a fresh timestamp")
|
||||
directory.mkdir(parents=True)
|
||||
record = {"phase": "SPI-P1", "stage": args.stage, "status": "running",
|
||||
'tool_input_schema': TOOL_INPUT_SCHEMA,
|
||||
"source": source, "manifest": manifest, "phase_accepted": False,
|
||||
'external_inputs': external_inputs(args.pdk)}
|
||||
dump(directory / "record.json", record)
|
||||
with tarfile.open(directory / "sources.tar.gz", "w:gz") as archive:
|
||||
for name in source:
|
||||
archive.add(ROOT / name, arcname=name)
|
||||
try:
|
||||
if args.stage == "lint":
|
||||
execute(directory, "lint", ["verilator", "--lint-only", "--Wall",
|
||||
verilator_config(directory), "--top-module", TOP,
|
||||
*[f"-I{p}" for p in INCLUDES], *map(str, SOURCES)])
|
||||
elif args.stage == "rtl":
|
||||
record['cases'] = list(CASES)
|
||||
for top in CASES:
|
||||
simulate(directory, args.simulator, top, args.jobs)
|
||||
elif args.stage == "synth":
|
||||
synth(directory, args.pdk)
|
||||
elif args.stage in ("netsim", "sta"):
|
||||
checked_record(phase / "synth/record.json", source)
|
||||
netlist = phase / "synth/out/netlist.v"
|
||||
liberty, models = technology(args.pdk)
|
||||
if args.stage == "netsim":
|
||||
simulate(directory, "IVERILOG", "spi_netlist_tb", args.jobs, netlist, models)
|
||||
else:
|
||||
execute(directory, "sta", ["sta", "-exit", str(ROOT /
|
||||
"physical/smoke/sta/opensta/spi_block.tcl")], environment={
|
||||
"SPI_NETLIST": str(netlist), "SPI_LIBERTY": str(liberty),
|
||||
"SPI_REPORT_DIR": str(directory)})
|
||||
elif args.stage == "formal":
|
||||
formal(directory, record['external_inputs'], retained, previous)
|
||||
else:
|
||||
common = (args.common_variant_root.resolve() / 'meta/spi-p1'
|
||||
if args.common_variant_root else phase)
|
||||
record["stages"] = {name: checked_record(
|
||||
(common if name in ('lint', 'rtl-verilator', 'rtl-iverilog', 'formal') else phase) /
|
||||
name / 'record.json', source) for name in
|
||||
('lint', 'rtl-verilator', 'rtl-iverilog', 'formal', 'synth', 'netsim', 'sta')}
|
||||
if source != inputs():
|
||||
raise ValueError("source changed during execution")
|
||||
if record['external_inputs'] != external_inputs(args.pdk):
|
||||
raise ValueError('external SPI inputs changed during execution')
|
||||
record["status"] = "passed"
|
||||
except (OSError, ValueError, RuntimeError, subprocess.SubprocessError) as error:
|
||||
record.update(status="failed", error=str(error))
|
||||
print(error, file=sys.stderr)
|
||||
return 1
|
||||
finally:
|
||||
record["artifacts"] = {**retained, **{str(p): digest(p) for p in directory.rglob("*")
|
||||
if p.is_file() and p.name != "record.json"}}
|
||||
dump(directory / "record.json", record)
|
||||
return 0
|
||||
|
||||
|
||||
if __name__ == "__main__":
|
||||
raise SystemExit(main())
|
||||
Reference in new issue
Block a user