M-Labs/riscv-formal-nmigen
6
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Tweak parameters for Minerva verification tasks

Browse Source
This commit is contained in:
Donald Sebastian Leung 2020-09-15 15:44:02 +08:00
parent a9f1431959
commit 0f4a2a76bd
3 changed files with 264 additions and 199 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

20
README.md
View File

@ -27,17 +27,31 @@ This should run the tests (cache, multiplier, divider) provided by Minerva itsel
$ python -m rvfi.cores.minerva.verify
```
This should run in the order of a few minutes.
This should run in the order of a few hours.
### Progress
- [ ] Instruction Checks (mostly passing)
- [ ] JAL failing at line 202
- [ ] LB, LH, LW, LBU, LHU, SB, SH, SW: Parser error - invalid slice
- [ ] SRL failing at line 201
- [x] PC forward checks
- [x] PC backward checks
- [x] Register checks
- [x] Causal checks
- [ ] Liveness checks
- [ ] Uniqueness checks
## Scope
The RV32I, RV32M, RV64I and RV64M ISAs are currently implemented but yet to be fully tested. Support for compressed instructions may be added in the future as time permits.
The RV32I, RV32M, RV64I and RV64M ISAs are currently implemented but only RV32IM are being tested by integrating with the Minerva core.
## Known Issues
- ~~21/08/2020: Verification passes unconditionally, even in the presence of obvious bugs. This is due to the `rvfi.valid` signal from the CPU being held at constant 0. Suitable instruction and data buses as well as interrupt signals have not been wired to Minerva which is likely preventing the core and verification from functioning properly~~
- ~~25/08/2020: Interrupts have been hardwired to zero and instruction/data buses attached to the Minerva core; however, running the verification quickly exhausts available memory on a machine with 32G RAM. Possible culprit: huge number of `Assume` statements on memory values~~
- 07/09/2020: Instruction checks fail at line 201 asserting the value of `rd_wdata`. At least we now have a proper failure instead of an unconditional pass or an out of memory issue. Whether the translated specs themselves are in error is under investigation.
- ~~07/09/2020: Instruction checks fail at line 201 asserting the value of `rd_wdata`. At least we now have a proper failure instead of an unconditional pass or an out of memory issue. Whether the translated specs themselves are in error is under investigation.~~
- 15/09/2020: Apart from the occasional failed assertion in specific verification tasks (likely due to bugs in translation), all of the memory-related instruction checks fail with a "parser error: invalid slice" preventing the assertions from ever running. The root cause of this issue is yet to be determined.
## License

47
failing_instructions.txt
View File

@ -1,47 +0,0 @@
Failing instructions:
- LUI (L200, 201, 202)
- AUIPC (L202)
- JAL (L202)
- JALR (L202)
- BEQ (L202)
- BNE (L202)
- BLT (L202)
- BGE (L202)
- BLTU (L202)
- BGEU (L202)
- LB (L202)
- LH (L202, 205, 215, 217)
- LW (L202, 205, 217)
- LBU (L202)
- LHU (L202, 205, 215, 217)
- SB (L202)
- SH (L202, 205, 209, 212, 217)
- SW (L202, 205, 217)
- ADDI (L202)
- SLTI (L202)
- SLTIU (L202)
- XORI (L200, 202)
- ORI (L202)
- ANDI (L202)
- SLLI (L200, 202)
- SRLI (L202)
- SRAI (L200, 202)
- ADD (L202)
- SUB (L202)
- SLL (L202)
- SLT (L200, 202)
- SLTU (L200, 202)
- XOR (L200, 202)
- SRL (L201)
- SRA (L202)
- OR (L202)
- AND (L202)
- MUL (L202, 217)
- MULH (L202, 217)
- MULHSU (L202, 217)
- MULHU (L202, 217)
- DIV (L202, 217)
- DIVU (L202, 217)
- REM (L202, 217)
- REMU (L202, 217)

396
rvfi/cores/minerva/verify.py
View File

@ -64,22 +64,36 @@ class InsnSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
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, False, True),
params=RISCVFormalParameters(32, 32, False, False, True, True),
insn_model=self.insn_model,
rvformal_addr_valid=lambda x:Const(1))
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
@ -111,160 +125,174 @@ class InsnSpec(Elaboratable):
class InsnTestCase(FHDLTestCase):
def verify(self):
print("Verifying LUI instruction ...")
self.assertFormal(InsnSpec(InsnLui), mode="cover", depth=40)
self.assertFormal(InsnSpec(InsnLui), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnAuipc), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnJal), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnJalr), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnBeq), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnBne), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnBlt), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnBge), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnBltu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnBgeu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnLb), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnLh), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnLw), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnLbu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnLhu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSb), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSh), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSw), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnAddi), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSlti), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSltiu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnXori), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnOri), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnAndi), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSlli), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSrli), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSrai), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnAdd), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSub), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSll), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSlt), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSltu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnXor), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSrl), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnSra), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnOr), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnAnd), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnMul), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnMulh), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnMulhsu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnMulhu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnDiv), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnDivu), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnRem), mode="bmc", depth=40)
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=40)
self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=40)
self.assertFormal(InsnSpec(InsnRemu), mode="cover", depth=20)
self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=20)
class PcFwdSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
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, False, True),
params=RISCVFormalParameters(32, 32, False, False, True, True),
rvformal_addr_valid=lambda x:Const(1))
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
@ -278,28 +306,42 @@ class PcFwdSpec(Elaboratable):
class PcFwdTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(PcFwdSpec(), mode="cover", depth=40)
self.assertFormal(PcFwdSpec(), mode="bmc", depth=40)
self.assertFormal(PcFwdSpec(), mode="cover", depth=20)
self.assertFormal(PcFwdSpec(), mode="bmc", depth=20)
class PcBwdSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
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, False, True),
params=RISCVFormalParameters(32, 32, False, False, True, True),
rvformal_addr_valid=lambda x:Const(1))
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
@ -313,26 +355,40 @@ class PcBwdSpec(Elaboratable):
class PcBwdTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(PcBwdSpec(), mode="cover", depth=40)
self.assertFormal(PcBwdSpec(), mode="bmc", depth=40)
self.assertFormal(PcBwdSpec(), mode="cover", depth=20)
self.assertFormal(PcBwdSpec(), mode="bmc", depth=20)
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, True))
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))
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
@ -350,26 +406,40 @@ class RegSpec(Elaboratable):
class RegTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(RegSpec(), mode="cover", depth=40)
self.assertFormal(RegSpec(), mode="bmc", depth=40)
self.assertFormal(RegSpec(), mode="cover", depth=10)
self.assertFormal(RegSpec(), mode="bmc", depth=10)
class CausalSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
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.causal_spec = causal_spec = CausalCheck()
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
@ -384,30 +454,44 @@ class CausalSpec(Elaboratable):
class CausalTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(CausalSpec(), mode="cover", depth=40)
self.assertFormal(CausalSpec(), mode="bmc", depth=40)
self.assertFormal(CausalSpec(), mode="cover", depth=20)
self.assertFormal(CausalSpec(), mode="bmc", depth=20)
class LivenessSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
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.liveness_spec = liveness_spec = LivenessCheck()
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
m.d.comb += liveness_spec.check.eq(AnySeq(1))
m.d.comb += liveness_spec.rvfi_valid.eq(cpu.rvfi.valid)
m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order)
@ -417,26 +501,40 @@ class LivenessSpec(Elaboratable):
class LivenessTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(LivenessSpec(), mode="cover", depth=40)
self.assertFormal(LivenessSpec(), mode="bmc", depth=40)
self.assertFormal(LivenessSpec(), mode="cover", depth=20)
self.assertFormal(LivenessSpec(), mode="bmc", depth=20)
class UniqueSpec(Elaboratable):
def elaborate(self, platform):
m = Module()
m.submodules.cpu = cpu = Minerva(with_rvfi=True)
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.unique_spec = unique_spec = UniqueCheck()
# Wire input ports to Minerva core
m.d.comb += cpu.external_interrupt.eq(AnySeq(32))
m.d.comb += cpu.timer_interrupt.eq(AnySeq(1))
m.d.comb += cpu.software_interrupt.eq(AnySeq(1))
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(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(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))
@ -449,8 +547,8 @@ class UniqueSpec(Elaboratable):
class UniqueTestCase(FHDLTestCase):
def verify(self):
self.assertFormal(UniqueSpec(), mode="cover", depth=40)
self.assertFormal(UniqueSpec(), mode="bmc", depth=40)
self.assertFormal(UniqueSpec(), mode="cover", depth=20)
self.assertFormal(UniqueSpec(), mode="bmc", depth=20)
print('*' * 80)
print('*' + ' ' * 78 + '*')