diff --git a/rvfi/checks/liveness_check.py b/rvfi/checks/liveness_check.py new file mode 100644 index 0000000..17ac00a --- /dev/null +++ b/rvfi/checks/liveness_check.py @@ -0,0 +1,46 @@ +from nmigen import * +from nmigen.asserts import * + +""" +Liveness Check +""" + +class LivenessCheck(Elaboratable): + def __init__(self): + self.reset = Signal(1) + self.rvfi_order = Signal(64) + self.trig = Signal(1) + self.rvfi_valid = Signal(1) + self.rvfi_halt = Signal(1) + self.check = Signal(1) + + def ports(self): + input_ports = [ + self.reset, + self.rvfi_order, + self.trig, + self.rvfi_valid, + self.rvfi_halt, + self.check + ] + return input_ports + + def elaborate(self, platform): + m = Module() + + insn_order = AnyConst(64) + found_next_insn = Signal(1, reset=0) + + with m.If(self.reset): + m.d.sync += found_next_insn.eq(0) + with m.Else(): + with m.If(self.rvfi_valid & (self.rvfi_order == insn_order + 1)): + m.d.sync += found_next_insn.eq(1) + with m.If(self.trig): + m.d.comb += Assume(self.rvfi_valid) + m.d.comb += Assume(~self.rvfi_halt) + m.d.comb += Assume(insn_order == self.rvfi_order) + with m.If(self.check): + m.d.comb += Assert(found_next_insn) + + return m diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index 792301c..8bc3b8b 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -4,6 +4,7 @@ from ...checks.pc_fwd_check import * from ...checks.pc_bwd_check import * from ...checks.reg_check import * from ...checks.causal_check import * +from ...checks.liveness_check import * from minerva.core import * from ...insns.insn_lui import * from ...insns.insn_auipc import * @@ -220,6 +221,26 @@ class CausalTestCase(FHDLTestCase): def verify(self): self.assertFormal(CausalSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") +class LivenessSpec(Elaboratable): + def elaborate(self, platform): + m = Module() + + m.submodules.cpu = cpu = Minerva(with_rvfi=True) + m.submodules.liveness_spec = liveness_spec = LivenessCheck() + + m.d.comb += liveness_spec.reset.eq(0) + m.d.comb += liveness_spec.rvfi_valid.eq(cpu.rvfi.valid) + m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order) + m.d.comb += liveness_spec.trig.eq(1) + m.d.comb += liveness_spec.rvfi_halt.eq(cpu.rvfi.halt) + m.d.comb += liveness_spec.check.eq(1) + + return m + +class LivenessTestCase(FHDLTestCase): + def verify(self): + self.assertFormal(LivenessSpec(), mode="bmc", depth=12, engine="smtbmc --nopresat") + print('*' * 80) print('*' + ' ' * 78 + '*') print('* Verifying the Minerva core ... *') @@ -241,6 +262,9 @@ RegTestCase().verify() print("Verifying causal checks ...") CausalTestCase().verify() +print("Verifying liveness checks ...") +LivenessTestCase().verify() + print('*' * 80) print('*' + ' ' * 78 + '*') print('* All verification tasks successful! *')