diff --git a/checks/rvfi_imem_check.py b/checks/rvfi_imem_check.py new file mode 100644 index 0000000..304a988 --- /dev/null +++ b/checks/rvfi_imem_check.py @@ -0,0 +1,88 @@ +from nmigen import * +from nmigen.hdl.ast import * + +class rvfi_imem_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.imem_addr = Signal(self.RISCV_FORMAL_XLEN) + self.imem_data = Signal(16) + 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.imem_addr, + self.imem_data + ] + return input_ports + output_ports + def elaborate(self, platform): + m = Module() + + imem_addr_randval = AnyConst(self.RISCV_FORMAL_XLEN) + imem_data_randval = AnyConst(16) + m.d.comb += self.imem_addr.eq(imem_addr_randval) + m.d.comb += self.imem_data.eq(imem_data_randval) + + pc = Signal(self.RISCV_FORMAL_XLEN) + insn = Signal(self.RISCV_FORMAL_ILEN) + + with m.If(self.reset): + pass + with m.Else(): + with m.If(self.enable & self.rvfi_valid): + m.d.sync += pc.eq(self.rvfi_pc_rdata) + m.d.sync += insn.eq(self.rvfi_insn) + + with m.If(pc == self.imem_addr): + m.d.comb += Assert(insn[:16] == self.imem_data) + + with m.If((insn[:2] == 0b11) & (pc + 2 == self.imem_addr)): + m.d.comb += Assert(insn[16:32] == self.imem_data) + + return m