diff --git a/checks/rvfi_hang_check.py b/checks/rvfi_hang_check.py new file mode 100644 index 0000000..acfc371 --- /dev/null +++ b/checks/rvfi_hang_check.py @@ -0,0 +1,77 @@ +from nmigen import * +from nmigen.hdl.ast import * + +class rvfi_hang_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.trig = 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.trig, + 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() + + okay = Signal(1, reset=0) + + with m.If(self.reset): + m.d.sync += okay.eq(0) + with m.Else(): + with m.If(self.rvfi_valid): + m.d.sync += okay.eq(1) + with m.If(self.check): + m.d.comb += Assert(okay) + with m.If(self.rvfi_valid): + m.d.comb += Assume(~self.rvfi_halt) + m.d.comb += Assume(self.rvfi_insn != 0b00010000010100000000000001110011) # WFI + + return m