From: Jacob Lifshay Date: Thu, 24 Feb 2022 03:28:02 +0000 (-0800) Subject: add formal proof for shift/rot o.ok X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=033b1352a30d1a1cba2f7a854b5ae076a7733c16;p=soc.git add formal proof for shift/rot o.ok --- diff --git a/src/soc/fu/shift_rot/formal/proof_main_stage.py b/src/soc/fu/shift_rot/formal/proof_main_stage.py index 8e2952fc..2423518b 100644 --- a/src/soc/fu/shift_rot/formal/proof_main_stage.py +++ b/src/soc/fu/shift_rot/formal/proof_main_stage.py @@ -114,7 +114,7 @@ def rotl32(v, amt): # properties about its outputs class Driver(Elaboratable): def __init__(self, which): - assert isinstance(which, TstOp) + assert isinstance(which, TstOp) or which is None self.which = which def elaborate(self, platform): @@ -152,11 +152,17 @@ class Driver(Elaboratable): comb += Assert(dut.o.ctx.op == dut.i.ctx.op) comb += Assert(dut.o.ctx.muxid == dut.i.ctx.muxid) - # we're only checking a particular operation: - comb += Assume(dut.i.ctx.op.insn_type == self.which.op) + if self.which is None: + for i in TstOp: + comb += Assume(dut.i.ctx.op.insn_type != i.op) + comb += Assert(~dut.o.o.ok) + else: + # we're only checking a particular operation: + comb += Assume(dut.i.ctx.op.insn_type == self.which.op) + comb += Assert(dut.o.o.ok) - # dispatch to check fn for each op - getattr(self, f"_check_{self.which.name.lower()}")(m, dut) + # dispatch to check fn for each op + getattr(self, f"_check_{self.which.name.lower()}")(m, dut) return m @@ -328,6 +334,9 @@ class ALUTestCase(FHDLTestCase): self.assertFormal(module, mode="bmc", depth=2) self.assertFormal(module, mode="cover", depth=2) + def test_none(self): + self.run_it(None) + def test_shl(self): self.run_it(TstOp.SHL)