From 2e2771513cbcc4497c03f1f016d7b566e0fa0c89 Mon Sep 17 00:00:00 2001 From: colepoirier Date: Mon, 18 May 2020 15:25:37 -0700 Subject: [PATCH] Added 2nd of 3 assertions for proof_bperm.py, currently not correct --- src/soc/fu/logical/formal/proof_bperm.py | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/soc/fu/logical/formal/proof_bperm.py b/src/soc/fu/logical/formal/proof_bperm.py index 02d63cb8..453e419f 100644 --- a/src/soc/fu/logical/formal/proof_bperm.py +++ b/src/soc/fu/logical/formal/proof_bperm.py @@ -87,7 +87,10 @@ class Driver(Elaboratable): # checking if the index is >= 64 (it's hardware, so use an # m.If()). Finally, I'd add an assert that checks whether # ra[i] is equal to 0 - + for i in range(8): + index = rb[i*8:i*8+8] + with m.If(index >= 64): + comb += Assert(ra[i] == 0) return m @@ -108,7 +111,7 @@ class TestCase(FHDLTestCase): # and steps it through `depth` cycles, checking that the # assertions hold at every cycle. Since this is a # combinatorial module, it only needs 1 cycle to prove - # everything. + # everything. self.assertFormal(module, mode="bmc", depth=2) self.assertFormal(module, mode="cover", depth=2) -- 2.30.2