M-Labs
/
riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity
riscv-formal-nmigen/rvfi/cores/minerva/verify.py

440 lines
18 KiB
Python
Raw Normal View History

Remove copy of Minerva
2020-08-20 15:32:10 +08:00
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 *
Add liveness check
2020-08-21 12:54:53 +08:00
from ...checks.liveness_check import *
Add uniqueness check
2020-08-21 13:25:52 +08:00
from ...checks.unique_check import *
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
from minerva.core import *
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
from ...insns.isa_rv32i import *
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
from .memory_bus import *
Merge riscv_formal_parameters.py into verify.py
2020-08-24 10:20:30 +08:00
from collections import namedtuple
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem'])
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
class InsnSpec(Elaboratable):
def __init__(self, insn_model):
self.insn_model = insn_model
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
m.submodules.insn_spec = insn_spec = InsnCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
insn_model=self.insn_model,
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
rvformal_addr_valid=lambda x:Const(1))
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
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
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
class InsnTestCase(FHDLTestCase):
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
def verify(self):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(InsnSpec(IsaRV32I), mode="bmc", depth=40, engine="smtbmc --nopresat")
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
class PcFwdSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
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):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(PcFwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
class PcBwdSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
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):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(PcBwdSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
class RegSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, False))
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
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):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(RegSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
class CausalSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.causal_spec = causal_spec = CausalCheck()
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
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):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(CausalSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Add liveness check
2020-08-21 12:54:53 +08:00
class LivenessSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.liveness_spec = liveness_spec = LivenessCheck()
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Add liveness check
2020-08-21 12:54:53 +08:00
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):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(LivenessSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
Add liveness check
2020-08-21 12:54:53 +08:00
Add uniqueness check
2020-08-21 13:25:52 +08:00
class UniqueSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.unique_spec = unique_spec = UniqueCheck()
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone instruction bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.ibus = ibus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# Connect Wishbone data bus to Minerva CPU
Merge instruction and data bus abstractions
2020-08-25 10:12:02 +08:00
m.submodules.dbus = dbus = MemoryBus()
Wire instruction and data buses (WIP) to Minerva core
2020-08-24 14:46:52 +08:00
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)
Wire interrupt signals to Minerva for verification
2020-08-24 13:28:33 +08:00
# 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)
Add uniqueness check
2020-08-21 13:25:52 +08:00
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):
Replace individual instruction checks with ISA check
2020-08-21 15:14:42 +08:00
self.assertFormal(UniqueSpec(), mode="bmc", depth=40, engine="smtbmc --nopresat")
Add uniqueness check
2020-08-21 13:25:52 +08:00
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
print('*' * 80)
print('*' + ' ' * 78 + '*')
print('* Verifying the Minerva core ... *')
print('*' + ' ' * 78 + '*')
print('*' * 80)
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
print("Verifying RV32I instructions ...")
InsnTestCase().verify()
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
print("Verifying PC forward checks ...")
PcFwdTestCase().verify()
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
print("Verifying PC backward checks ...")
PcBwdTestCase().verify()
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
print("Verifying register checks ...")
RegTestCase().verify()
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Reduce code duplication in Minerva verification script
2020-08-21 11:43:20 +08:00
print("Verifying causal checks ...")
CausalTestCase().verify()
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
Add liveness check
2020-08-21 12:54:53 +08:00
print("Verifying liveness checks ...")
LivenessTestCase().verify()
Add uniqueness check
2020-08-21 13:25:52 +08:00
print("Verifying uniqueness checks ...")
UniqueTestCase().verify()
Remove copy of Minerva
2020-08-20 15:32:10 +08:00
print('*' * 80)
print('*' + ' ' * 78 + '*')
print('* All verification tasks successful! *')
print('*' + ' ' * 78 + '*')
print('*' * 80)