diff --git a/rvfi/checks/pc_fwd_check.py b/rvfi/checks/pc_fwd_check.py new file mode 100644 index 0000000..8407214 --- /dev/null +++ b/rvfi/checks/pc_fwd_check.py @@ -0,0 +1,57 @@ +from nmigen import * +from nmigen.asserts import * + +""" +PC Forward Check +""" + +class PcFwdCheck(Elaboratable): + def __init__(self, RISCV_FORMAL_XLEN, rvformal_addr_valid): + # Core-specific constants + self.RISCV_FORMAL_XLEN = RISCV_FORMAL_XLEN + + # Address validity and equality + self.rvformal_addr_valid = rvformal_addr_valid + self.rvformal_addr_eq = lambda a, b: (self.rvformal_addr_valid(a) == self.rvformal_addr_valid(b)) & ((~self.rvformal_addr_valid(a)) | (a == b)) + + # Input ports + self.reset = Signal(1) + self.check = Signal(1) + self.rvfi_valid = Signal(1) + self.rvfi_order = Signal(64) + self.rvfi_pc_rdata = Signal(self.RISCV_FORMAL_XLEN) + self.rvfi_pc_wdata = Signal(self.RISCV_FORMAL_XLEN) + def ports(self): + input_ports = [ + self.reset, + self.check, + self.rvfi_valid, + self.rvfi_order, + self.rvfi_pc_rdata, + self.rvfi_pc_wdata + ] + return input_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(self.rvformal_addr_eq(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 diff --git a/rvfi/cores/minerva/test/test_pc_forward.py b/rvfi/cores/minerva/test/test_pc_forward.py new file mode 100644 index 0000000..d43cf0c --- /dev/null +++ b/rvfi/cores/minerva/test/test_pc_forward.py @@ -0,0 +1,25 @@ +from nmigen import * +from nmigen.test.utils import * +from ..core import * +from ....checks.pc_fwd_check import * + +class PcFwdSpec(Elaboratable): + def elaborate(self, platform): + m = Module() + + m.submodules.cpu = cpu = Minerva(with_rvfi=True) + m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(RISCV_FORMAL_XLEN=32, rvformal_addr_valid=lambda x:Const(1)) + + m.d.comb += pc_fwd_spec.reset.eq(0) + m.d.comb += pc_fwd_spec.check.eq(1) + + m.d.comb += pc_fwd_spec.rvfi_valid.eq(cpu.rvfi.valid) + m.d.comb += pc_fwd_spec.rvfi_order.eq(cpu.rvfi.order) + m.d.comb += pc_fwd_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata) + m.d.comb += pc_fwd_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata) + + return m + +class PcFwdTestCase(FHDLTestCase): + def verify(self): + self.assertFormal(PcFwdSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index 9c4fcca..fe18bd7 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -1,6 +1,7 @@ import unittest from .test.test_cache import * from .test.test_instructions import * +from .test.test_pc_forward import * from .test.test_units_divider import * from .test.test_units_multiplier import * @@ -48,5 +49,8 @@ SraTestCase().verify() OrTestCase().verify() AndTestCase().verify() +print("Verifying PC forward checks ...") +PcFwdTestCase().verify() + print("Testing multiplier and divider ...") unittest.main()