riscv-formal-nmigen/rvfi/cores/minerva/verify.py

440 lines
18 KiB
Python

from nmigen.test.utils import *
from ...checks.insn_check import *
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 ...checks.unique_check import *
from minerva.core import *
from ...insns.isa_rv32i import *
from .memory_bus import *
from collections import namedtuple
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem'])
class InsnSpec(Elaboratable):
def __init__(self, insn_model):
self.insn_model = insn_model
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.insn_spec = insn_spec = InsnCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
insn_model=self.insn_model,
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
m.d.comb += insn_spec.reset.eq(0)
m.d.comb += insn_spec.check.eq(1)
m.d.comb += insn_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += insn_spec.rvfi_order.eq(cpu.rvfi.order)
m.d.comb += insn_spec.rvfi_insn.eq(cpu.rvfi.insn)
m.d.comb += insn_spec.rvfi_trap.eq(cpu.rvfi.trap)
m.d.comb += insn_spec.rvfi_halt.eq(cpu.rvfi.halt)
m.d.comb += insn_spec.rvfi_intr.eq(cpu.rvfi.intr)
m.d.comb += insn_spec.rvfi_mode.eq(cpu.rvfi.mode)
m.d.comb += insn_spec.rvfi_ixl.eq(cpu.rvfi.ixl)
m.d.comb += insn_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
m.d.comb += insn_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
m.d.comb += insn_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata)
m.d.comb += insn_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata)
m.d.comb += insn_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
m.d.comb += insn_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata)
m.d.comb += insn_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
m.d.comb += insn_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)
m.d.comb += insn_spec.rvfi_mem_addr.eq(cpu.rvfi.mem_addr)
m.d.comb += insn_spec.rvfi_mem_rmask.eq(cpu.rvfi.mem_rmask)
m.d.comb += insn_spec.rvfi_mem_wmask.eq(cpu.rvfi.mem_wmask)
m.d.comb += insn_spec.rvfi_mem_rdata.eq(cpu.rvfi.mem_rdata)
m.d.comb += insn_spec.rvfi_mem_wdata.eq(cpu.rvfi.mem_wdata)
return m
class InsnTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(InsnSpec(IsaRV32I), mode="bmc", depth=40, engine="smtbmc --nopresat")
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(
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
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=40, engine="smtbmc --nopresat")
class PcBwdSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
m.d.comb += pc_bwd_spec.reset.eq(0)
m.d.comb += pc_bwd_spec.check.eq(1)
m.d.comb += pc_bwd_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += pc_bwd_spec.rvfi_order.eq(cpu.rvfi.order)
m.d.comb += pc_bwd_spec.rvfi_pc_rdata.eq(cpu.rvfi.pc_rdata)
m.d.comb += pc_bwd_spec.rvfi_pc_wdata.eq(cpu.rvfi.pc_wdata)
return m
class PcBwdTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(PcBwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class RegSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False))
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
m.d.comb += reg_spec.reset.eq(0)
m.d.comb += reg_spec.check.eq(1)
m.d.comb += reg_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += reg_spec.rvfi_order.eq(cpu.rvfi.order)
m.d.comb += reg_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
m.d.comb += reg_spec.rvfi_rs1_rdata.eq(cpu.rvfi.rs1_rdata)
m.d.comb += reg_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
m.d.comb += reg_spec.rvfi_rs2_rdata.eq(cpu.rvfi.rs2_rdata)
m.d.comb += reg_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
m.d.comb += reg_spec.rvfi_rd_wdata.eq(cpu.rvfi.rd_wdata)
return m
class RegTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(RegSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
class CausalSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.causal_spec = causal_spec = CausalCheck()
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
m.d.comb += causal_spec.reset.eq(0)
m.d.comb += causal_spec.check.eq(1)
m.d.comb += causal_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += causal_spec.rvfi_rd_addr.eq(cpu.rvfi.rd_addr)
m.d.comb += causal_spec.rvfi_order.eq(cpu.rvfi.order)
m.d.comb += causal_spec.rvfi_rs1_addr.eq(cpu.rvfi.rs1_addr)
m.d.comb += causal_spec.rvfi_rs2_addr.eq(cpu.rvfi.rs2_addr)
return m
class CausalTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(CausalSpec(), mode="bmc", depth=40, 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()
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
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=40, engine="smtbmc --nopresat")
class UniqueSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.unique_spec = unique_spec = UniqueCheck()
# Connect Wishbone instruction bus to Minerva CPU
m.submodules.ibus = ibus = MemoryBus()
m.d.comb += ibus.adr.eq(cpu.ibus.adr)
m.d.comb += ibus.dat_w.eq(cpu.ibus.dat_w)
m.d.comb += cpu.ibus.dat_r.eq(ibus.dat_r)
m.d.comb += ibus.sel.eq(cpu.ibus.sel)
m.d.comb += ibus.cyc.eq(cpu.ibus.cyc)
m.d.comb += ibus.stb.eq(cpu.ibus.stb)
m.d.comb += cpu.ibus.ack.eq(ibus.ack)
m.d.comb += ibus.we.eq(cpu.ibus.we)
m.d.comb += ibus.cti.eq(cpu.ibus.cti)
m.d.comb += ibus.bte.eq(cpu.ibus.bte)
m.d.comb += cpu.ibus.err.eq(ibus.err)
# Connect Wishbone data bus to Minerva CPU
m.submodules.dbus = dbus = MemoryBus()
m.d.comb += dbus.adr.eq(cpu.dbus.adr)
m.d.comb += dbus.dat_w.eq(cpu.dbus.dat_w)
m.d.comb += cpu.dbus.dat_r.eq(dbus.dat_r)
m.d.comb += dbus.sel.eq(cpu.dbus.sel)
m.d.comb += dbus.cyc.eq(cpu.dbus.cyc)
m.d.comb += dbus.stb.eq(cpu.dbus.stb)
m.d.comb += cpu.dbus.ack.eq(dbus.ack)
m.d.comb += dbus.we.eq(cpu.dbus.we)
m.d.comb += dbus.cti.eq(cpu.dbus.cti)
m.d.comb += dbus.bte.eq(cpu.dbus.bte)
m.d.comb += cpu.dbus.err.eq(dbus.err)
# Disable all interrupts
m.d.comb += cpu.external_interrupt.eq(0)
m.d.comb += cpu.timer_interrupt.eq(0)
m.d.comb += cpu.software_interrupt.eq(0)
m.d.comb += unique_spec.reset.eq(0)
m.d.comb += unique_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order)
m.d.comb += unique_spec.trig.eq(1)
m.d.comb += unique_spec.check.eq(1)
return m
class UniqueTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(UniqueSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
print('*' * 80)
print('*' + ' ' * 78 + '*')
print('* Verifying the Minerva core ... *')
print('*' + ' ' * 78 + '*')
print('*' * 80)
print("Verifying RV32I instructions ...")
InsnTestCase().verify()
print("Verifying PC forward checks ...")
PcFwdTestCase().verify()
print("Verifying PC backward checks ...")
PcBwdTestCase().verify()
print("Verifying register checks ...")
RegTestCase().verify()
print("Verifying causal checks ...")
CausalTestCase().verify()
print("Verifying liveness checks ...")
LivenessTestCase().verify()
print("Verifying uniqueness checks ...")
UniqueTestCase().verify()
print('*' * 80)
print('*' + ' ' * 78 + '*')
print('* All verification tasks successful! *')
print('*' + ' ' * 78 + '*')
print('*' * 80)