From 597144a6f9826884cd82d0ee5d81030059b21f1c Mon Sep 17 00:00:00 2001 From: Michael Nolan Date: Sun, 17 May 2020 13:12:32 -0400 Subject: [PATCH] Add incomplete proof_bperm.py with comments on how to finish the proof --- src/soc/logical/formal/proof_bperm.py | 125 ++++++++++++++++++++++++++ 1 file changed, 125 insertions(+) create mode 100644 src/soc/logical/formal/proof_bperm.py diff --git a/src/soc/logical/formal/proof_bperm.py b/src/soc/logical/formal/proof_bperm.py new file mode 100644 index 00000000..da198940 --- /dev/null +++ b/src/soc/logical/formal/proof_bperm.py @@ -0,0 +1,125 @@ +# Proof of correctness for bit permute module +# Copyright (C) 2020 Michael Nolan + +from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl, + signed) +from nmigen.asserts import Assert, AnyConst, Assume, Cover +from nmigen.test.utils import FHDLTestCase +from nmigen.cli import rtlil + +from soc.logical.bperm import Bpermd + +import unittest + + +# So formal verification is a little different than writing a test +# case, as you're actually generating logic around your module to +# check that it behaves a certain way. So here, I'm going to create a +# module to put my formal assertions in +class Driver(Elaboratable): + def __init__(self): + # We don't need any inputs and outputs here, so I won't + # declare any + pass + + def elaborate(self, platform): + # standard stuff + m = Module() + comb = m.d.comb + + # instantiate the device under test as a submodule + m.submodules.bperm = bperm = Bpermd(64) + + # Grab the inputs and outputs of the DUT to make them more + # convenient to access + rs = bperm.rs + rb = bperm.rb + ra = bperm.ra + + # Before we prove any properties about the DUT, we need to set + # up its inputs. There's a couple ways to do this, you could + # define some inputs and outputs for the driver module and + # wire them up to the DUT, but that's kind of a pain. The + # other option is to use AnyConst/AnySeq, which tells yosys + # that those inputs can take on any value. + + # AnyConst should be used when the input should take on a + # random value, but that value should be constant throughout + # the test. + # AnySeq should be used when the input can change on every + # cycle + + # Since this is a combinatorial circuit, it really doesn't + # matter which one you choose, so I chose AnyConst. If this + # was a sequential circuit, (especially a state machine) you'd + # want to use AnySeq + comb += [rs.eq(AnyConst(64)), + rb.eq(AnyConst(64))] + + + # The pseudocode in the Power ISA manual (v3.1) is as follows: + # do i = 0 to 7 + # index <- RS[8*i:8*i+8] + # if index < 64: + # perm[i] <- RB[index] + # else: + # perm[i] <- 0 + # RA <- 56'b0 || perm[0:8] # big endian though + + # Looking at this, I can identify 3 properties that the bperm + # module should keep: + # 1. RA[8:64] should always equal 0 + # 2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0 + # 3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index] + + # Now we need to Assert that the properties above hold: + + # Property 1: RA[8:64] should always equal 0 + comb += Assert(ra[8:] == 0) + # Notice how we're adding Assert to comb like it's a circuit? + # That's because it kind of is. If you run this proof and have + # yosys graph the ilang, you'll be able to see an equals + # comparison cell feeding into an assert cell + + # Now we need to prove property #2. I'm going to leave this to + # you Cole. I'd start by writing a for loop and extracting the + # 8 indices into signals. Then I'd write an if statement + # 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 + + + + return m + + +class TestCase(FHDLTestCase): + # This bit here is actually in charge of running the formal + # proof. It has nmigen spit out the ilang, and feeds it to + # SymbiYosys to run the proof. If the proof fails, yosys will + # generate a .vcd file showing how it was able to violate your + # assertions in proof_bperm_formal/engine_0/trace.vcd. From that + # you should be able to figure out what went wrong, and either + # correct the assertion or fix the DUT + def test_formal(self): + module = Driver() + # This runs a Bounded Model Check on the driver module + # above. What that does is it starts at some initial state, + # 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. + self.assertFormal(module, mode="bmc", depth=2) + self.assertFormal(module, mode="cover", depth=2) + + # As mentioned above, you can look at the graph in yosys and see + # all the assertion cells + def test_ilang(self): + dut = Driver() + vl = rtlil.convert(dut, ports=[]) + with open("bperm.il", "w") as f: + f.write(vl) + + +if __name__ == '__main__': + unittest.main() -- 2.30.2