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

601 lines
24 KiB
Python
Raw Normal View History

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 *
2020-08-21 12:54:53 +08:00
from ...checks.liveness_check import *
2020-08-21 13:25:52 +08:00
from ...checks.unique_check import *
2020-08-20 15:32:10 +08:00
from minerva.core import *
from ...insns.insn_lui import *
from ...insns.insn_auipc import *
from ...insns.insn_jal import *
from ...insns.insn_jalr import *
from ...insns.insn_beq import *
from ...insns.insn_bne import *
from ...insns.insn_blt import *
from ...insns.insn_bge import *
from ...insns.insn_bltu import *
from ...insns.insn_bgeu import *
from ...insns.insn_lb import *
from ...insns.insn_lh import *
from ...insns.insn_lw import *
from ...insns.insn_lbu import *
from ...insns.insn_lhu import *
from ...insns.insn_sb import *
from ...insns.insn_sh import *
from ...insns.insn_sw import *
from ...insns.insn_addi import *
from ...insns.insn_slti import *
from ...insns.insn_sltiu import *
from ...insns.insn_xori import *
from ...insns.insn_ori import *
from ...insns.insn_andi import *
from ...insns.insn_slli import *
from ...insns.insn_srli import *
from ...insns.insn_srai import *
from ...insns.insn_add import *
from ...insns.insn_sub import *
from ...insns.insn_sll import *
from ...insns.insn_slt import *
from ...insns.insn_sltu import *
from ...insns.insn_xor import *
from ...insns.insn_srl import *
from ...insns.insn_sra import *
from ...insns.insn_or import *
from ...insns.insn_and import *
from ...insns.insn_mul import *
from ...insns.insn_mulh import *
from ...insns.insn_mulhsu import *
from ...insns.insn_mulhu import *
from ...insns.insn_div import *
from ...insns.insn_divu import *
from ...insns.insn_rem import *
from ...insns.insn_remu import *
from collections import namedtuple
RISCVFormalParameters = namedtuple('RISCVFormalParameters',
['ilen', 'xlen', 'csr_misa', 'compressed', 'aligned_mem', 'altops'])
2020-08-20 15:32:10 +08:00
class InsnSpec(Elaboratable):
def __init__(self, insn_model):
self.insn_model = insn_model
2020-08-20 15:32:10 +08:00
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(
with_rvfi=True,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
m.submodules.insn_spec = insn_spec = InsnCheck(
params=RISCVFormalParameters(32, 32, False, False, True, True),
insn_model=self.insn_model,
2020-08-20 15:32:10 +08:00
rvformal_addr_valid=lambda x:Const(1))
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += insn_spec.reset.eq(AnySeq(1))
m.d.comb += insn_spec.check.eq(AnySeq(1))
2020-08-20 15:32:10 +08:00
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):
2020-08-20 15:32:10 +08:00
def verify(self):
print("Verifying LUI instruction ...")
self.assertFormal(InsnSpec(InsnLui), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLui), mode="bmc", depth=20)
print("Verifying AUIPC instruction ...")
self.assertFormal(InsnSpec(InsnAuipc), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAuipc), mode="bmc", depth=20)
print("Verifying JAL instruction ...")
self.assertFormal(InsnSpec(InsnJal), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnJal), mode="bmc", depth=20)
print("Verifying JALR instruction ...")
self.assertFormal(InsnSpec(InsnJalr), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnJalr), mode="bmc", depth=20)
print("Verifying BEQ instruction ...")
self.assertFormal(InsnSpec(InsnBeq), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBeq), mode="bmc", depth=20)
print("Verifying BNE instruction ...")
self.assertFormal(InsnSpec(InsnBne), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBne), mode="bmc", depth=20)
print("Verifying BLT instruction ...")
self.assertFormal(InsnSpec(InsnBlt), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBlt), mode="bmc", depth=20)
print("Verifying BGE instruction ...")
self.assertFormal(InsnSpec(InsnBge), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBge), mode="bmc", depth=20)
print("Verifying BLTU instruction ...")
self.assertFormal(InsnSpec(InsnBltu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBltu), mode="bmc", depth=20)
print("Verifying BGEU instruction ...")
self.assertFormal(InsnSpec(InsnBgeu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnBgeu), mode="bmc", depth=20)
print("Verifying LB instruction ...")
self.assertFormal(InsnSpec(InsnLb), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLb), mode="bmc", depth=20)
print("Verifying LH instruction ...")
self.assertFormal(InsnSpec(InsnLh), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLh), mode="bmc", depth=20)
print("Verifying LW instruction ...")
self.assertFormal(InsnSpec(InsnLw), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLw), mode="bmc", depth=20)
print("Verifying LBU instruction ...")
self.assertFormal(InsnSpec(InsnLbu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLbu), mode="bmc", depth=20)
print("Verifying LHU instruction ...")
self.assertFormal(InsnSpec(InsnLhu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnLhu), mode="bmc", depth=20)
print("Verifying SB instruction ...")
self.assertFormal(InsnSpec(InsnSb), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSb), mode="bmc", depth=20)
print("Verifying SH instruction ...")
self.assertFormal(InsnSpec(InsnSh), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSh), mode="bmc", depth=20)
print("Verifying SW instruction ...")
self.assertFormal(InsnSpec(InsnSw), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSw), mode="bmc", depth=20)
print("Verifying ADDI instruction ...")
self.assertFormal(InsnSpec(InsnAddi), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAddi), mode="bmc", depth=20)
print("Verifying SLTI instruction ...")
self.assertFormal(InsnSpec(InsnSlti), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSlti), mode="bmc", depth=20)
print("Verifying SLTIU instruction ...")
self.assertFormal(InsnSpec(InsnSltiu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSltiu), mode="bmc", depth=20)
print("Verifying XORI instruction ...")
self.assertFormal(InsnSpec(InsnXori), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnXori), mode="bmc", depth=20)
print("Verifying ORI instruction ...")
self.assertFormal(InsnSpec(InsnOri), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnOri), mode="bmc", depth=20)
print("Verifying ANDI instruction ...")
self.assertFormal(InsnSpec(InsnAndi), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAndi), mode="bmc", depth=20)
print("Verifying SLLI instruction ...")
self.assertFormal(InsnSpec(InsnSlli), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSlli), mode="bmc", depth=20)
print("Verifying SRLI instruction ...")
self.assertFormal(InsnSpec(InsnSrli), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSrli), mode="bmc", depth=20)
print("Verifying SRAI instruction ...")
self.assertFormal(InsnSpec(InsnSrai), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSrai), mode="bmc", depth=20)
print("Verifying ADD instruction ...")
self.assertFormal(InsnSpec(InsnAdd), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAdd), mode="bmc", depth=20)
print("Verifying SUB instruction ...")
self.assertFormal(InsnSpec(InsnSub), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSub), mode="bmc", depth=20)
print("Verifying SLL instruction ...")
self.assertFormal(InsnSpec(InsnSll), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSll), mode="bmc", depth=20)
print("Verifying SLT instruction ...")
self.assertFormal(InsnSpec(InsnSlt), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSlt), mode="bmc", depth=20)
print("Verifying SLTU instruction ...")
self.assertFormal(InsnSpec(InsnSltu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSltu), mode="bmc", depth=20)
print("Verifying XOR instruction ...")
self.assertFormal(InsnSpec(InsnXor), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnXor), mode="bmc", depth=20)
print("Verifying SRL instruction ...")
self.assertFormal(InsnSpec(InsnSrl), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSrl), mode="bmc", depth=20)
print("Verifying SRA instruction ...")
self.assertFormal(InsnSpec(InsnSra), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnSra), mode="bmc", depth=20)
print("Verifying OR instruction ...")
self.assertFormal(InsnSpec(InsnOr), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnOr), mode="bmc", depth=20)
print("Verifying AND instruction ...")
self.assertFormal(InsnSpec(InsnAnd), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnAnd), mode="bmc", depth=20)
print("Verifying MUL instruction ...")
self.assertFormal(InsnSpec(InsnMul), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMul), mode="bmc", depth=20)
print("Verifying MULH instruction ...")
self.assertFormal(InsnSpec(InsnMulh), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMulh), mode="bmc", depth=20)
print("Verifying MULHSU instruction ...")
self.assertFormal(InsnSpec(InsnMulhsu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMulhsu), mode="bmc", depth=20)
print("Verifying MULHU instruction ...")
self.assertFormal(InsnSpec(InsnMulhu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnMulhu), mode="bmc", depth=20)
print("Verifying DIV instruction ...")
self.assertFormal(InsnSpec(InsnDiv), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnDiv), mode="bmc", depth=20)
print("Verifying DIVU instruction ...")
self.assertFormal(InsnSpec(InsnDivu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnDivu), mode="bmc", depth=20)
print("Verifying REM instruction ...")
self.assertFormal(InsnSpec(InsnRem), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnRem), mode="bmc", depth=20)
print("Verifying REMU instruction ...")
self.assertFormal(InsnSpec(InsnRemu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=20)
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,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
m.submodules.pc_fwd_spec = pc_fwd_spec = PcFwdCheck(
params=RISCVFormalParameters(32, 32, False, False, True, True),
rvformal_addr_valid=lambda x:Const(1))
2020-08-20 15:32:10 +08:00
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += pc_fwd_spec.reset.eq(AnySeq(1))
m.d.comb += pc_fwd_spec.check.eq(AnySeq(1))
2020-08-20 15:32:10 +08:00
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="cover", depth=20)
self.assertFormal(PcFwdSpec(), mode="bmc", depth=20)
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,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
m.submodules.pc_bwd_spec = pc_bwd_spec = PcBwdCheck(
params=RISCVFormalParameters(32, 32, False, False, True, True),
rvformal_addr_valid=lambda x:Const(1))
2020-08-20 15:32:10 +08:00
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += pc_bwd_spec.reset.eq(AnySeq(1))
m.d.comb += pc_bwd_spec.check.eq(AnySeq(1))
2020-08-20 15:32:10 +08:00
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="cover", depth=20)
self.assertFormal(PcBwdSpec(), mode="bmc", depth=20)
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,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
m.submodules.reg_spec = reg_spec = RegCheck(params=RISCVFormalParameters(32, 32, False, False, True, True))
2020-08-20 15:32:10 +08:00
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += reg_spec.reset.eq(AnySeq(1))
m.d.comb += reg_spec.check.eq(AnySeq(1))
2020-08-20 15:32:10 +08:00
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="cover", depth=10)
self.assertFormal(RegSpec(), mode="bmc", depth=10)
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,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
2020-08-20 15:32:10 +08:00
m.submodules.causal_spec = causal_spec = CausalCheck()
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += causal_spec.reset.eq(AnySeq(1))
m.d.comb += causal_spec.check.eq(AnySeq(1))
2020-08-20 15:32:10 +08:00
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="cover", depth=20)
self.assertFormal(CausalSpec(), mode="bmc", depth=20)
2020-08-20 15:32:10 +08:00
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,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
2020-08-21 12:54:53 +08:00
m.submodules.liveness_spec = liveness_spec = LivenessCheck()
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += liveness_spec.reset.eq(AnySeq(1))
m.d.comb += liveness_spec.trig.eq(AnySeq(1))
m.d.comb += liveness_spec.check.eq(AnySeq(1))
2020-08-21 12:54:53 +08:00
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.rvfi_halt.eq(cpu.rvfi.halt)
# Bounded fairness constraints
ibus_wait = Signal(2, reset=0)
dbus_wait = Signal(2, reset=0)
with m.If(cpu.ibus.cyc & cpu.ibus.stb & ~(cpu.ibus.ack | cpu.ibus.err)):
m.d.sync += ibus_wait.eq(ibus_wait + 1)
with m.Else():
m.d.sync += ibus_wait.eq(0)
with m.If(cpu.dbus.cyc & cpu.dbus.stb & ~(cpu.dbus.ack | cpu.dbus.err)):
m.d.sync += dbus_wait.eq(dbus_wait + 1)
with m.Else():
m.d.sync += dbus_wait.eq(0)
m.d.comb += Assume((ibus_wait < 2) & (dbus_wait < 2))
with m.If(liveness_spec.reset):
m.d.sync += ibus_wait.eq(0)
m.d.sync += dbus_wait.eq(0)
2020-08-21 12:54:53 +08:00
return m
class LivenessTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(LivenessSpec(), mode="cover", depth=20)
self.assertFormal(LivenessSpec(), mode="bmc", depth=20)
2020-08-21 12:54:53 +08:00
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,
with_muldiv=True,
with_icache=True,
icache_nways=2,
icache_nlines=2,
icache_nwords=4,
icache_base=0x1000,
icache_limit=0x4000,
with_dcache=True,
dcache_nways=2,
dcache_nlines=2,
dcache_nwords=4,
dcache_base=0x1000,
dcache_limit=0x4000)
2020-08-21 13:25:52 +08:00
m.submodules.unique_spec = unique_spec = UniqueCheck()
# Wire input ports to Minerva core
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 += cpu.ibus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.ibus.ack.eq(AnySeq(1))
m.d.comb += cpu.ibus.err.eq(0)
m.d.comb += cpu.dbus.dat_r.eq(AnySeq(32))
m.d.comb += cpu.dbus.ack.eq(AnySeq(1))
m.d.comb += cpu.dbus.err.eq(0)
m.d.comb += unique_spec.reset.eq(AnySeq(1))
m.d.comb += unique_spec.trig.eq(AnySeq(1))
m.d.comb += unique_spec.check.eq(AnySeq(1))
2020-08-21 13:25:52 +08:00
m.d.comb += unique_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += unique_spec.rvfi_order.eq(cpu.rvfi.order)
return m
class UniqueTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(UniqueSpec(), mode="cover", depth=20)
self.assertFormal(UniqueSpec(), mode="bmc", depth=20)
2020-08-21 13:25:52 +08:00
2020-08-20 15:32:10 +08:00
print('*' * 80)
print('*' + ' ' * 78 + '*')
print('* Verifying the Minerva core ... *')
print('*' + ' ' * 78 + '*')
print('*' * 80)
print("Verifying RV32M instructions ...")
InsnTestCase().verify()
2020-08-20 15:32:10 +08:00
print("Verifying PC forward checks ...")
PcFwdTestCase().verify()
2020-08-20 15:32:10 +08:00
print("Verifying PC backward checks ...")
PcBwdTestCase().verify()
2020-08-20 15:32:10 +08:00
print("Verifying register checks ...")
RegTestCase().verify()
2020-08-20 15:32:10 +08:00
print("Verifying causal checks ...")
CausalTestCase().verify()
2020-08-20 15:32:10 +08:00
2020-08-21 12:54:53 +08:00
print("Verifying liveness checks ...")
LivenessTestCase().verify()
2020-08-21 13:25:52 +08:00
print("Verifying uniqueness checks ...")
UniqueTestCase().verify()
2020-08-20 15:32:10 +08:00
print('*' * 80)
print('*' + ' ' * 78 + '*')
print('* All verification tasks successful! *')
print('*' + ' ' * 78 + '*')
print('*' * 80)