da198940f75b3868ca864f1d75c6e99c55b1f073
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 nmigen
.test
.utils
import FHDLTestCase
8 from nmigen
.cli
import rtlil
10 from soc
.logical
.bperm
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)),
60 # The pseudocode in the Power ISA manual (v3.1) is as follows:
62 # index <- RS[8*i:8*i+8]
64 # perm[i] <- RB[index]
67 # RA <- 56'b0 || perm[0:8] # big endian though
69 # Looking at this, I can identify 3 properties that the bperm
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]
75 # Now we need to Assert that the properties above hold:
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
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
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
):
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
112 self
.assertFormal(module
, mode
="bmc", depth
=2)
113 self
.assertFormal(module
, mode
="cover", depth
=2)
115 # As mentioned above, you can look at the graph in yosys and see
116 # all the assertion cells
117 def test_ilang(self
):
119 vl
= rtlil
.convert(dut
, ports
=[])
120 with
open("bperm.il", "w") as f
:
124 if __name__
== '__main__':