Tiny Exchange Trader

Hello! I started this project in another life, when I was a quant trading intern. I'd learned about FPGA engineering and was fascinated, so I tried it out myself! I made further improvements recently and uploaded it to Github. This is Tiny Exchange Trader, a small hardware trading system that studies safe decisions when market data arrives damaged, late, duplicated, or out of order.

A toy exchange publishes byte streams to a SystemVerilog trader. A fault layer attacks those streams. The circuit must notice lost trust, recover cleanly, and keep account state conservative.

*Codex assisted in the write-up of this project.

This replay comes from the RTL. The exchange drops one message. The circuit marks its book stale, stops trading, requests a snapshot, and returns to live operation after the snapshot is accepted.

Core idea

The project separates three commitments that are easy to blur together:

• A sequence gap invalidates the market book. A tokenized snapshot restores it.
• A reset makes the local position UNCERTAIN. An account baseline restores it.
• An authorized order is irrevocable. Backpressure may stall its bytes, but the circuit cannot retract them.

These rules turn a small threshold strategy into a useful state-machine problem. The arithmetic is simple. Trust, recovery, and event ordering carry the interesting work.

System map

flowchart LR
    EX[Exchange ledger] --> FL[Fault layer]
    FL -->|market bytes| RX[Ingress FIFO and receiver]
    RX --> MS[Market trust and recovery]
    MS --> ST[Strategy and risk]
    ST -->|authorization| TX[Order serializer]
    TX -->|order bytes| EX
    EX -->|execution bytes| AC[Account state]
    AC --> ST
    OR[Wire oracle and reference model] -. checks packets, state, and timing .-> RX
    OR -.-> MS
    OR -.-> AC

Loading

The exchange owns the real book and position. Fault injection happens after publication, so a dropped packet still changes the exchange ledger. Recovery traffic and execution reports travel through the same hostile link.

The wire protocol is called tinyx-v1. It has a fixed big-endian header, fixed message lengths, and CRC-32. docs/protocol.md gives the byte-level contract.

Measured results

The current release evidence is sealed to the source, design configuration, and toolchain. The release checker rejects mismatched or stale artifacts.

Check	Result
Python unit tests	201 passed
Hypothesis state machines	2 passed
Cross-backend comparisons	200 / 200 passed
Deliberate RTL mutants	12 / 12 caught
Formal tasks	13 / 13 resolved
Frozen chaos runs	800 / 800 passed
Frozen throughput runs	360 / 360 passed
Cross-configuration runs	254 / 254 applicable runs passed
ECP5 routes at 25 MHz	20 / 20 met timing

All sixteen runtime properties reached their enabling conditions. docs/results.md contains the generated tables. docs/progress.md records the release evidence and commands.

Receiver study

The design includes two receiver architectures.

• PARSER=0 stores a frame, then makes a separate CRC pass.
• PARSER=1 computes CRC per byte through a four-byte delay pipeline.

Their sustained-load behavior is stark.

At zero inter-frame gap, the buffered receiver accepts about half a byte per clock. Its 64-entry ingress FIFO overflows 5,340 times across fifteen runs and authorizes zero orders. A 256-entry FIFO delays the cliff, yet it still authorizes only nine orders.

The streaming receiver accepts about one byte per clock. It parses every frame in the same workload and never overflows at either FIFO depth.

This result is the main architectural lesson. Buffer depth helps with bursts. Receiver service rate controls sustained capacity.

The campaigns found one RTL bug and six verification-path bugs. Each fix has a small reproducer and a regression test.

Area	Example
RTL receiver	One byte carried SOP and EOP in the middle of a frame. It represented two damaged frames, while both receivers reported only one.
Reference model	A recovery deadline counted its handshake clock and expired one cycle early.
Harness and scoreboard	Reset residue, barrier ordering, same-cycle event order, post-edge sampling, and cleared pairing state each produced a false answer.

The ratio is useful. Verification code deserves the same suspicion as the hardware it judges. docs/bugs.md keeps the full debugging journal.

Verification stack

Each layer has a narrow job:

• The Python reference model tracks the protocol contract clock by clock.
• A wire oracle reconstructs packets from accepted bytes without consulting the receiver.
• Packet accounting requires every accepted frame to produce exactly one event or fault.
• Cocotb and a persistent Verilator harness run the same scenarios against the RTL.
• Hypothesis explores long state-machine histories.
• Planted mutants check whether named detectors react to known RTL defects.
• SymbiYosys checks FIFO ordering, admission control, and serializer stability.
• Yosys and nextpnr produce routed ECP5 measurements for four configurations.

Hardware study

This hardware work is an implementation study. No hardware board was used. The open-source ECP5 flow compares both receivers at FIFO depths 64 and 256. Five routing seeds are recorded for each configuration.

The four configurations use 6,014 to 9,024 LUT4 equivalents. Their routed maximum clock rates span 38.13 to 46.70 MHz. Every frozen route meets the common 25 MHz target.

An earlier 50 MHz target missed timing and remains in the historical record. docs/implementation.md explains the critical path and the single revision made after that result.

Local run

The bootstrap script installs a pinned Python environment and open-source HDL toolchain. macOS and Linux are supported.

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

The complete frozen study is resumable:

make freeze-bench
make check-benchmark-config
make chaos SPLIT=final MATRIX=required DRIVER=native LINK_MODE=1
make bench SUITE=throughput DRIVER=native
make implement
make parse-reports
make summarize
make plots
make check-report
make check-release

make reproduce runs the full release pipeline in one command. The recorded run took 74 minutes on the development machine. Saved results are reused only when their source, toolchain, contract, configuration, driver, and expanded scenario hashes match.

Repository guide

Path	Contents
rtl/	Synthesizable SystemVerilog
tinyx/	Protocol, exchange, reference model, oracle, and scenario engine
tb/	Cocotb module and integration tests
sim/	Persistent Verilator harness
formal/	SymbiYosys harnesses
scenarios/	Directed cases and minimized campaign failures
tools/	Campaign, measurement, plotting, and release commands
benchmarks/	Frozen workloads and route matrix
results/	Recorded evidence used by the reports
docs/	Protocol, design, results, bugs, and implementation notes

Reading list

• docs/design.md covers the architecture and verification strategy.
• docs/results.md contains every generated measurement.
• docs/bugs.md records failures, reductions, and fixes.
• docs/replays.md shows six RTL traces as animated replays.
• docs/understanding.md explains the central design decisions.
• docs/formal.md states the formal assumptions and bounds.
• docs/implementation.md covers synthesis and routing.
• docs/toolchain.md lists exact tool versions and licenses.

Scope

This project covers one instrument, a compact protocol, and a threshold rule used to exercise the control path. It has no board measurements, power claims, profitability claims, order-book depth, cancel-and-replace flow, or multi-venue model.

The formal checks have explicit bounds and assumptions. The campaign results describe a frozen synthetic workload. They provide repeatable evidence for this design and this toolchain.