[abmajith]

Core (rtl/cores/rabbit_common, shared):

• rabbit_csr: mie, mip, vectored mtvec (reset vectored, like CV32E40P), interrupt priority 31..16 > 11 > 3 > 7 (CV32E40P order), wake/pending outputs
• rabbit_execute: an interrupt replaces the instruction at the commit point (it does not retire, mepc = its pc); first handler instruction marked rvfi_intr; WFI = redirect to pc+4 plus sleep request
• rabbit3/rabbit5 pipelines: sleep_q stops fetch, restarts in the cycle an enabled interrupt appears; core_sleep_o for clock gating

SoC: rabbit_timer (mtime/mtimecmp, line 7), IRQ register in rabbit_sim_ctrl. Firmware: sw/baremetal/irq self-test (mip, masking, priority, timer control loop with WFI, WFI without handler, latency); passes on cv32e40p (reference), rabbit3 and rabbit5.

Formal:

• riscv-formal 45/45 on both cores with interrupt lines 7/16 free; intr cover
• timing testbench: spec model of mstatus/mie/mtvec from RVFI; new T4 (wake timing), I1 latency bound (rabbit3 4, rabbit5 7 cycles, both reached), I2 no spurious, I3 precise mepc, I4 mcause, I5 trap vector, W0-W2 sleep
• mutation tests: 9 planted bugs caught, 1 equivalent mutant explained

Also: cocotb Makefile rebuilds when RTL in files.f changes (stale models).