Skip to content

progress.md

Latest commit

 

History

History
109 lines (76 loc) · 5.34 KB

progress.md

File metadata and controls

109 lines (76 loc) · 5.34 KB
Raw

Release ledger

This page is the compact build record for Tiny Exchange Trader. Generated measurements live in results.md. Debugging notes live in bugs.md.

Current evidence

Every artifact records a source hash, design hash, toolchain identity, and protocol contract. The aggregation and release tools compare those fields before accepting a result.

Evidence Recorded result
Unit tests 201 passed
Hypothesis state machines 2 passed
RTL parser and link combinations 4 passed
Cocotb and native comparisons 200 / 200 matched
Planted mutants 12 / 12 caught
Formal tasks 13 / 13 resolved
Frozen chaos runs 800 / 800 passed
Frozen throughput runs 360 / 360 passed
Applicable configuration runs 254 / 254 passed
Frozen routes at 25 MHz 20 / 20 met timing
RTL replay clips 6 generated
Report figures 6 generated
Fresh-checkout steps 27 / 27 passed

The release check reads the underlying JSON and CSV files. This table is a guide for readers, not an independent source of truth.

Build history

Stage Result
Protocol Defined tinyx-v1, generated the RTL constants, and pinned codec fixtures.
Reference system Built the exchange, fault layer, account model, market model, scenario engine, and wire oracle.
RTL baseline Added frame parsing, market recovery, account reconciliation, risk checks, and order serialization.
Native simulation Added a persistent Verilator harness for long campaigns.
Fault campaigns Split development, validation, and frozen final seeds. Added failure reduction and replay.
Receiver comparison Added buffered and streaming parsers behind the same event contract.
Formal checks Proved small FIFO instances and bounded the admission and serializer properties.
Implementation Synthesized and routed four ECP5 configurations across five seeds each.
Release Added sealed evidence checks, fresh-checkout reproduction, report audits, and CI.

Frozen workloads

benchmarks/config.json fixes four hardware configurations, route seeds 1 through 5, a 25 MHz target, 200 final chaos seeds, and 360 throughput runs. benchmarks/throughput_seeds.json stores the market messages and congestion offsets.

The throughput schedule assigns every message to an absolute clock. Each run records any drift from that plan. The maximum observed drift was eight clocks.

Development, validation, and final seeds are disjoint. The final split uses seeds 3000 through 3199. Every expanded scenario is hashed, so a generator change invalidates saved jobs even when the master seed stays the same.

Campaign findings

The final campaigns exposed three defects before passing:

Area Defect Regression
RTL A nested SOP that also carried EOP produced two damaged frames, while the receivers queued one fault. C45_nested_sop_that_is_also_eop
Reference model The recovery timeout expired one clock early. C44_reply_deadline_boundary
Native scoreboard Reset cleared fault-pairing state before the abandoned span arrived. C46_fault_at_the_reset_barrier

Earlier generated runs found four more verification-path defects. They involved partial-frame reset residue, delayed frames surviving a barrier, same-cycle fault ordering, and post-edge token sampling. Cases C37 through C40 preserve those failures.

Every listed case fails when its fix is reverted. bugs.md contains the timelines and reductions.

Formal scope

The SymbiYosys suite contains thirteen tasks.

  • FIFO occupancy, output stability, and ordering use induction at capacities 2, 4, and 8.
  • Admission control uses the real risk_check and account_state modules with free semantic events. Its bounded depth is 64.
  • Serializer stability and framing use a bounded depth of 64. The completed-frame cover task uses depth 100.

All tasks resolved. The production FIFO depths remain outside the direct induction instances. formal.md lists each assumption and reduction.

Implementation record

The frozen implementation matrix contains four parser and FIFO configurations. Each configuration has five routed seeds at 25 MHz. All twenty routes meet timing. Routed maximum clock rates span 38.13 to 46.70 MHz.

The earlier 50 MHz experiment missed timing. Its reports remain available as historical evidence. One revision split comparisons around the 32-by-32-bit notional product. The product stayed full width. Mutation M11 and the risk boundary sweep protect that decision.

Reproduction

Use the short checks while editing:

make lint
make lint-rtl
make test-python
make test-stateful
make test-rtl-matrix
make test-backend-equivalence-matrix COUNT=50

Run the complete release pipeline with:

make reproduce
make check-release

The recorded full reproduction took 74 minutes on the development machine. It completed 33 stages, including seven commands from a fresh checkout.

Release gate

tools/check_release.py checks toolchain setup, properties, campaigns, mutants, formal tasks, the hardware matrix, backend equivalence, liveness, replays, report artifacts, licensing, fresh-checkout reproduction, and observed CI.

Run it directly for a detailed ledger:

bash scripts/env.sh python tools/check_release.py