Integrate qualified PR #24 packetized LSC-1 onto main#26
Conversation
- Minimal 25 MHz counter/LED smoke_top + LPF (v3.1.8 pin-subset hypothesis) - UART RX/TX at 1 Mbaud, 2-flop sync, framing error handling - uart_bridge.sv: exact lean_silicon_lsc1 instantiation, byte buffering, POR, backpressure - New driver: fpga_harness/ulx3s_uart.py (explicit --port only) - Icarus TB skeleton: test/tb_uart_bridge.sv - SRAM-only build scripts; explicit prohibition of -f documented - Real yosys/nextpnr/ecppack run; 291.97 MHz post-route; bitstream SHA captured Ownership: PR #13 (host runtime), PR #15 (board_detect/SHA256SUMS) untouched. Worktree: fpga/ulx3s-smoke-uart-mincore @ 03926bb [skip ci] sprint deliverable
- Exact commands, tool versions, timing (291.97 MHz smoke / 160.26 MHz bridge) - Bitstream SHAs recorded - SRAM-only openFPGALoader recipe with explicit -f prohibition - Supported MinCore transaction list - Bounded claims only; no hardware execution evidence [skip ci]
Every response byte was being corrupted or lost on the way to the host, and none of the checked-in verification could see it. RTL: - uart_tx released tx_ready at bit_cnt == 8, so data bit 7 lasted one 25 MHz clock instead of a full baud interval. A receiver sampled every zero-valued bit 7 as one (a SET echo of 00 arrived as 80). Ready now releases at 9. - The bridge's power-on "synchroniser" only ever shifted in ones, so rst_n was never low and no register in the bridge or the core was ever initialised. The core latched x into its error state and answered nothing. Replaced with a zero-initialised shift register that genuinely holds reset for 8 edges. - Both handshake directions now use a one-deep skid buffer whose ready deasserts on the handshake that fills it. Previously RX_VALID was pulsed against a ready sampled a cycle early (dropping bytes that arrived mid transaction) and TX_READY mirrored the serialiser a cycle late (letting the core hand over a second byte that overwrote the first). - Added a sticky rx_overrun probe that drives no logic, so the bench can assert no byte was ever displaced. Verification: - Replaced the tb_uart_bridge liveness window with a real 1 Mbaud 8N1 receiver. It fails on a missing byte, a short final bit, a bad stop bit, a wrong or extra byte, and on rx_overrun, across STATUS, SET, XOR, MUL, unknown opcode and abort recovery. Wired it into `make sim`, which previously never ran it. - ulx3s_uart.py --tx mul printed the board's reply and exited 0 whatever it was. It now computes the expected GF(2^128) product with both independent oracles in sim/model.py, cross-checks them, and gates the exit status. Added tests that feed complete but wrong 16-byte responses and require exit 1. Build and evidence: - build_smoke.sh and build_uart.sh resolved sources and output through one ".." too many, so the bridge build could not find any RTL and evidence landed outside the repository. Both now resolve the repository root from their own location and archive artefacts under the names the manifests use. - Committed the executable bit so `make -C fpga/ulx3s smoke` runs, and pointed the uart target at build_uart.sh instead of an echo. - The LPF had no frequency constraint, so a "25 MHz" claim was really nextpnr's 12 MHz default. Constrained it; both designs still close (291.97 / 154.37 MHz). - results/ SHA256SUMS named smoke.bit for a file archived as ulx3s_smoke.bit, so the integrity check could not run. The scripts now emit and self-verify both manifests. Regenerated ulx3s_bridge.bit from the repaired RTL; the digest is reproducible across three independent builds. - .gitignore's blanket *.log dropped the synthesis and route logs the manifest promised. Exempted the results directory and archived them. Not addressed by design: 0x7f still cannot appear as a payload byte, since the bridge treats it as an abort before command framing. Escaping it would change the wire protocol. Documented as a limitation instead.
status is the default --tx, and it was the only command whose reply was printed without being checked. A misbuilt bridge emitting four arbitrary bytes passed the default board-smoke invocation with exit 0, so the check that is supposed to catch a broken build was the one command that could not fail. Compare against 01 01 0f 08 and exit 1 on mismatch, matching how set, xor and mul already gate their exit status. A test parses status_byte() out of leanvm_b_stream_alu.sv so the host constant cannot drift from the RTL.
The usage example shipped `--tx 03`, the SET128 opcode byte, but argparse only accepts command names. The first command a new user copies exited 2 before opening the port, so the documented entry point never worked. Point the example at `--tx set` and give a status example alongside it. PAYLOAD_BYTES now backs both the argparse choices and the width check, so the accepted commands and their payload widths cannot drift apart. Guarded by tests that pull every `python3 -m fpga_harness.ulx3s_uart` line out of the module docstring and ULX3S_SMOKE_AND_UART.md, parse each one, and check the payload width matches the command.
uart_bridge.sv derives its abort pulse from any received 0x7f, not only from one in command position, so a 0x7f inside an operand tears the transaction down mid-flight. Reproduced in simulation: a SET128 whose payload byte 5 is 0x7f comes back as 15 bytes with 0xe0 from byte 5 on. 128-bit operands are arbitrary data, so ordinary vectors reach this -- about 6% of random SET payloads and 12% of random XOR/MUL operand pairs. Previously the host printed MATCH: False and exited 1, which is the exit status for "the board answered wrong" and points an investigation at the silicon instead of the link. Reject such operands up front and exit 2, and write the limitation down as an open bridge design question rather than an LSC-1 property. The ASIC takes ABORT on uio_in[6], a pin, and has no in-band abort byte, so this is the bridge's framing to settle. No RTL is changed here, so the committed bitstreams and their checksums still describe the shipped gates.
pyserial applies the timeout set in open_port to every individual read, so threading args.timeout into recv_exact bounded each read rather than the call. A byte landing just before the deadline bought the read after it a whole fresh timeout. Measured against a virtual clock, a 2.00 s budget took 3.90 s: one byte at t=1.9 s, then a second read that blocked the full 2 s. A link that dribbles bytes stretches it further, since every arrival re-arms. Re-arm the port from the time actually left before each read and restore the caller's value afterwards, so the next transaction is unaffected.
recv_exact returned the instant the nth byte landed, so a reply that was wrong but happened to start with the expected prefix left its surplus queued and the harness exited 0. Route every command through a settling reader that requires the link to fall silent, and classify a straggler as a transport fault rather than a match. The docs blamed the branch base for the archived bitstreams, but that revision contains no fpga/ulx3s file and so cannot have built them. Record the source revision and per-input digests from the build scripts themselves, and name the revision the artefacts actually reproduce from.
When the recorder ran outside a git checkout, every per-input comparison was skipped and the dirty flag stayed false, so the manifest reported inputs-match-revision: yes against a revision it had just recorded as unknown. Report the match as unknown in that case, so the archive claims only what was actually compared.
The recorder only digested $SOURCES and $LPF, so a build run from a locally edited build_smoke.sh or build_uart.sh -- different yosys or nextpnr flags, identical RTL -- still wrote inputs-match-revision: yes. The archive then attributed its bitstream to the recipe at HEAD, which never ran and cannot reproduce it. Both flows now hand their own script to the recorder. The test helper reads the recorded input set back out of the recorder invocation instead of restating it, so a build that drops an input fails rather than quietly narrowing what the archive claims to cover.
The archived manifests predate the recipe becoming a recorded input, so they covered only the RTL and the LPF. Regenerated by the recorder itself from a clean checkout of 62e96e7, and the documented artefact revision moved to the revision that actually holds those inputs. Only the recorded input set moved: every RTL and LPF digest is byte-identical to the previous manifests, and no synthesis command changed, so the archived bitstreams are unaffected.
…-mincore # Conflicts: # SHA256SUMS
# Conflicts: # SHA256SUMS
- tools/atomic_publish.py: use AT_FDCWD_DARWIN (-2) for renameatx_np on macOS - tools/portable_build_support.py: start build in own session and forward cancellation via os.killpg so grandchildren (yosys/nextpnr) are signalled - results/.../tool_versions*.txt: restore pinned OSS CAD Suite 0.67+94 / 0.10 / 1.4-79 - docs/ULX3S_SMOKE_AND_UART.md + manifests: update published SHA-256 to eb3d81ac... (smoke) and 7272b0d8... (bridge) matching refreshed artefacts Preserves: reproducible source at a472265, 25 MHz timing closure, pin/output safety (G2/B2/M1/L4 only), exact SHA256/provenance, protocol correctness (lean_silicon_lsc1 MinCore, no packet lanes touched). Focused tests exercising fixed modules: OK. Gate checks (smoke, boundary, consistency, checksums): OK. Provenance tests report expected mismatch for portable_build_support.py because committed artefacts record the pre-fix digest; bitstream regeneration is out of scope for this repair. Refs: discussion_r3651892558, discussion_r3651892560, discussion_r3651892562, discussion_r3651892564
# Conflicts: # SHA256SUMS # docs/STATUS.md # fpga/ulx3s/Makefile # fpga/ulx3s/build_uart.sh # fpga/ulx3s/uart_bridge.sv # fpga/ulx3s/uart_rx.sv # fpga/ulx3s/ulx3s_top.sv # fpga_harness/test_artefact_provenance.py # test/Makefile
|
@codex review |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_e6a41744-849d-4cde-b94a-d365b470a2e2) |
![chatgpt-codex-connector[bot]](https://avatars.githubusercontent.com/in/1144995?s=60&v=4){kind=small}
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: ba03b5783b
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_6796a7ab-264a-4e2a-9830-d273e9d5c798) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 29356f1c9e
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_e35afee6-39df-45ea-b249-3374f2ec090d) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: b76a5a0c46
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_cfeedd55-d119-4380-988a-0ec531f8fe71) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 21483f5f3d
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_d742c525-07e7-4a6b-a82c-e12e5f9bf7f2) |
Bugbot couldn't run - usage limit reachedBugbot is counted against Cursor usage for this user or team, and this run hit a usage or spend limit. A user or team admin can review and increase usage limits in the Cursor dashboard. (requestId: serverGenReqId_bf8ca0d1-6b9e-4232-8993-9e5d099d0634) |
There was a problem hiding this comment.
💡 Codex Review
lean-silicon/asic_core/rtl/lsc1_packet_frontend.sv
Lines 507 to 510 in 20f13be
Keep decoder faults unbound until parsing succeeds
For a malformed instruction payload such as a JUMP whose taken byte is 2, decode_request_payload raises before returning a decoded request, so the executable endpoint emits the fault with transaction ID 0. The RTL assigns the payload transaction ID here before completing those validations and later passes it to emit_fault, making fault payload bytes 0–3 differ from the model even though the corrected detail byte is 3; retain transaction ID 0 for payload-decoding faults until the full payload has parsed successfully.
ℹ️ About Codex in GitHub
Your team has set up Codex to review pull requests in this repo. Reviews are triggered when you
- Open a pull request for review
- Mark a draft as ready
- Comment "@codex review".
If Codex has suggestions, it will comment; otherwise it will react with 👍.
Codex can also answer questions or update the PR. Try commenting "@codex address that feedback".
| end else if (result_pending) begin | ||
| emit_fault(BAD_STATE, frame_payload[0 +: 32], 0); |
There was a problem hiding this comment.
When a result is pending and the next correctly framed instruction contains an invalid profile, cell, or JUMP taken byte, this guard immediately returns BAD_STATE; the normative path in sim/lsc1_transaction.py::_dispatch first calls decode_request_payload, so it returns the corresponding payload fault before _handle_instruction checks transaction state. Parse and validate the fixed-size instruction payload before applying the pending-state guard to preserve byte-exact model behavior.
Useful? React with 👍 / 👎.
| if (frame_payload[13*8 +: 8] != 0) begin | ||
| decision_ok = 1'b0; decision_fault = BAD_FLAGS; decision_detail = 1; | ||
| end else if (profile > 1) begin | ||
| decision_ok = 1'b0; decision_fault = BAD_PROFILE; |
There was a problem hiding this comment.
When an instruction preamble contains both a profile greater than 1 and a nonzero transaction-flags byte, the normative _read_preamble reads and validates the profile first and therefore returns BAD_PROFILE; this ordering tests the flags first and returns BAD_FLAGS. Reverse these two validations so malformed multi-error frames remain byte-for-byte consistent with the executable protocol decoder.
Useful? React with 👍 / 👎.
1 participant
Summary
Integrates the qualified packetized LSC-1 work from merged PR #24 onto current
mainwhile preserving the unrelated commits already onmain.4dac896587823fe47c8463936c2b46335c19ca9cdcd6bf3c3e7e64c6dfcf2da2288958fb7488961ba622528c7599cafee608f8ae3ced80fa8e848bf979c7ff4721fc7b956caa3a0978fe66225e640939ba03b5783b28e50253a0ccec01bb67cd51f150094618d9c3d1cc2552d4f92257fdeaaf0deda6c28eThe merge conflicts were duplicate-history conflicts in the ULX3S harness, status, test Makefile, and checksum inventory. They were resolved conservatively by retaining PR #24's later hardened versions and regenerating the repository checksum inventory. Main's PR #25 documentation/logo commits remain in the ancestry and were not altered.
Validation
Passed locally:
make PYTHON=.venv/bin/python checkLEANVM_B_UPSTREAM=/tmp/leanVM-b-pr24 make PYTHON=.venv/bin/python simPATH=... LEANVM_B_UPSTREAM=/tmp/leanVM-b-pr24 make PYTHON=.venv/bin/python m2-differentialc308034ab78619b39a59d26f3dc60e7df5b52649elan toolchain install leanprover/lean4:v4.32.1 && make leanLeanVMBMinCoretarget)sby -f gf8_mul.sbylean_silicon_lsc1python tools/generate_checksums.py --checksorry,admit, oraxiomin the checked Lean source setLocal formal limitations (authoritative GitHub CI is requested):
sby -f gf128_serialize.sbycould not run its engines:SMT Solver 'yices-smt2' not found in path.sby -f stream_alu_mul_pulse.sbycould not elaborate:slang.so: cannot open shared object file: No such file or directory.Boundaries
main.Note
High Risk
Large RTL and protocol-surface change at the tapeout top, with new control paths (retire, jump, deref) and host/FPGA integration; correctness relies on differential tests, not full formal ISA correspondence.
Overview
Product top is now
lsc1_packet_frontendonlean_silicon_lsc1, with the raw stream ALU moved to diagnosticlean_silicon_lsc1_mincore. Newlsc1_stream_adapterandlsc1_field_encoderconnect packet ops to the existing MinCore byte stream.The frontend grows from SET/XOR/MUL to NEGOTIATE, STATUS, DEREF (Cell/Pc/Fp), and JUMP, using the stream adapter instead of a standalone GF128 multiplier; RX payload width and body capture are extended for large frames (e.g. JUMP inverse witness).
Host runtime integrates Deref and Jump (pointer map, branch proposals, inverse witnesses); the frozen fixture now reaches full MATCH on memory and cycles.
lsc1_packet_uart.pydrives the physical packet lane (BREAK abort, capability checks, optional full program run).ULX3S:
uart_bridgePACKET_MODE(no 0x7f in-band abort in packet mode),ulx3s_packet_top+build_packet_uart.sh, UART RX wait_idle after framing errors.hardware_preflight.pyadds non-programming host evidence;fpga-preflightis optional outside defaultcheck.CI / build: Yosys top includes all packet RTL modules;
gate-count→mincore-state-count; sim adds packet UART bridge andsim/test_packet_frontend_rtl_differential.py(seeded byte-exact model vs RTL). Docs andinfo.yamlreflect implemented scalar executor vs pending BLAKE3/services.Reviewed by Cursor Bugbot for commit 20f13be. Bugbot is set up for automated code reviews on this repo. Configure here.