Make liveness checks pass
This commit is contained in:
parent
b38f19411a
commit
32388adce0
@ -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
|
||||
|
||||
@ -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):
|
||||
|
||||
Loading…
Reference in New Issue
Block a user