Skip to content

fix(formal): repair RVFI retire and memory fault reporting #6

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
qinhan2373 wants to merge 1 commit into
base: v2.x-dev
Choose a base branch
from
Open

fix(formal): repair RVFI retire and memory fault reporting #6

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
7 changes: 6 additions & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ DUMP_WAVE :=
PWR_ANALYSIS :=1
CL1_TEST_MODE ?= cache
CL1_PLATFORM ?= simple_soc
CL1_AXI_FORMAL_CACHE_IDXW ?= 1

CONFIG_DBG = n
CONFIG_NETSIM = n
Expand Down Expand Up @@ -72,7 +73,7 @@ WAVE ?= gtkwave

# Phony Targets
.DEFAULT_GOAL := verilog
.PHONY: all verilog verilog-sim verilog-full-cache-axi verilog-full-soc-syn verilog-full-soc-diff verilog-no-cache verilog-rvfi verilog-rvfi-axi verilog-rvfi-cache help reformat checkformat clean run
.PHONY: all verilog verilog-sim verilog-full-cache-axi verilog-full-soc-syn verilog-full-soc-diff verilog-no-cache verilog-rvfi verilog-rvfi-axi verilog-rvfi-axi-cache verilog-rvfi-cache help reformat checkformat clean run

# Generate Verilog
FIRTOOL_VERSION = 1.105.0
Expand Down Expand Up @@ -125,6 +126,10 @@ verilog-rvfi:
verilog-rvfi-axi:
$(call gen_verilog,CL1_TEST_MODE=cache CL1_TOP_NAME=Cl1Top_RVFI_AXI CL1_FORMAL_VERIF=true CL1_RISCV_FORMAL_ALTOPS=true CL1_HAS_ICACHE=false CL1_HAS_DCACHE=false,Cl1Top_RVFI_AXI)

# RVFI with riscv-formal M-extension alternative ops, AXI exposed, I/D cache enabled.
verilog-rvfi-axi-cache:
$(call gen_verilog,CL1_TEST_MODE=cache CL1_TOP_NAME=Cl1Top_AXI_CACHE CL1_FORMAL_VERIF=true CL1_RISCV_FORMAL_ALTOPS=true CL1_HAS_ICACHE=true CL1_HAS_DCACHE=true CL1_SYN=false CL1_FORMAL_CACHE_IDXW=$(CL1_AXI_FORMAL_CACHE_IDXW),Cl1Top_AXI_CACHE)

# RVFI with riscv-formal M-extension alternative ops, AXI exposed, minimal cache.
verilog-rvfi-cache:
$(call gen_verilog,CL1_TEST_MODE=cache CL1_TOP_NAME=Cl1Top_RVFI_CACHE CL1_FORMAL_VERIF=true CL1_RISCV_FORMAL_ALTOPS=true CL1_HAS_ICACHE=true CL1_HAS_DCACHE=true CL1_SYN=false,Cl1Top_RVFI_CACHE)
Expand Down
35 changes: 23 additions & 12 deletions cl1/src/scala/Cl1Top.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -113,12 +113,14 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) {
val wb_valid = BoringUtils.bore(core.wbStage.wb_valid)
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 trap = BoringUtils.bore(core.excp.excp_req)
val wb_diff_cmt = BoringUtils.bore(core.wbStage.diff_commit)
val trap_req = BoringUtils.bore(core.excp.excp_req)
val wb_excp_fault = BoringUtils.bore(core.wbStage.io.toExcp.excp_valid)
val wb_excp_code = BoringUtils.bore(core.wbStage.io.toExcp.excp_code)

// Retire through RVFI when the instruction commits at writeback.
val rvfi_valid = wb_cmt
// RVFI valid is a retire pulse. Exception requests are control-flow requests
// and can remain asserted while WB is stalled, so they must not create retires.
val rvfi_valid = wb_diff_cmt
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)
Expand Down Expand Up @@ -168,9 +170,15 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) {
val mem_wmask = RegEnable(mem_wmask_n, 0.U, mem_req_hsked)
val mem_wdata = RegEnable(mem_wdata_n, 0.U, mem_req_hsked)

val inst_access_fault = rvfi_valid && wb_excp_fault && (wb_excp_code === 1.U)
val load_access_fault = rvfi_valid && wb_excp_fault && (wb_excp_code === 5.U)
val store_access_fault = rvfi_valid && wb_excp_fault && (wb_excp_code === 7.U)
val data_access_fault = load_access_fault || store_access_fault
val mem_fault = inst_access_fault || data_access_fault

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_insn := Mux(inst_access_fault, 0.U, Mux(wb_is_c, wb_cinst, wb_inst))
rvfi_port.rvfi_trap := wb_excp_fault
rvfi_port.rvfi_halt := false.B

Expand All @@ -179,13 +187,13 @@ if(FORMAL_VERIF && WB_PIPESTAGE) { withReset(rst1) {
val excp_flush_ofst = BoringUtils.bore(core.excp.flush_ofst)
val mret_taken = BoringUtils.bore(core.excp.cmt_mret_en)
val cur_excp_mtvec = BoringUtils.bore(core.csr.mtvec)
val trap_target_pc = Mux(trap, Cat(cur_excp_mtvec(31, 2), 0.U(2.W)), excp_flush_pc + excp_flush_ofst)
val trap_target_pc = Mux(trap_req, Cat(cur_excp_mtvec(31, 2), 0.U(2.W)), 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) {
when (trap_req || intr_taken) {
intr_pending := true.B
} .elsewhen (rvfi_valid) {
intr_pending := false.B
Expand All @@ -202,14 +210,17 @@ 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(trap || mret_taken, trap_target_pc,
rvfi_port.rvfi_pc_wdata := Mux(trap_req || 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)
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_addr := Mux(mem_rsp_hsked || data_access_fault, mem_addr, 0.U)
rvfi_port.rvfi_mem_rmask := Mux(data_access_fault, 0.U, Mux(mem_rsp_hsked, mem_rmask, 0.U))
rvfi_port.rvfi_mem_wmask := Mux(data_access_fault, 0.U, 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)
rvfi_port.rvfi_mem_wdata := Mux(mem_rsp_hsked || store_access_fault, mem_wdata, 0.U)
rvfi_port.rvfi_mem_fault := mem_fault
rvfi_port.rvfi_mem_fault_rmask := Mux(load_access_fault, mem_rmask, 0.U)
rvfi_port.rvfi_mem_fault_wmask := Mux(store_access_fault, mem_wmask, 0.U)

// ---- CSR channels ----
val wb_csr_idx = BoringUtils.bore(core.wbStage.io.csr_idx)
Expand Down
3 changes: 3 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 @@ -33,6 +33,9 @@ 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_mem_fault = Output(Bool())
val rvfi_mem_fault_rmask = Output(UInt(4.W))
val rvfi_mem_fault_wmask = Output(UInt(4.W))

val rvfi_csr_mstatus = new RVFICSR
val rvfi_csr_mie = new RVFICSR
Expand Down