From 32388adce0f5d3b37970cce1abb2e51578d069af Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Thu, 17 Sep 2020 13:22:52 +0800 Subject: [PATCH] Make liveness checks pass --- README.md | 2 +- rvfi/cores/minerva/verify.py | 96 ++++++++++++++++++------------------ 2 files changed, 49 insertions(+), 49 deletions(-) diff --git a/README.md b/README.md index 1f55f2b..98b495e 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ This should run in the order of a few hours. - [x] PC backward checks - [x] Register checks - [x] Causal checks -- [ ] Liveness checks +- [x] Liveness checks - [x] Uniqueness checks ## Scope diff --git a/rvfi/cores/minerva/verify.py b/rvfi/cores/minerva/verify.py index c31cfad..d2dede2 100644 --- a/rvfi/cores/minerva/verify.py +++ b/rvfi/cores/minerva/verify.py @@ -124,139 +124,139 @@ class InsnSpec(Elaboratable): class InsnTestCase(FHDLTestCase): def verify(self): - print("Verifying LUI instruction ...") + print("- Verifying LUI instruction ...") self.assertFormal(InsnSpec(InsnLui), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnLui), mode="bmc", depth=20) - print("Verifying AUIPC instruction ...") + print("- Verifying AUIPC instruction ...") self.assertFormal(InsnSpec(InsnAuipc), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnAuipc), mode="bmc", depth=20) - print("Verifying JAL instruction ...") + print("- Verifying JAL instruction ...") self.assertFormal(InsnSpec(InsnJal), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnJal), mode="bmc", depth=20) - print("Verifying JALR instruction ...") + print("- Verifying JALR instruction ...") self.assertFormal(InsnSpec(InsnJalr), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnJalr), mode="bmc", depth=20) - print("Verifying BEQ instruction ...") + print("- Verifying BEQ instruction ...") self.assertFormal(InsnSpec(InsnBeq), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnBeq), mode="bmc", depth=20) - print("Verifying BNE instruction ...") + print("- Verifying BNE instruction ...") self.assertFormal(InsnSpec(InsnBne), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnBne), mode="bmc", depth=20) - print("Verifying BLT instruction ...") + print("- Verifying BLT instruction ...") self.assertFormal(InsnSpec(InsnBlt), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnBlt), mode="bmc", depth=20) - print("Verifying BGE instruction ...") + print("- Verifying BGE instruction ...") self.assertFormal(InsnSpec(InsnBge), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnBge), mode="bmc", depth=20) - print("Verifying BLTU instruction ...") + print("- Verifying BLTU instruction ...") self.assertFormal(InsnSpec(InsnBltu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnBltu), mode="bmc", depth=20) - print("Verifying BGEU instruction ...") + print("- Verifying BGEU instruction ...") self.assertFormal(InsnSpec(InsnBgeu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnBgeu), mode="bmc", depth=20) - print("Verifying LB instruction ...") + print("- Verifying LB instruction ...") self.assertFormal(InsnSpec(InsnLb), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnLb), mode="bmc", depth=20) - print("Verifying LH instruction ...") + print("- Verifying LH instruction ...") self.assertFormal(InsnSpec(InsnLh), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnLh), mode="bmc", depth=20) - print("Verifying LW instruction ...") + print("- Verifying LW instruction ...") self.assertFormal(InsnSpec(InsnLw), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnLw), mode="bmc", depth=20) - print("Verifying LBU instruction ...") + print("- Verifying LBU instruction ...") self.assertFormal(InsnSpec(InsnLbu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnLbu), mode="bmc", depth=20) - print("Verifying LHU instruction ...") + print("- Verifying LHU instruction ...") self.assertFormal(InsnSpec(InsnLhu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnLhu), mode="bmc", depth=20) - print("Verifying SB instruction ...") + print("- Verifying SB instruction ...") self.assertFormal(InsnSpec(InsnSb), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSb), mode="bmc", depth=20) - print("Verifying SH instruction ...") + print("- Verifying SH instruction ...") self.assertFormal(InsnSpec(InsnSh), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSh), mode="bmc", depth=20) - print("Verifying SW instruction ...") + print("- Verifying SW instruction ...") self.assertFormal(InsnSpec(InsnSw), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSw), mode="bmc", depth=20) - print("Verifying ADDI instruction ...") + print("- Verifying ADDI instruction ...") self.assertFormal(InsnSpec(InsnAddi), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnAddi), mode="bmc", depth=20) - print("Verifying SLTI instruction ...") + print("- Verifying SLTI instruction ...") self.assertFormal(InsnSpec(InsnSlti), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSlti), mode="bmc", depth=20) - print("Verifying SLTIU instruction ...") + print("- Verifying SLTIU instruction ...") self.assertFormal(InsnSpec(InsnSltiu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSltiu), mode="bmc", depth=20) - print("Verifying XORI instruction ...") + print("- Verifying XORI instruction ...") self.assertFormal(InsnSpec(InsnXori), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnXori), mode="bmc", depth=20) - print("Verifying ORI instruction ...") + print("- Verifying ORI instruction ...") self.assertFormal(InsnSpec(InsnOri), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnOri), mode="bmc", depth=20) - print("Verifying ANDI instruction ...") + print("- Verifying ANDI instruction ...") self.assertFormal(InsnSpec(InsnAndi), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnAndi), mode="bmc", depth=20) - print("Verifying SLLI instruction ...") + print("- Verifying SLLI instruction ...") self.assertFormal(InsnSpec(InsnSlli), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSlli), mode="bmc", depth=20) - print("Verifying SRLI instruction ...") + print("- Verifying SRLI instruction ...") self.assertFormal(InsnSpec(InsnSrli), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSrli), mode="bmc", depth=20) - print("Verifying SRAI instruction ...") + print("- Verifying SRAI instruction ...") self.assertFormal(InsnSpec(InsnSrai), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSrai), mode="bmc", depth=20) - print("Verifying ADD instruction ...") + print("- Verifying ADD instruction ...") self.assertFormal(InsnSpec(InsnAdd), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnAdd), mode="bmc", depth=20) - print("Verifying SUB instruction ...") + print("- Verifying SUB instruction ...") self.assertFormal(InsnSpec(InsnSub), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSub), mode="bmc", depth=20) - print("Verifying SLL instruction ...") + print("- Verifying SLL instruction ...") self.assertFormal(InsnSpec(InsnSll), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSll), mode="bmc", depth=20) - print("Verifying SLT instruction ...") + print("- Verifying SLT instruction ...") self.assertFormal(InsnSpec(InsnSlt), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSlt), mode="bmc", depth=20) - print("Verifying SLTU instruction ...") + print("- Verifying SLTU instruction ...") self.assertFormal(InsnSpec(InsnSltu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSltu), mode="bmc", depth=20) - print("Verifying XOR instruction ...") + print("- Verifying XOR instruction ...") self.assertFormal(InsnSpec(InsnXor), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnXor), mode="bmc", depth=20) - print("Verifying SRL instruction ...") + print("- Verifying SRL instruction ...") self.assertFormal(InsnSpec(InsnSrl), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSrl), mode="bmc", depth=20) - print("Verifying SRA instruction ...") + print("- Verifying SRA instruction ...") self.assertFormal(InsnSpec(InsnSra), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnSra), mode="bmc", depth=20) - print("Verifying OR instruction ...") + print("- Verifying OR instruction ...") self.assertFormal(InsnSpec(InsnOr), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnOr), mode="bmc", depth=20) - print("Verifying AND instruction ...") + print("- Verifying AND instruction ...") self.assertFormal(InsnSpec(InsnAnd), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnAnd), mode="bmc", depth=20) - print("Verifying MUL instruction ...") + print("- Verifying MUL instruction ...") self.assertFormal(InsnSpec(InsnMul), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnMul), mode="bmc", depth=20) - print("Verifying MULH instruction ...") + print("- Verifying MULH instruction ...") self.assertFormal(InsnSpec(InsnMulh), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnMulh), mode="bmc", depth=20) - print("Verifying MULHSU instruction ...") + print("- Verifying MULHSU instruction ...") self.assertFormal(InsnSpec(InsnMulhsu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnMulhsu), mode="bmc", depth=20) - print("Verifying MULHU instruction ...") + print("- Verifying MULHU instruction ...") self.assertFormal(InsnSpec(InsnMulhu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnMulhu), mode="bmc", depth=20) - print("Verifying DIV instruction ...") + print("- Verifying DIV instruction ...") self.assertFormal(InsnSpec(InsnDiv), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnDiv), mode="bmc", depth=20) - print("Verifying DIVU instruction ...") + print("- Verifying DIVU instruction ...") self.assertFormal(InsnSpec(InsnDivu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnDivu), mode="bmc", depth=20) - print("Verifying REM instruction ...") + print("- Verifying REM instruction ...") self.assertFormal(InsnSpec(InsnRem), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnRem), mode="bmc", depth=20) - print("Verifying REMU instruction ...") + print("- Verifying REMU instruction ...") self.assertFormal(InsnSpec(InsnRemu), mode="cover", depth=20) self.assertFormal(InsnSpec(InsnRemu), mode="bmc", depth=20) @@ -494,7 +494,7 @@ class LivenessSpec(Elaboratable): m.d.sync += cycle.eq(cycle + 1) m.d.comb += liveness_spec.reset.eq(cycle < 1) m.d.comb += liveness_spec.trig.eq(cycle == 11) - m.d.comb += liveness_spec.check.eq(cycle == 49) + m.d.comb += liveness_spec.check.eq(cycle == 39) m.d.comb += liveness_spec.rvfi_valid.eq(cpu.rvfi.valid) m.d.comb += liveness_spec.rvfi_order.eq(cpu.rvfi.order) @@ -520,8 +520,8 @@ class LivenessSpec(Elaboratable): class LivenessTestCase(FHDLTestCase): def verify(self): - self.assertFormal(LivenessSpec(), mode="cover", depth=50) - self.assertFormal(LivenessSpec(), mode="bmc", depth=50) + self.assertFormal(LivenessSpec(), mode="cover", depth=40) + self.assertFormal(LivenessSpec(), mode="bmc", depth=40) class UniqueSpec(Elaboratable): def elaborate(self, platform):