src/soc/pipe/logical/formal/proof_bperm.py

   1 # Proof of correctness for bit permute module
   2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
   3
   4 from nmigen import (Module, Signal, Elaboratable, Mux, Cat, Repl,
   5                     signed)
   6 from nmigen.asserts import Assert, AnyConst, Assume, Cover
   7 from nmigen.test.utils import FHDLTestCase
   8 from nmigen.cli import rtlil
   9
  10 from soc.logical.bperm import Bpermd
  11
  12 import unittest
  13
  14
  15 # So formal verification is a little different than writing a test
  16 # case, as you're actually generating logic around your module to
  17 # check that it behaves a certain way. So here, I'm going to create a
  18 # module to put my formal assertions in
  19 class Driver(Elaboratable):
  20     def __init__(self):
  21         # We don't need any inputs and outputs here, so I won't
  22         # declare any
  23         pass
  24
  25     def elaborate(self, platform):
  26         # standard stuff
  27         m = Module()
  28         comb = m.d.comb
  29
  30         # instantiate the device under test as a submodule
  31         m.submodules.bperm = bperm = Bpermd(64)
  32
  33         # Grab the inputs and outputs of the DUT to make them more
  34         # convenient to access
  35         rs = bperm.rs
  36         rb = bperm.rb
  37         ra = bperm.ra
  38
  39         # Before we prove any properties about the DUT, we need to set
  40         # up its inputs. There's a couple ways to do this, you could
  41         # define some inputs and outputs for the driver module and
  42         # wire them up to the DUT, but that's kind of a pain. The
  43         # other option is to use AnyConst/AnySeq, which tells yosys
  44         # that those inputs can take on any value.
  45
  46         # AnyConst should be used when the input should take on a
  47         # random value, but that value should be constant throughout
  48         # the test.
  49         # AnySeq should be used when the input can change on every
  50         # cycle
  51
  52         # Since this is a combinatorial circuit, it really doesn't
  53         # matter which one you choose, so I chose AnyConst. If this
  54         # was a sequential circuit, (especially a state machine) you'd
  55         # want to use AnySeq
  56         comb += [rs.eq(AnyConst(64)),
  57                  rb.eq(AnyConst(64))]
  58
  59
  60         # The pseudocode in the Power ISA manual (v3.1) is as follows:
  61         # do i = 0 to 7
  62         #    index <- RS[8*i:8*i+8]
  63         #    if index < 64:
  64         #        perm[i] <- RB[index]
  65         #    else:
  66         #        perm[i] <- 0
  67         # RA <- 56'b0 || perm[0:8]  # big endian though
  68
  69         # Looking at this, I can identify 3 properties that the bperm
  70         # module should keep:
  71         #   1. RA[8:64] should always equal 0
  72         #   2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0
  73         #   3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index]
  74
  75         # Now we need to Assert that the properties above hold:
  76
  77         # Property 1: RA[8:64] should always equal 0
  78         comb += Assert(ra[8:] == 0)
  79         # Notice how we're adding Assert to comb like it's a circuit?
  80         # That's because it kind of is. If you run this proof and have
  81         # yosys graph the ilang, you'll be able to see an equals
  82         # comparison cell feeding into an assert cell
  83
  84         # Now we need to prove property #2. I'm going to leave this to
  85         # you Cole. I'd start by writing a for loop and extracting the
  86         # 8 indices into signals. Then I'd write an if statement
  87         # checking if the index is >= 64 (it's hardware, so use an
  88         # m.If()). Finally, I'd add an assert that checks whether
  89         # ra[i] is equal to 0
  90
  91
  92
  93         return m
  94
  95
  96 class TestCase(FHDLTestCase):
  97     # This bit here is actually in charge of running the formal
  98     # proof. It has nmigen spit out the ilang, and feeds it to
  99     # SymbiYosys to run the proof. If the proof fails, yosys will
 100     # generate a .vcd file showing how it was able to violate your
 101     # assertions in proof_bperm_formal/engine_0/trace.vcd. From that
 102     # you should be able to figure out what went wrong, and either
 103     # correct the assertion or fix the DUT
 104     def test_formal(self):
 105         module = Driver()
 106         # This runs a Bounded Model Check on the driver module
 107         # above. What that does is it starts at some initial state,
 108         # and steps it through `depth` cycles, checking that the
 109         # assertions hold at every cycle. Since this is a
 110         # combinatorial module, it only needs 1 cycle to prove
 111         # everything.
 112         self.assertFormal(module, mode="bmc", depth=2)
 113         self.assertFormal(module, mode="cover", depth=2)
 114
 115     # As mentioned above, you can look at the graph in yosys and see
 116     # all the assertion cells
 117     def test_ilang(self):
 118         dut = Driver()
 119         vl = rtlil.convert(dut, ports=[])
 120         with open("bperm.il", "w") as f:
 121             f.write(vl)
 122
 123
 124 if __name__ == '__main__':
 125     unittest.main()