Skip to content

v0.3.1 - Formal and Synthesis Evidence Fixes

Choose a tag to compare

@ed766 ed766 released this 15 Jul 20:52

Highlights

  • Fixes the one-way invalid-victim formal assertion so it applies only to the 2-way geometry.
  • Adds passing 1-way and 2-way small-geometry bounded safety evidence at depth 20 under the pinned OSS CAD Suite.
  • Preserves the canonical 5/5 formal result: three nominal safety/reachability tasks plus two expected mutation failures.
  • Replaces an impractical whole-cache Yosys run with an explicitly scoped storage/control geometry proxy for equal-capacity direct-mapped and 2-way comparison.
  • Makes release-check regenerate baseline, edge, and direct-mapped coverage evidence and run the synthesis proxy before associativity reporting.
  • Revalidates 22/22 named tests, 100/100 stress scenarios, 127/127 C++ trace replays, 55/55 interaction crosses, 19/19 coverage-edge cases, 20/20 associativity checks, 7/7 SECDED RAS points, and 4/4 mutation detections.

Yosys, formal, coverage, and performance results remain open-source verification proxies rather than commercial signoff.