src/soc/fu/logical/formal/proof_bpermd.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.fu.logical.bpermd 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         # The pseudocode in the Power ISA manual (v3.1) is as follows:
  60         # do i = 0 to 7
  61         #    index <- RS[8*i:8*i+8]
  62         #    if index < 64:
  63         #        perm[i] <- RB[index]
  64         #    else:
  65         #        perm[i] <- 0
  66         # RA <- 56'b0 || perm[0:8]  # big endian though
  67
  68         # Looking at this, I can identify 3 properties that the bperm
  69         # module should keep:
  70         #   1. RA[8:64] should always equal 0
  71         #   2. If RB[i*8:i*8+8] >= 64 then RA[i] should equal 0
  72         #   3. If RB[i*8:i*8+8] < 64 then RA[i] should RS[index]
  73
  74         # Now we need to Assert that the properties above hold:
  75
  76         # Property 1: RA[8:64] should always equal 0
  77         comb += Assert(ra[8:] == 0)
  78         # Notice how we're adding Assert to comb like it's a circuit?
  79         # That's because it kind of is. If you run this proof and have
  80         # yosys graph the ilang, you'll be able to see an equals
  81         # comparison cell feeding into an assert cell
  82
  83         # Now we need to prove property #2. I'm going to leave this to
  84         # you Cole. I'd start by writing a for loop and extracting the
  85         # 8 indices into signals. Then I'd write an if statement
  86         # checking if the index is >= 64 (it's hardware, so use an
  87         # m.If()). Finally, I'd add an assert that checks whether
  88         # ra[i] is equal to 0
  89         for i in range(8):
  90             index = rs[i*8:i*8+8]
  91             with m.If(index >= 64):
  92                 comb += Assert(ra[i] == 0)
  93             with m.Else():
  94                 # to avoid having to create an Array of rb,
  95                 # cycle through from 0-63 on the index *whistle nonchalantly*
  96                 for j in range(64):
  97                     with m.If(index == j):
  98                         comb += Assert(ra[i] == rb[63-j])
  99
 100         return m
 101
 102
 103 class TestCase(FHDLTestCase):
 104     # This bit here is actually in charge of running the formal
 105     # proof. It has nmigen spit out the ilang, and feeds it to
 106     # SymbiYosys to run the proof. If the proof fails, yosys will
 107     # generate a .vcd file showing how it was able to violate your
 108     # assertions in proof_bperm_formal/engine_0/trace.vcd. From that
 109     # you should be able to figure out what went wrong, and either
 110     # correct the assertion or fix the DUT
 111     def test_formal(self):
 112         module = Driver()
 113         # This runs a Bounded Model Check on the driver module
 114         # above. What that does is it starts at some initial state,
 115         # and steps it through `depth` cycles, checking that the
 116         # assertions hold at every cycle. Since this is a
 117         # combinatorial module, it only needs 1 cycle to prove
 118         # everything.
 119         self.assertFormal(module, mode="bmc", depth=2)
 120         self.assertFormal(module, mode="cover", depth=2)
 121
 122     # As mentioned above, you can look at the graph in yosys and see
 123     # all the assertion cells
 124     def test_ilang(self):
 125         dut = Driver()
 126         vl = rtlil.convert(dut, ports=[])
 127         with open("bpermd.il", "w") as f:
 128             f.write(vl)
 129
 130
 131 if __name__ == '__main__':
 132     unittest.main()