riscv-formal-nmigen/rvfi/checks/reg_check.py

from nmigen import *
from nmigen.asserts import *

"""
Register Check
"""

class RegCheck(Elaboratable):
    def __init__(self, params):
        # Core-specific parameters
        self.params = params

        # Input ports
        self.reset = Signal(1)
        self.check = Signal(1)
        self.rvfi_valid = Signal(1)
        self.rvfi_order = Signal(64)
        self.rvfi_rs1_addr = Signal(5)
        self.rvfi_rs1_rdata = Signal(self.params.xlen)
        self.rvfi_rs2_addr = Signal(5)
        self.rvfi_rs2_rdata = Signal(self.params.xlen)
        self.rvfi_rd_addr = Signal(5)
        self.rvfi_rd_wdata = Signal(self.params.xlen)

    def ports(self):
        input_ports = [
            self.reset,
            self.check,
            self.rvfi_valid,
            self.rvfi_order,
            self.rvfi_rs1_addr,
            self.rvfi_rs1_rdata,
            self.rvfi_rs2_addr,
            self.rvfi_rs2_rdata,
            self.rvfi_rd_addr,
            self.rvfi_rd_wdata
        ]
        return input_ports

    def elaborate(self, platform):
        m = Module()

        insn_order = AnyConst(64)
        register_index = AnyConst(5)
        register_shadow = Signal(self.params.xlen, reset=0)
        register_written = Signal(1, reset=0)

        with m.If(self.reset):
            m.d.sync += register_shadow.eq(0)
            m.d.sync += register_written.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(register_written & (register_index == self.rvfi_rs1_addr)):
                    m.d.comb += Assert(register_shadow == self.rvfi_rs1_rdata)
                with m.If(register_written & (register_index == self.rvfi_rs2_addr)):
                    m.d.comb += Assert(register_shadow == self.rvfi_rs2_rdata)
            with m.Else():
                with m.If(self.rvfi_valid & (self.rvfi_order < insn_order) & (register_index == self.rvfi_rd_addr)):
                    m.d.sync += register_shadow.eq(self.rvfi_rd_wdata)
                    m.d.sync += register_written.eq(1)

        return m