use get_l0_mem in HDLState to get memory data
[soc.git] / 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 nmutil.formaltest 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()