diff --git a/checks/rvfi_dmem_check.py b/checks/rvfi_dmem_check.py new file mode 100644 index 0000000..4444ed7 --- /dev/null +++ b/checks/rvfi_dmem_check.py @@ -0,0 +1,82 @@ +from nmigen import * +from nmigen.hdl.ast import * + +class rvfi_dmem_check(Elaboratable): + def __init__(self, RISCV_FORMAL_ILEN=32, RISCV_FORMAL_XLEN=32): + self.RISCV_FORMAL_ILEN = RISCV_FORMAL_ILEN + self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN + self.reset = Signal(1) + self.enable = Signal(1) + self.dmem_addr = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_valid = Signal(1) + self.rvfi_order = Signal(64) + self.rvfi_insn = Signal(self.RISCV_FORMAL_ILEN) + self.rvfi_trap = Signal(1) + self.rvfi_halt = Signal(1) + self.rvfi_intr = Signal(1) + self.rvfi_mode = Signal(2) + self.rvfi_ixl = Signal(2) + self.rvfi_rs1_addr = Signal(5) + self.rvfi_rs2_addr = Signal(5) + self.rvfi_rs1_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rs2_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_rd_addr = Signal(5) + self.rvfi_rd_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_mem_addr = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_mem_rmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) + self.rvfi_mem_wmask = Signal(int(self.RISCV_FORMAL_XLEN // 8)) + self.rvfi_mem_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_mem_wdata = Signal(self.RISCV_FORMAL_XLEN) + def ports(self): + input_ports = [ + self.reset, + self.enable, + self.rvfi_valid, + self.rvfi_order, + self.rvfi_insn, + self.rvfi_trap, + self.rvfi_halt, + self.rvfi_intr, + self.rvfi_mode, + self.rvfi_ixl, + self.rvfi_rs1_addr, + self.rvfi_rs2_addr, + self.rvfi_rs1_rdata, + self.rvfi_rs2_rdata, + self.rvfi_rd_addr, + self.rvfi_rd_wdata, + self.rvfi_pc_rdata, + self.rvfi_pc_wdata, + self.rvfi_mem_addr, + self.rvfi_mem_rmask, + self.rvfi_mem_wmask, + self.rvfi_mem_rdata, + self.rvfi_mem_wdata + ] + output_ports = [ + self.dmem_addr + ] + return input_ports + output_ports + def elaborate(self, platform): + m = Module() + + dmem_addr_randval = AnyConst(self.RISCV_FORMAL_XLEN) + m.d.comb += self.dmem_addr.eq(dmem_addr_randval) + + dmem_shadow = Signal(self.RISCV_FORMAL_XLEN) + dmem_written = Signal(int(self.RISCV_FORMAL_XLEN // 8), reset=0) + + with m.If(self.reset): + m.d.sync += dmem_written.eq(0) + with m.Else(): + with m.If(self.rvfi_valid & (self.rvfi_mem_addr == self.dmem_addr) & 1): + for i in range(int(self.RISCV_FORMAL_XLEN // 8)): + with m.If(self.enable & self.rvfi_mem_rmask[i] & dmem_written[i]): + m.d.comb += Assert(dmem_shadow[i*8:i*8+8] == self.rvfi_mem_rdata[i*8:i*8+8]) + with m.If(self.rvfi_mem_wmask[i]): + m.d.sync += dmem_shadow[i*8:i*8+8].eq(self.rvfi_mem_wdata[i*8:i*8+8]) + m.d.sync += dmem_written[i].eq(1) + + return m