Wire interrupt signals to Minerva for verification

This commit is contained in:
Donald Sebastian Leung 2020-08-24 13:28:33 +08:00
parent ee80bff3db
commit 2a4f6dd07e

View File

@ -26,6 +26,15 @@ class InsnSpec(Elaboratable):
insn_model=self.insn_model,
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)
@ -66,6 +75,15 @@ class PcFwdSpec(Elaboratable):
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)
@ -89,6 +107,15 @@ class PcBwdSpec(Elaboratable):
params=RISCVFormalParameters(32, 32, False, False, False),
rvformal_addr_valid=lambda x:Const(1))
# Connect Wishbone instruction bus to Minerva CPU
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)
@ -110,6 +137,15 @@ class RegSpec(Elaboratable):
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
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)
@ -134,6 +170,15 @@ class CausalSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.causal_spec = causal_spec = CausalCheck()
# Connect Wishbone instruction bus to Minerva CPU
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)
@ -155,6 +200,15 @@ class LivenessSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.liveness_spec = liveness_spec = LivenessCheck()
# Connect Wishbone instruction bus to Minerva CPU
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)
@ -175,6 +229,15 @@ class UniqueSpec(Elaboratable):
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
m.submodules.unique_spec = unique_spec = UniqueCheck()
# Connect Wishbone instruction bus to Minerva CPU
# TODO
# Connect Wishbone data bus to Minerva CPU
# TODO
# 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)