Repository navigation
Rabbit mext - #16
Merged
Merged
Rabbit mext#16
Conversation
…roven - rtl/cores/rabbit_common/rabbit_muldiv.sv: one 33x17 Booth multiplier used twice (MUL/MULH/MULHSU/MULHU in 2 cycles), restoring divider with a fixed 34 cycles (also x/0 and overflow), abandoned on an interrupt so the proven interrupt latency (4 / 7 cycles) holds; operand isolation for power. - rabbit_execute: busy_o holds an M instruction in the commit stage; fixed rvfi_intr being lost when the handler starts with an M instruction. - rabbit3: instruction hold register and no fetch while X waits. rabbit5: IF/ID wait, EX stores the forwarded operands while it waits. - Verification: riscv-formal 53/53 (RV32IM, ALTOPS, short formal divider); timing rule R8 + M0-M2 properties, I1 restated for M handlers; unit proof dv/formal/rabbit/muldiv (W=4 PDR, W=6 BMC, W=8 exhaustive sim, W=32 latency); sw/baremetal/muldiv on every core, RTL and gate level. All planted mutants caught. - sky130 (synth -booth + ABC): rabbit3 114.9k um2, rabbit5 126.5k um2, CV32E40P (RV32IMC) 170.3k um2. hello: 2756 / 3471 cycles. - Makefile: gls netlist now rebuilds when rabbit_common changes. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…no progress guarantee) Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…(IMPLICITSTATIC) Loop variables are now automatic; testbench warnings are no longer fatal (the RTL stays strictly linted by make lint). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
tools/check_all.sh [quick|gls|formal|synth|mutants|all] reruns every check behind the numbers in the docs (also: make check-all STAGES=...). tools/synth_sky130.sh gives the sky130 area / delay table. tools/mutants.py plants 8 known bugs in copies under build/mutants and checks each is caught; --baseline also checks the unmodified copy passes. All 8 caught, all baselines pass (39 min for the 4 pipeline mutants). Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.