ila

An internal logic analyzer with AXI4-Lite CSRs for FPGA and ASIC — an embedded debug core in the SignalTap / Xilinx-ILA mold, but open, tiny and bus-controlled: watch up to 128 signal bits, trigger on a masked compare (level / rising-edge / forced) with a programmable pre-trigger window, then read the captured waveform back over AXI4-Lite from a CPU, a debug bridge, or a crossbar port.

Plain synthesizable SystemVerilog, verified by self-checking Verilator testbenches plus SymbiYosys formal proofs, with registers single-sourced from gen/regmap.py and packaged as vendor-neutral IP-XACT 1685-2014.

Design spec: docs/spec.md · register map: docs/registers.md (generated).

Features

PROBE_W ≤ 128 probe bits sampled every aclk into a circular BRAM buffer (DEPTH rows, power of 2)
trigger: (probe & TMASK) == (TVAL & TMASK), level or rising-edge-of-match, plus force-trigger; all-zero mask = capture-anything
programmable pre-trigger position: POS pre-samples guaranteed, then exactly DEPTH-1-POS post-samples — classic windowing
status: armed / triggered / done / wrapped; WP/TPTR pointers + RDIDX/RDATA* readout; INFO geometry register for host discovery
probes must be synchronous to aclk (synchronize async signals before probing — an ILA that samples metastable inputs lies to you)

Status

Area	State
RTL	✅ lint `-Wall`-clean
TB	✅ `ILA P 0000` — level/edge/forced triggers, exact windowing incl. POS 0 and DEPTH−1, ring wrap, full-buffer counter-consecutiveness, readback, disarm
Coverage	✅ 98.9% rtl/ (86/87; the miss is an unreachable defensive FSM `default`)
Formal	✅ F_cap proven (pointer/status structural invariants — in range, frozen when done, done⇒triggered, triggered-from-armed — DEPTH 8/32, unbounded abc pdr) + F_rd bounded-checked (smtbmc bitwuzla, depth 20 = one full capture+readback cycle, exhaustive over all inputs: exact post-window count `DEPTH-1-POS` + shadow-memory readout integrity; both also simulation-covered). `make formal`
IP-XACT	✅ schema-validated (ipxact/), full memory map
Integration	✅ `ILAX P 0000` — capture + readout through `../xbar`'s crossbar incl. DECERR (`make sim-xbar`)
OOC	✅ timing closed on `xc7a100t-1` (Vivado 2026.1), 32×1024 config: 312 LUT / 416 FF / 1 BRAM, WNS +3.07 ns @ 10 ns → Fmax ≈ 144 MHz (the buffer infers block RAM — kept in a reset-less process deliberately)

make lint       # Verilator -Wall, clean
make sim        # CSR-driven regression -> "ILA P 0000"
make sim-xbar   # behind the crossbar (needs ../xbar) -> "ILAX P 0000"
make coverage   # merged line coverage, rtl/ only
make formal     # F_cap + F_rd (SymbiYosys, abc pdr)
make ipxact     # vendor-neutral IEEE 1685-2014 package
make synth-ooc  # Vivado out-of-context synth+impl, timing-gated

Layout

rtl/     core/capture.sv (trigger + ring buffer), bus/axil_regs.sv,
         ila_axil.sv (top)
tb/      tb_ila.sv, tb_ila_xbar.sv (integration), shared AXI tasks
formal/  ila_cap.sby + ila_cap_fv.v (yosys-dialect harness; DUT sv2v'd)
docs/    spec.md, registers.md (generated)
gen/     regmap.py (single source of truth), ipxact_gen.py

Features

Status

Layout

License