From 033b1352a30d1a1cba2f7a854b5ae076a7733c16 Mon Sep 17 00:00:00 2001 From: Jacob Lifshay Date: Wed, 23 Feb 2022 19:28:02 -0800 Subject: [PATCH] add formal proof for shift/rot o.ok --- .../fu/shift_rot/formal/proof_main_stage.py | 19 ++++++++++++++----- 1 file changed, 14 insertions(+), 5 deletions(-) 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) -- 2.30.2