[abmajith]

• rtl/cores/rabbit_common: decoder, ALU, regfile, CSRs moved out of rabbit5; new rabbit_execute (whole execute stage: operands, branches, exceptions, CSRs, next pc -> exec_t record) and rabbit_rvfi; LSU/branch helpers in rabbit_pkg
• rabbit5_core.sv now only the pipeline (496 -> 278 lines); same 3958 cycles for hello, riscv-formal 45/45
• rabbit3: F | X | W pipeline from the same blocks; no forwarding network and no load-use stall (regfile write-first bypass), 1-bubble redirects; hello 3145 cycles, riscv-formal 45/45, timing properties, GLS smoke
• dv/formal/rabbit: one flow for every core (CORE=rabbit3|rabbit5); each core declares its timing model in core.mk and the shared timing testbench proves it
• fix: timing testbench free inputs are now top-level inputs; slang silently drops (* anyseq *), which made the earlier rabbit5 timing proof weaker than reported. Re-proven and re-mutation-tested.
• riscv-formal cover moved to step 10 (exact counts at step 20 took up to 14 min; the bounds are proven in the timing testbench instead)
• CI: rabbit3 in all matrices; formal and GLS per core
• docs: rabbit3 "start here" learning path, rabbit_common overview