mirror of
https://github.com/retroSoC/retroSoC.git
synced 2026-11-04 22:32:36 +00:00
maksyuki
e6b9a9f43d
- Introduced for deterministic corpus framing, CRC checks, and regression evidence for NPU-P6. - Added to validate NPU-P6 reference execution. - Created a new RTL model for gate-level NPU transactions. - Updated to instantiate and streamline the testbench. - Enhanced with capability checks and added NPU-P6 reference contract tests. - Modified to include in the source list and refactor rejection logic. - Updated README.md to document new test scripts and their purposes.
99 lines
3.7 KiB
Python
99 lines
3.7 KiB
Python
#!/usr/bin/env python3
|
|
"""Assemble the bounded NPU-P6 formal closure report."""
|
|
|
|
from __future__ import annotations
|
|
|
|
import argparse
|
|
import hashlib
|
|
import json
|
|
import re
|
|
import subprocess
|
|
from pathlib import Path
|
|
|
|
|
|
ROOT = Path(__file__).resolve().parents[1]
|
|
TARGETS = ("npu_dma", "npu_context", "npu_control")
|
|
|
|
|
|
def identity(path: Path) -> dict[str, object]:
|
|
data = path.read_bytes()
|
|
return {"path": str(path.resolve()), "bytes": len(data), "sha256": hashlib.sha256(data).hexdigest()}
|
|
|
|
|
|
def task(target_dir: Path, name: str) -> dict[str, object]:
|
|
status_path = target_dir / name / "status"
|
|
result_path = target_dir / f"result-{name}.json"
|
|
config_path = target_dir / f"{name}.sby"
|
|
if status_path.read_text(encoding="utf-8").split()[0] != "PASS":
|
|
raise ValueError(f"formal task failed: {status_path}")
|
|
result = json.loads(result_path.read_text(encoding="utf-8"))
|
|
if result.get("status") != "passed" or result.get("exit_code") != 0:
|
|
raise ValueError(f"formal structured result failed: {result_path}")
|
|
config = config_path.read_text(encoding="utf-8")
|
|
depth_match = re.search(r"(?m)^depth\s+(\d+)$", config)
|
|
mode_match = re.search(r"(?m)^mode\s+(\w+)$", config)
|
|
if depth_match is None or mode_match is None:
|
|
raise ValueError(f"formal task lacks mode/depth: {config_path}")
|
|
return {
|
|
"mode": mode_match.group(1),
|
|
"depth": int(depth_match.group(1)),
|
|
"status": "PASS",
|
|
"result": identity(result_path),
|
|
"log": identity(target_dir / f"{name}.log"),
|
|
"config": identity(config_path),
|
|
}
|
|
|
|
|
|
def main() -> int:
|
|
parser = argparse.ArgumentParser(description=__doc__)
|
|
parser.add_argument("--formal-dir", type=Path, required=True)
|
|
parser.add_argument("--output", type=Path, required=True)
|
|
args = parser.parse_args()
|
|
records = {}
|
|
for target in TARGETS:
|
|
target_dir = args.formal_dir / target
|
|
records[target] = {
|
|
"prove": task(target_dir, "prove"),
|
|
"cover": task(target_dir, "cover"),
|
|
}
|
|
report = {
|
|
"schema": 1,
|
|
"phase": "NPU-P6",
|
|
"verification_ids": ["NPU-V015"],
|
|
"git_revision": subprocess.check_output(
|
|
["git", "-C", str(ROOT), "rev-parse", "HEAD"], text=True
|
|
).strip(),
|
|
"scope": {
|
|
"npu_dma": "AXI accepted-transfer conservation and bounded pause/flush safety",
|
|
"npu_context": "two-context ownership, backpressure and exactly-once 64-beat drain",
|
|
"npu_control": "launch/result/snapshot mailbox and lifecycle reconciliation",
|
|
},
|
|
"assumptions": {
|
|
"liveness": "no unbounded liveness claim",
|
|
"environment": "bounded responder stalls and explicitly modeled mailbox consumers",
|
|
},
|
|
"implementation": {
|
|
name: identity(ROOT / name)
|
|
for name in (
|
|
"scripts/npu_p6_formal_report.py",
|
|
"rtl/mini/formal/generate_formal_filelist.py",
|
|
"rtl/mini/formal/npu_context_formal.sv",
|
|
"rtl/mini/formal/npu_context_formal_props.sv",
|
|
"rtl/mini/formal/npu_control_formal.sv",
|
|
"rtl/mini/formal/npu_control_formal_props.sv",
|
|
"rtl/mini/mk/formal.mk",
|
|
)
|
|
},
|
|
"targets": records,
|
|
"summary": {"required_tasks": 6, "passes": 6, "failures": 0, "skipped": 0},
|
|
"verdict": "PASS",
|
|
}
|
|
args.output.parent.mkdir(parents=True, exist_ok=True)
|
|
args.output.write_text(json.dumps(report, indent=2, sort_keys=True) + "\n", encoding="utf-8")
|
|
print(f"NPU-P6 formal closure: PASS ({args.output})")
|
|
return 0
|
|
|
|
|
|
if __name__ == "__main__":
|
|
raise SystemExit(main())
|