diff --git a/checks/rvfi_pc_fwd_check.py b/checks/rvfi_pc_fwd_check.py new file mode 100644 index 0000000..9fa5c61 --- /dev/null +++ b/checks/rvfi_pc_fwd_check.py @@ -0,0 +1,82 @@ +from nmigen import * +from nmigen.hdl.ast import * + +class rvfi_pc_fwd_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.check = Signal(1) + 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.check, + 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 = [] + return input_ports + output_ports + def elaborate(self, platform): + m = Module() + + insn_order = AnyConst(64) + expect_pc = Signal(self.RISCV_FORMAL_XLEN) + expect_pc_valid = Signal(1, reset=0) + + pc_rdata = Signal(self.RISCV_FORMAL_XLEN) + m.d.comb += pc_rdata.eq(self.rvfi_pc_rdata) + + with m.If(self.reset): + m.d.sync += expect_pc_valid.eq(0) + with m.Else(): + with m.If(self.check): + m.d.comb += Assume(self.rvfi_valid) + m.d.comb += Assume(insn_order == self.rvfi_order) + with m.If(expect_pc_valid): + m.d.comb += Assert(expect_pc == pc_rdata) + with m.Else(): + with m.If(self.rvfi_valid & (self.rvfi_order == insn_order - 1)): + m.d.sync += expect_pc.eq(self.rvfi_pc_wdata) + m.d.sync += expect_pc_valid.eq(1) + + return m