Skip to content

feat: formal RVFI support (M-ext ALTOPS, misalign trap, RVFI CSR chan… #2

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
0611roxe wants to merge 1 commit into
base: main
Choose a base branch
from
Open

feat: formal RVFI support (M-ext ALTOPS, misalign trap, RVFI CSR chan… #2

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
3 changes: 3 additions & 0 deletions .gitignore
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -42,3 +42,6 @@ patch/firtool/firtool-*/
Thumbs.db
.claude/
.codex

# mill temp files (random 6-char suffix)
mill.??????
22 changes: 16 additions & 6 deletions cl1/src/scala/Cl1CSR.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -247,15 +247,18 @@ class Cl1CSR() extends Module {
val dscratch1 = RegEnable(csr_wdat, 0.U(32.W), wen_dscratch1) // Debug Scratch 1

// val mstatus = RegInit("h1800".U(32.W))
val mtvec = RegEnable(csr_wdat, TVEC_ADDR.U(32.W), wen_mtvec)
// mtvec MODE WARL: only MODE={0,1} are legal; bit[1] is hardwired to 0.
val mtvec_wdata = csr_wdat & ~"h2".U(32.W)
val mtvec = RegEnable(mtvec_wdata, TVEC_ADDR.U(32.W), wen_mtvec)

val mepc_wdata = Mux(cmt_epc_en, cmt_epc_n, csr_wdat)
val mepc = RegEnable(mepc_wdata, 0.U(32.W), wen_mepc)
// mepc is WARL: with the C extension IALIGN=16, so bit[0] is hardwired to 0.
val mepc_wdata = Mux(cmt_epc_en, cmt_epc_n, csr_wdat) & ~"h1".U(32.W)
val mepc = RegEnable(mepc_wdata, 0.U(32.W), wen_mepc)
val mcause_wdata = Mux(cmt_cause_en, cmt_cause_n, csr_wdat)
val mcause = RegEnable(cmt_cause_n, 0.U(32.W), wen_mcause)

val misa = WireInit("h40000104".U(32.W))
val mcause = RegEnable(mcause_wdata, 0.U(32.W), wen_mcause)

val misa = WireInit("h40001104".U(32.W))


val allCSRs = Seq(
CSRs.misa -> misa,
Expand Down Expand Up @@ -322,5 +325,12 @@ class Cl1CSR() extends Module {
dbg.step_r := step

dontTouch(mstatus)
dontTouch(mie)
dontTouch(mip)
dontTouch(mepc)
dontTouch(mcause)
dontTouch(mtvec)
dontTouch(mscratch)
dontTouch(misa)

}
4 changes: 2 additions & 2 deletions cl1/src/scala/Cl1Config.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -32,7 +32,7 @@ object Cl1Config {
val Technology = "SMIC110"

val FORMAL_VERIF = true
val RISCV_FORMAL_ALTOPS = false
val RISCV_FORMAL_ALTOPS = true
val EXPOSE_CORE_BUS = true // When true, expose CoreBus (fetch + mem) instead of AXI4 at top level
}

Expand All @@ -42,4 +42,4 @@ object Cl1PowerSaveConfig {
val DCACHE_CKG_EN = if (MODPOWERCFG) true else false
val LSU_CKG_EN = if (MODPOWERCFG) true else false
val RF_NORESET = true
}
}
10 changes: 10 additions & 0 deletions cl1/src/scala/Cl1Core.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -125,6 +125,16 @@ class Cl1Core extends Module {
wbStage.io.toExcp <> excp.io.wb2Excp

excp.io.dbg2excp <> dm.io.dbg2excp
if (cl1.Cl1Config.FORMAL_VERIF) {
// Under formal verification, force debug-mode-related signals into
// architectural mode so traps go to mtvec (not the debug exception base).
// BMC otherwise picks anyinit values for dm registers and explores
// debug-mode trap dispatch, which is outside the RVFI ISA model.
excp.io.dbg2excp.debug_mode := false.B
excp.io.dbg2excp.debug_irq_mask := false.B
excp.io.dbg2excp.debug_take_req := false.B
excp.io.dbg2excp.ebrk_excp_en := dm.io.dbg2excp.ebrk_excp_en
}
excp.io.excp2Csr <> csr.io.excp_intf

excp.io.ext_irq := io.ext_irq
Expand Down
7 changes: 4 additions & 3 deletions cl1/src/scala/Cl1EXCP.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,10 +111,11 @@ class Cl1EXCP() extends Module with TrapCode {
tmr_irq & mtie
val irq_mask = ~mie | debug_irq_mask
val irq_req = irq_req_raw & ~irq_mask
// MEI > MSI > MTI for simultaneously enabled & pending M-mode interrupts.
val irq_casue = MuxCase(0.U, Seq(
(ext_irq & meie) -> M_EXTER_IRQ,
(sft_irq & msie) -> M_SFTER_IRQ,
(tmr_irq & mtie) -> M_TIMER_IRQ,
(ext_irq & meie) -> M_EXTER_IRQ
(tmr_irq & mtie) -> M_TIMER_IRQ
))

val excp_take_en = cmt_ecall | ebrk_excp_en | excp_valid
Expand Down Expand Up @@ -191,4 +192,4 @@ class Cl1EXCP() extends Module with TrapCode {
io.ifu_halt := wfi_ifu_halt
io.dxu_halt := dx_halt
io.core_wfi := core_wfi_o
}
}
2 changes: 1 addition & 1 deletion cl1/src/scala/Cl1IDEXStage.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -431,4 +431,4 @@ class Cl1IDEXStage extends Module with TrapCode {
Bpustat.io.hit_cnt := hit_cnt
}

}
}
2 changes: 1 addition & 1 deletion cl1/src/scala/Cl1MDULp.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -358,4 +358,4 @@ dontTouch(div_quot_oen)
dontTouch(div_remd_oen)
dontTouch(div_rslt)

}
}
103 changes: 98 additions & 5 deletions cl1/src/scala/Cl1Top.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -111,14 +111,19 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) {
val wb_flush = BoringUtils.bore(core.wbStage.io.flush)
val wb_ecall = BoringUtils.bore(core.wbStage.isValidEcall)
val wb_cmt = BoringUtils.bore(core.wbStage.wb_commit)
val rvfi_valid = wb_cmt
val wb_diff_cmt = BoringUtils.bore(core.wbStage.diff_commit)
val trap = BoringUtils.bore(core.excp.excp_take_en)
val wb_excp_fault = BoringUtils.bore(core.wbStage.io.toExcp.excp_valid)

// Retire through RVFI when the instruction either commits normally, or
// takes an M-mode trap (ECALL, or EBREAK with dcsr.ebreakm==0).
val rvfi_valid = wb_diff_cmt || trap
val valid_cnt = Wire(UInt(64.W))
val wb_pc = BoringUtils.bore(core.wbStage.wb_pc)
val wb_is_c = BoringUtils.bore(core.wbStage.pplIn.isCInst)
val wb_cinst = BoringUtils.bore(core.wbStage.io.cInst)
val wb_inst = BoringUtils.bore(core.wbStage.io.inst)
valid_cnt := RegEnable((valid_cnt + 1.U), 0.U, rvfi_valid)
val trap = BoringUtils.bore(core.excp.excp_take_en)

val dx_rs1_addr = BoringUtils.bore(core.idStage.io.rs1Addr)
val dx_rs2_addr = BoringUtils.bore(core.idStage.io.rs2Addr)
Expand Down Expand Up @@ -165,9 +170,26 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) {
rvfi_port.rvfi_valid := rvfi_valid
rvfi_port.rvfi_order := valid_cnt
rvfi_port.rvfi_insn := Mux(wb_is_c, wb_cinst, wb_inst)
rvfi_port.rvfi_trap := trap
rvfi_port.rvfi_trap := wb_excp_fault
rvfi_port.rvfi_halt := false.B
rvfi_port.rvfi_intr := false.B

val intr_taken = BoringUtils.bore(core.excp.irq_take_en)
val excp_flush_pc = BoringUtils.bore(core.excp.flush_pc)
val excp_flush_ofst = BoringUtils.bore(core.excp.flush_ofst)
val mret_taken = BoringUtils.bore(core.excp.cmt_mret_en)
val trap_target_pc = excp_flush_pc + excp_flush_ofst

val dbg_flush = BoringUtils.bore(core.dm.io.dbg_flush)
chisel3.assume(!dbg_flush)

val intr_pending = RegInit(false.B)
when (trap || intr_taken) {
intr_pending := true.B
} .elsewhen (rvfi_valid) {
intr_pending := false.B
}

rvfi_port.rvfi_intr := intr_pending && rvfi_valid
rvfi_port.rvfi_mode := "b11".U(2.W)
rvfi_port.rvfi_ixl := "b01".U(2.W)

Expand All @@ -178,13 +200,84 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) {
rvfi_port.rvfi_rd_addr := Mux(wb_rd_wen, wb_rd_addr, 0.U)
rvfi_port.rvfi_rd_wdata := Mux(wb_rd_wen, wb_rd_wdata, 0.U)
rvfi_port.rvfi_pc_rdata := wb_pc
rvfi_port.rvfi_pc_wdata := Mux(dx_valid, dx_pc,f2_pc)
rvfi_port.rvfi_pc_wdata := Mux(trap || mret_taken, trap_target_pc,
Mux(dx_valid, dx_pc, f2_pc))

rvfi_port.rvfi_mem_addr := Mux(mem_rsp_hsked, mem_addr, 0.U) & "hffff_fffc".U
rvfi_port.rvfi_mem_rmask := Mux(mem_rsp_hsked, mem_rmask, 0.U)
rvfi_port.rvfi_mem_wmask := Mux(mem_rsp_hsked, mem_wmask, 0.U)
rvfi_port.rvfi_mem_rdata := Mux(mem_rsp_hsked, wb_mem_rdata, 0.U)
rvfi_port.rvfi_mem_wdata := Mux(mem_rsp_hsked, mem_wdata, 0.U)

// ---- CSR channels ----
val wb_csr_idx = BoringUtils.bore(core.wbStage.io.csr_idx)
val wb_csr_wen = BoringUtils.bore(core.wbStage.io.csrWen)
val wb_csr_wdata = BoringUtils.bore(core.wbStage.io.csrWdat)
val wb_csr_rdata = BoringUtils.bore(core.wbStage.pplIn.rdWdat)

val wb_is_csr_insn = (wb_inst(6,0) === "b1110011".U) && (wb_inst(14,12) =/= 0.U)

val cur_mstatus = BoringUtils.bore(core.csr.mstatus)
val cur_mie = BoringUtils.bore(core.csr.mie)
val cur_mip = BoringUtils.bore(core.csr.mip)
val cur_mepc = BoringUtils.bore(core.csr.mepc)
val cur_mcause = BoringUtils.bore(core.csr.mcause)
val cur_mtvec = BoringUtils.bore(core.csr.mtvec)
val cur_mscratch = BoringUtils.bore(core.csr.mscratch)
val cur_misa = BoringUtils.bore(core.csr.misa)

val cmt_epc_en = BoringUtils.bore(core.excp.cmt_epc_en)
val cmt_cause_en = BoringUtils.bore(core.excp.cmt_cause_en)
val cmt_status_en = BoringUtils.bore(core.excp.cmt_status_en)
val cmt_mret_en = BoringUtils.bore(core.excp.cmt_mret_en)
val cmt_epc_n = BoringUtils.bore(core.excp.cmt_epc_n)
val cmt_cause_n = BoringUtils.bore(core.excp.cmt_cause_n)

val cur_mstatus_mie = cur_mstatus(3)
val cur_mstatus_mpie = cur_mstatus(7)

val mstatus_trap_wdata = {
val cur = cur_mstatus
val withClrMie = Cat(cur(31, 4), 0.U(1.W), cur(2, 0)) // MIE=0
val withMpieMie = Cat(withClrMie(31, 8), cur_mstatus_mie, withClrMie(6, 0)) // MPIE<-MIE
withMpieMie
}
val mstatus_mret_wdata = {
val cur = cur_mstatus
val withSetMie = Cat(cur(31, 4), cur_mstatus_mpie, cur(2, 0)) // MIE<-MPIE
val withSetMpie = Cat(withSetMie(31, 8), 1.U(1.W), withSetMie(6, 0)) // MPIE=1
withSetMpie
}
val mstatus_implicit_wdata = Mux(cmt_status_en, mstatus_trap_wdata, mstatus_mret_wdata)

def driveCsr(chan: RVFICSR, addr: UInt, cur: UInt,
implicitWrite: Bool = false.B,
implicitWdata: UInt = 0.U): Unit = {
val selCsrInsn = wb_is_csr_insn && (wb_csr_idx === addr) && rvfi_valid
val selW = wb_csr_wen && (wb_csr_idx === addr) && rvfi_valid
val implW = implicitWrite && rvfi_valid
val anyW = selW || implW
chan.rmask := Fill(32, selCsrInsn)
chan.wmask := Fill(32, anyW)
chan.rdata := cur
chan.wdata := Mux(selW, wb_csr_wdata, Mux(implW, implicitWdata, cur))
}

driveCsr(rvfi_port.rvfi_csr_mstatus, CSRs.mstatus, cur_mstatus,
cmt_status_en || cmt_mret_en, mstatus_implicit_wdata)
driveCsr(rvfi_port.rvfi_csr_mie, CSRs.mie, cur_mie)
driveCsr(rvfi_port.rvfi_csr_mip, CSRs.mip, cur_mip)
driveCsr(rvfi_port.rvfi_csr_mepc, CSRs.mepc, cur_mepc,
cmt_epc_en, Cat(cmt_epc_n(31, 1), 0.U(1.W)))
driveCsr(rvfi_port.rvfi_csr_mcause, CSRs.mcause, cur_mcause,
cmt_cause_en, cmt_cause_n)
driveCsr(rvfi_port.rvfi_csr_mtvec, CSRs.mtvec, cur_mtvec)
driveCsr(rvfi_port.rvfi_csr_mscratch, CSRs.mscratch, cur_mscratch)

rvfi_port.rvfi_csr_misa.rmask := Fill(32, true.B)
rvfi_port.rvfi_csr_misa.wmask := 0.U
rvfi_port.rvfi_csr_misa.rdata := cur_misa
rvfi_port.rvfi_csr_misa.wdata := cur_misa
}}

}
18 changes: 18 additions & 0 deletions cl1/src/scala/Cl1WBStage.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,24 @@ class Cl1WBStage extends Module {
val wb_ebreak = pplIn.privInstr(2)
val wb_mret = pplIn.privInstr(1)
val wb_dret = pplIn.privInstr(0)

// Formal-only: under `-nordff`, every pipeline register field becomes an
// independent anyinit variable.
if (FORMAL_VERIF) {
val f3_priv = instr(14, 12) === 0.U
val priv_form = (instr(6, 0) === "b1110011".U) &
(instr(11, 7) === 0.U) &
(instr(19, 15) === 0.U) & f3_priv
val f12 = instr(31, 20)
val expected = Cat(
priv_form & (f12 === "h105".U), // wfi
priv_form & (f12 === "h000".U), // ecall
priv_form & (f12 === "h001".U), // ebreak
priv_form & (f12 === "h302".U), // mret
priv_form & (f12 === "h7b2".U) // dret
)
chisel3.assume(pplIn.privInstr === expected)
}

val isValidEcall = wb_valid && wb_ecall
val isValidEret = wb_valid && wb_mret
Expand Down
16 changes: 16 additions & 0 deletions cl1/src/scala/RVFI.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,13 @@ package cl1

import chisel3._

class RVFICSR extends Bundle {
val rmask = Output(UInt(32.W))
val wmask = Output(UInt(32.W))
val rdata = Output(UInt(32.W))
val wdata = Output(UInt(32.W))
}

class RVFI extends Bundle {
val rvfi_valid = Output(Bool())
val rvfi_order = Output(UInt(64.W))
Expand All @@ -26,4 +33,13 @@ class RVFI extends Bundle {
val rvfi_mem_wmask = Output(UInt(4.W))
val rvfi_mem_rdata = Output(UInt(32.W))
val rvfi_mem_wdata = Output(UInt(32.W))

val rvfi_csr_mstatus = new RVFICSR
val rvfi_csr_mie = new RVFICSR
val rvfi_csr_mip = new RVFICSR
val rvfi_csr_mepc = new RVFICSR
val rvfi_csr_mcause = new RVFICSR
val rvfi_csr_mtvec = new RVFICSR
val rvfi_csr_mscratch = new RVFICSR
val rvfi_csr_misa = new RVFICSR
}