openXC7: a DSP48E1 fed from the fabric produces a wrong bitstream (40-line reproducer)

[github-actions]

Re-filed from #2149. An attempt claimed that issue on 2026-09-24 and left an empty branch, and a dispatch row that has spent its retry ceiling keeps its issue for good - so no bee could take it again, however much the brief improved. The work below is carried over unchanged.

---

The defect

On the openXC7 flow (yosys -> nextpnr-xilinx -> prjxray), a DSP48E1 whose operands come from the fabric produces a bitstream that computes the wrong answer. Constants work; live signals do not.

Minimal reproducer, ~40 lines: fpga/verilog/dsp_probe.v (constant operands, passes) and fpga/verilog/dsp_probe_live.v (LFSR operands, fails). -nodsp blocks inference but keeps an explicit instance, so one bitstream carries a raw DSP and a LUT-built reference of the same product and the die compares them.

build	simulation	silicon	DSP48E1
constant operands, USE_DPORT("FALSE")	pass	PASS	1
constant operands, USE_DPORT("TRUE") + pre-adder	pass	PASS	1
live operands from an LFSR	pass	FAIL	1

Three QMTech XC7A200T-FGG676 boards, five stable reads per build, every read bracketed with a wrong-part bitstream so Done went 0 -> 1.

What is ruled out

• The RTL -- passes behavioural simulation.
• yosys -- its DSP-mapped netlist passes gate-level simulation against yosys's own xilinx/cells_sim.v DSP48E1 model.
• "the operating mode never reaches the bitstream" -- OPMODE, ALUMODE, INMODE and the register controls are all in the FASM; prjxray models the tile with 436 segbits.
• "the D-port pre-adder is at fault" -- a probe with USE_DPORT("TRUE") passes, duplicated USE_DPORT[0] FASM line and all. That duplicate is harmless.

What remains

Routing of data into the DSP48E1 input pins: nextpnr-xilinx, or prjxray's model of those pips. Separating them needs a reference bitstream (Vivado), which this host does not have.

Why this matters here

Every FPGA claim in this repository is built through openXC7. Any design that feeds a DSP from the fabric is exposed. The workaround is -nodsp, and it is not free -- measured in docs/reports/GFT-NODSP-COST-W727.md: a 1-DSP multiplier goes 47 -> 236 LUT; a 12-DSP dot product goes 1673 -> 6000.

Full write-up: docs/reports/TRINET-DSP-DEFECT-W723.md. Downstream report: gHashTag/tri-net#381.

Theorems T246, T249, T250 in docs/theory/IGLA-FORMAL-RESULTS.md.

Original file list

• fpga/verilog/dsp_probe.v
• fpga/verilog/dsp_probe_live.v

The instruments

Every one of these reads and prints; none of them writes. Run them from the repository root, with <spec> replaced by the file in ## Boundary:

.t27 is not Rust and not Zig, and a bee fluent in either writes one by
accident. Measured 2026-09-20: a bee filled eight bodies in
specs/file/watcher.t27 with return Ok(());, Err(FileError::WatcherNotFound)
and for i in 0..watchers.length. The parse ratchet refused the whole file --
Unexpected token in expression: RParen, line 123 -- and a spec that does not
parse generates nothing, so every test it already carried stopped running.

At the top level the parser accepts exactly these eight forms, with an optional
pub, and no others:

const   var   fn   enum   struct   test   invariant   bench

There is no trait, no impl, no type X = ..., no generics, no macro. What
a bee reaches for from another language, and what happens:

• Rust's result sugar (Ok(()), Err(E::V), ?) is not a construct here.
• Rust macros (println!, format!, vec!) are not constructs here.
• A range loop (for i in 0..n) is Rust and Zig, not this language.
• Zig builtins (catch unreachable, @intCast, @constCast) are not constructs here.
• Cross-module reuse (use other::fn;) parses and then generates a comment and an unqualified call, so the Zig fails with use of undeclared identifier (use a::b; generates no import, so no spec can reuse a function from another spec #4298). It does not work yet.

t27c parse <spec> answers in one line whether what you wrote is the language.
Run it before you report, every time.

• t27c spec-status <spec> - the compiler's one-word verdict: IMPLEMENTED, PARTIAL, UNWRITTEN, NOPARSE, NOFN. Exit code is 0 whatever it says, so read the word.
• t27c symbols <spec> - every name the file declares, with its kind. Answers "does this already exist here?" before you add it.
• t27c outline <spec> - per function: its locals, what it calls, what it returns. The contract you are implementing against.
• t27c coverage <spec> - which functions have a test and which do not. The issue asks for tests; this is how you check you wrote them.
• t27c lint <spec> - style and shape warnings. It OVER-REPORTS has no test or invariant: measured 2026-09-20 over 60 specs it printed 677 of those where coverage found 190 untested functions, disagreeing on 59 of the 60 - it warns about bit_to_trit_pair in specs/base/ternary_encoding.t27, which test bit_to_trit_pair_zero calls on line 249. Read it as a hint; coverage is the answer.
• t27c typecheck <spec> - types, before generation. Prints Typecheck OK (0 errors, 0 warnings) or the errors.
• t27c test-report <spec> - builds this spec and runs its own tests, which is what the oracle does. BLOCKED means the generated Zig does not compile, with the error beside it.
• python3 tools/dupe_scan.py --name <function> - where that function already lives, if it does. 576 of 4021 bodies here are byte-identical copies.

The rest of the toolbelt is in docs/BEE_TOOLBELT.md.

---

Queen-runnable restatement (2026-10-05)

The root cause sits in nextpnr-xilinx or prjxray (other repositories) and separating them needs a Vivado reference bitstream, which no bee has; the two reproducers are already t27 specs on master (specs/port/fpga/verilog/dsp_probe.t27, specs/port/fpga/verilog/dsp_probe_live.t27, #5113). What a bee can still do in t27 is record the measured result as a rule the flow can consult: which DSP48E1 builds are trusted on openXC7 and when -nodsp is required, pinned by tests, so the knowledge stops living only in a report.

Boundary

• specs/fpga/openxc7_dsp_fabric.t27

User Scenarios & Testing

• Given master, where the DSP48E1 fabric-operand defect is described only in docs/reports/TRINET-DSP-DEFECT-W723.md, when specs/fpga/openxc7_dsp_fabric.t27 lands, then the three measured builds of the table above (constant operands, constant operands with the D-port pre-adder, live LFSR operands) and the decision "a DSP48E1 whose operands come from the fabric needs -nodsp on openXC7" are stated in t27 and checked by tests.

Requirements

• FR-001: The spec MUST declare fn silicon_passes(operands_from_fabric: bool, use_dport: bool) -> bool that reproduces the measured table: true for constant operands with or without the D-port, false for live fabric operands.
• FR-002: The spec MUST declare fn needs_nodsp(operands_from_fabric: bool) -> bool, true exactly when the operands come from the fabric, with a test for each case.
• FR-003: The spec MUST NOT claim the root cause; it records only what was measured (comment cites the report and tri-net#381).
• FR-004: The change MUST NOT add or modify non-t27 hand-written code (specs/policy/own_language.t27).

Success Criteria

• grep -cE '^[[:space:]]*(pub )?fn (silicon_passes|needs_nodsp)\(' specs/fpga/openxc7_dsp_fabric.t27 prints 2
• grep -cE '^[[:space:]]*test[[:space:]]+[A-Za-z_]' specs/fpga/openxc7_dsp_fabric.t27 prints at least 3
• t27c spec-status specs/fpga/openxc7_dsp_fabric.t27 prints IMPLEMENTED
• t27c test-report specs/fpga/openxc7_dsp_fabric.t27 2>&1 | grep -c BLOCKED prints 0