1 # Proof of correctness for bit permute module
2 # Copyright (C) 2020 Michael Nolan <mtnolan2640@gmail.com>
4 from nmigen
import (Module
, Signal
, Elaboratable
, Mux
, Cat
, Repl
,
6 from nmigen
.asserts
import Assert
, AnyConst
, Assume
, Cover
7 from nmutil
.formaltest
import FHDLTestCase
8 from nmigen
.cli
import rtlil
10 from soc
.fu
.logical
.bpermd
import Bpermd
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
):
21 # We don't need any inputs and outputs here, so I won't
25 def elaborate(self
, platform
):
30 # instantiate the device under test as a submodule
31 m
.submodules
.bperm
= bperm
= Bpermd(64)
33 # Grab the inputs and outputs of the DUT to make them more
34 # convenient to access
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.
46 # AnyConst should be used when the input should take on a
47 # random value, but that value should be constant throughout
49 # AnySeq should be used when the input can change on every
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
56 comb
+= [rs
.eq(AnyConst(64)),
59 # The pseudocode in the Power ISA manual (v3.1) is as follows:
61 # index <- RS[8*i:8*i+8]
63 # perm[i] <- RB[index]
66 # RA <- 56'b0 || perm[0:8] # big endian though
68 # Looking at this, I can identify 3 properties that the bperm
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]
74 # Now we need to Assert that the properties above hold:
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
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
91 with m
.If(index
>= 64):
92 comb
+= Assert(ra
[i
] == 0)
94 # to avoid having to create an Array of rb,
95 # cycle through from 0-63 on the index *whistle nonchalantly*
97 with m
.If(index
== j
):
98 comb
+= Assert(ra
[i
] == rb
[63-j
])
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
):
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
119 self
.assertFormal(module
, mode
="bmc", depth
=2)
120 self
.assertFormal(module
, mode
="cover", depth
=2)
122 # As mentioned above, you can look at the graph in yosys and see
123 # all the assertion cells
124 def test_ilang(self
):
126 vl
= rtlil
.convert(dut
, ports
=[])
127 with
open("bpermd.il", "w") as f
:
131 if __name__
== '__main__':