[NO-MERGE] LSC1-08: extract BLAKE3 lifecycle shell - #76
Conversation
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_df0d7df9-a638-4258-8fca-881cb13bff41) |
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_040c1d42-44fc-47ff-81a0-b9694ef86eef) |
![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: 57f893998d
ℹ️ 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".
| .fault(encoder_fault), .result(encoder_result) | ||
| ); | ||
|
|
||
| lsc1_blake3_lifecycle blake3_lifecycle ( |
There was a problem hiding this comment.
The new instantiation introduces a mandatory RTL dependency, but I checked the Yosys source lists in .github/workflows/ci.yml (lines 158–161), fpga/ulx3s/build_packet_uart.sh (lines 40–50), fpga/ulx3s/build_uart.sh (lines 51–61), and assurance/full-lsc1-netlist/plan.json (lines 12–20), and none includes lsc1_blake3_lifecycle.sv. Consequently those lint, FPGA, and full-netlist assurance flows elaborate lsc1_packet_frontend with an unresolved lsc1_blake3_lifecycle cell; add the new source to each manifest.
Useful? React with 👍 / 👎.
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_7b3d3c91-7227-430e-93b5-e7016c2a6abb) |
|
@codex review Please review current head |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 4a6ed07eea
ℹ️ 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".
| if (frame_length != 8) begin | ||
| emit_fault(BAD_LENGTH, frame_payload[0 +: 32], 2); | ||
| end else if (blake_result_pending) begin | ||
| blake_retire_attempt <= 1'b1; |
There was a problem hiding this comment.
When a matching BLAKE3 RETIRE is accepted, this nonblocking handoff is not observed by blake3_lifecycle until the next rising edge. The frontend therefore commits pc/fp and queues the RETIRED response immediately, but the child asserts done_pulse one clock later, when the transmitter also becomes active and presents the first response byte. This makes BLAKE3 retirement differ from the scalar path and violates the pin contract that DONE is asserted in the cycle following acceptance and on the edge where committed state moves; align the lifecycle pulse with the frontend's acceptance/commit edge.
Useful? React with 👍 / 👎.
|
@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_7dbb28ec-7dff-4066-b0f2-7a073b2e0ed8) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 98b18fd8a2
ℹ️ 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".
| .tx_start(tx_start), .tx_busy(tx_busy), .compute_state(compute_state), | ||
| .alu_busy(alu_busy), .encoder_busy(encoder_busy), | ||
| .result_pending(result_pending), .service_pending(service_pending) | ||
| .result_pending(result_pending), .service_pending(blake_service_pending) |
There was a problem hiding this comment.
When FORMAL_FULL_LSC1 is enabled, this now passes only the scalar result_pending flag to full_lsc1_controller_invariants, even though BLAKE3 result state moved to blake_result_pending. Consequently the pending-implies-BUSY and abort-clears-pending assertions, plus result-pending coverage, no longer exercise the BLAKE3 RESULT-to-RETIRE interval that they covered before extraction; bind the result input to the union of both pending flags.
Useful? React with 👍 / 👎.
| alu_start <= 1'b0; | ||
| encoder_start <= 1'b0; | ||
| done_pulse <= 1'b0; | ||
| core_done_pulse <= 1'b0; |
There was a problem hiding this comment.
After renaming the internal register to core_done_pulse, the corrupted_staged_fp_retention and duplicate_completion_pulse entries in formal/check_deref_retire_formal_mutations.py still search for literal done_pulse <= ... blocks. On every make formal-deref-coverage-mutation run those anchors have count zero, so run_formal raises ValueError and the mutation campaign fails before invoking the proofs; update both anchors and replacements to the new register name.
Useful? React with 👍 / 👎.
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_9497bd9f-5540-4712-824c-2a1b1f7027a1) |
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_c6daa5c9-eb59-430d-9ac4-a8cf53597d8c) |
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_9ada7d56-cd5b-4447-ad34-6d99370f85d2) |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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_8ee3bee2-2412-45a4-83f9-ed232c582369) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 34e5c099bd
ℹ️ 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".
| source.write_text(harness("scalar_result_pending || blake_result_pending")) | ||
| baseline = run(source, "prove") | ||
| coverage = run(source, "cover") | ||
| source.write_text(harness("scalar_result_pending")) | ||
| mutation = run(source, "prove") |
There was a problem hiding this comment.
Fresh evidence in the current head is that all three SBY runs prove or mutate a generated binding.sv harness rather than lsc1_packet_frontend and its invariant instance; the production RTL is checked only by literal substring searches above. Consequently, if the real BLAKE3 pending path becomes unreachable or its connectivity is otherwise broken while those strings remain, the baseline, cover, and mutation receipt still passes, so the reported blake_only_pending_cover does not close the production coverage gap. Instantiate or mutate the actual frontend binding in the SBY harness.
Useful? React with 👍 / 👎.
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_740754fb-a73a-4b59-9657-2f74fe4464ce) |
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_828d639f-80f4-48c2-80e0-e1589cb641cc) |
|
Codex Review: Didn't find any major issues. Can't wait for the next one! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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_fcdf5896-ed21-45f1-84c2-23cba15e8efc) |
|
@codex review Please review current head |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 2cc9b75ed5
ℹ️ 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".
| work = Path(raw) | ||
| for source in SOURCES: | ||
| shutil.copy2(RTL / source, work / source) | ||
| shutil.copy2(FORMAL / CHECKER, work / CHECKER) |
There was a problem hiding this comment.
Fresh evidence at the current head is that the receipt now copies blake3_pending_binding_checker.sv instead of full_lsc1_controller_invariants.sv. If the production pending assertion is deleted or weakened, all three runs still use the duplicate assertion from the checker, and the frontend mutation remains killed, so make formal-deref-coverage-mutation can report success without verifying that the shipped invariant enforces the pending union.
Useful? React with 👍 / 👎.
|
@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_0741961d-eac3-4a02-8b70-18a16aee04a1) |
|
Codex Review: Didn't find any major issues. Chef's kiss. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
|
@codex review Please review exact head |
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_db0ecd2c-2ec3-4d91-9216-44ed213af835) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 97b437848b
ℹ️ 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".
| "proof_pass": proof.returncode == 0, | ||
| "cover_reached": cover.returncode == 0, | ||
| "property_missing": property_missing, | ||
| "killed": isolated and property_missing and proof.returncode == 0 and cover.returncode == 0, |
There was a problem hiding this comment.
Fresh evidence at the exact head is that the assertion mutants are now isolated, but they are still declared killed only when both formal jobs succeed and property_missing confirms the replacement that this script just performed. With the union intact, weakening or removing the implication cannot affect either job, so a harness completely insensitive to the production assertion produces the same successful receipt. Make an independent validation step consume each mutant and reject the missing/weakened property rather than counting proof/cover success as a kill.
Useful? React with 👍 / 👎.
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_1dbf20da-5e2a-4170-b64e-07328feed876) |
|
Codex Review: Didn't find any major issues. Already looking forward to the next diff. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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_ad8c3c7e-0a34-4dc0-b05f-7c5706610415) |
|
Codex Review: Didn't find any major issues. More of your lovely PRs please. Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
|
@codex review Please review exact head |
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_156f097c-d7e4-4f6f-af8d-19ea1e06e381) |
There was a problem hiding this comment.
💡 Codex Review
Here are some automated review suggestions for this pull request.
Reviewed commit: 3a65dbaba1
ℹ️ 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".
| con = cell.get("connections", {}) | ||
| if not {"A", "EN"}.issubset(con) or len(con["A"]) != 1 or len(con["EN"]) != 1: | ||
| unknown.append(name) | ||
| continue |
There was a problem hiding this comment.
When the production implication is changed from always @(*) to an edge-triggered assertion under pinned Yosys 0.68, $check stores that distinction in its TRG connection and TRG_* parameters, but this validation only inspects A and EN. Updating the committed 0.68 fixture's matching cell to have a clock trigger still makes validate_design return valid, so the receipt can accept a property that no longer covers arbitrary initial lifecycle state as intended; require the matching $check to be untriggered.
Useful? React with 👍 / 👎.
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_22d6da46-4668-4b2d-8fd6-339cbe92d113) |
|
@codex review Fresh exact-head review requested for the elaborated trigger-semantics repair. Please review the current PR head only. The validator now requires the matching pinned-Yosys |
|
Codex Review: Didn't find any major issues. Breezy! Reviewed commit: ℹ️ About Codex in GitHubYour team has set up Codex to review pull requests in this repo. Reviews are triggered when you
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". |
1 participant
Scope
lsc1_blake3_lifecycleSERVICE_REQUIRED/RESULT/RETIREDbytes and CRCsEvidence
make check(379 Python tests, repository checks, checksum inventory)make sim(authored RTL simulations, packet mutation gate, full RTL differential, v3 finite-stall replay)make lsc1-authored-rtl-contract(observations=30 source=rtl-traces)make lsc1-host-authored-rtl-boundary(steps=13 model=MATCH lean=PASS rtl=MATCH)make -C test/packet_frontend lifecycle lifecycle-mutationpython3 -m unittest sim.test_conformance_v3_rtl_differential sim.test_packet_frontend_rtl_differential -q(18 tests)make checksum-checkThe focused shell test exercises transaction/service identifiers, RESULT CRC capture, matching and foreign RETIRE, mismatch discard, exactly-once
done_pulse, and reset/abort clearing. Its mutation gate kills identifier-match, done-pulse, and abort-clear mutations. The existing v3 authored-RTL harness continues to exercise byte stability under supported finite two-state RX/TX stall schedules.Claim boundary
This PR claims only preservation at the extracted authored-SystemVerilog lifecycle-shell interface and the existing executable LSC1-05/06/07 gates. It makes no broader refinement, implementation, or hardware claim.
NO-MERGE: requested focused evidence PR; do not merge as part of this task.
Note
Medium Risk
Changes retirement and commit timing on the BLAKE3 path in the packet frontend, but scope is bounded by new lifecycle RTL, updated formal invariants, and mutation/oracle CI gates rather than broad protocol changes.
Overview
Extracts full-profile BLAKE3 service/result/retire state into new
lsc1_blake3_lifecycle, while the packet frontend keeps decode, staging, and TX byte serialization.The frontend wires the shell for
OP_BLAKE3,OP_SERVICE_RESPONSE, andOP_RETIRE: BLAKE pending IDs and CRCs drive external TX payloads;done_pulsemerges core and BLAKE completion; RETIRE for BLAKE is handled on the same cycle as the lifecycle via combinationalblake_retire_attempt(no registered handoff). Scalar RETIRE andresult_pendingbehavior stay on the existing path.Assurance adds a production binding that
blake_result_pendingimplies the unionresult_pendingpassed to formal invariants, plus BMC/cover and mutation checks (check_blake3_pending_invariant.py, structural contract validator, versioned Yosys oracle fixtures). Formal bridge/scalar/jump.sbyflows, deref mutation lists, netlist plan inputs, CI Yosys read list, and packet-frontend sim targets are updated to include the new RTL.Reviewed by Cursor Bugbot for commit e298460. Bugbot is set up for automated code reviews on this repo. Configure here.