1 # Notes on Formal Proofs
3 If you study the ALU and SPR function unit directories, you'll find a set of formal proofs which I (Samuel A. Falvo II) found very confusing.
4 After some study of the ALU proofs, however, I've come to see some basic patterns.
5 Whether these patterns apply to other proofs throughout the rest of the code-base is unknown; I haven't gotten that far yet.
6 But, for now, this "cheat sheet" of sorts should help newcomers to the project better understand why these Python modules are structured the way they are.
8 In the discussion below, I'll be referring to the following URLs:
10 - [alu/formal/proof_main_stage.py](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;hb=HEAD)
11 - [alu/main_stage.py](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/main_stage.py;h=719a9a731e4c9c5f637f574fbf01203fea36df28;hb=HEAD)
13 ## Pipeline Stage Architecture
15 A pipeline stage appears to have the following overall architecture
16 (there will almost certainly be exceptions to this that I'm not familiar with).
17 (lkcl: no, there are absolutely none. no exceptions. at all. this is
18 because there is a defined API):
21 OpSubset Operand Inputs (originally from Register File)
24 +-------------------------+
26 +-------------------------+
29 OpSubset Result Outputs
30 (to next stage / register file logic)
32 Note that the **Pipeline Stage** is *purely combinatorial logic.*
33 (lkcl: yes. this is noted in the pipeline API, see
34 <https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/stageapi.py;hb=HEAD>)
35 Any state between pipeline stages is instantiated through mechanisms not disclosed here.
36 (IIRC, that logic is located in the `nmutil` package, but my memory is hazy here.)
37 (lkcl: in the pipeline API. see stageapi.py).
41 The `Driver` class is an `Elaboratable` class (an `nmigen` module)
42 which specifies all the properties that the module under test
43 (in this case, `ALUMainStage`)
44 must satisfy to be considered "correct."
49 The `__init__` method is the constructor for the class.
50 It prevents `Elaboratable`'s constructor from running.
52 It's not yet clear to me why this is done.
53 (lkcl: because whitequark found that people were forgetting to add an
54 elaborate function, and wondering why their code failed to work).
56 ### `elaborate` method
58 Bluntly, this method is (depending on what you're familiar with) a
59 macro or a monad. Its job is to build a *description* of the final
60 output module by appending various objects to `comb`. In this case,
61 the module's job is to specify the correct behavior of a production
62 submodule, `ALUMainStage`. This is fairly basic `nmigen` material,
63 so I won't spend any more time on this.
65 #### `CompALUOpSubset`
67 `CompALUOpSubset` is, ultimately, an `nmigen`
68 [record](https://gitlab.com/nmigen/nmigen/blob/master/nmigen/hdl/rec.py#L89)
69 which contains a number of fields related to telling the pipeline stage
70 *what to do* and providing all the information it needs in order *to*
71 "do". (Hence the *Op* in the class name.) I won't disclose
72 the fields here, because they're liable to change at any time. What is
73 important to know here is that this record exists for one purpose: to
74 ensure that when the interface to the ALU pipeline stage changes for
75 any reason, *all* consumers of that interface are updated consistently.
77 Because this is a record, its fields may be introspected. This happens
78 frequently: it is the case that an Op-type record is passed
79 unchanged from stage to stage. However, `nmigen` does not seem to support
80 testing records for equality in formal assertions. (lkcl: it does) To
81 express this constraint without needing to update a pile of use-sites
82 every time the interface changes, you'll find logic
83 [like this](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;h=5e70d1e885b41ca50d69f57e9ee94b568d001c2e;hb=HEAD#l64).
85 (lkcl: which has been established why:
86 <https://bugs.libre-soc.org/show_bug.cgi?id=429#c3> and it is down
87 to FPPipeContext not being a Record, but its member variable - op -
90 **NOTE:** Instantiating one of these records
91 (lkcl: FPPipeContext is not a Record, see above)) *does not* provide
92 these inputs to the module under test. It merely makes the fields of
93 this record available to the formal verification solver so it can fiddle
94 the bits as it explores the design space. The record must be connected
95 directly to the module via a signal assignment:
96 [see line 62 of the source listing.](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;h=5e70d1e885b41ca50d69f57e9ee94b568d001c2e;hb=HEAD#l62)
98 comb += dut.i.ctx.op.eq(rec)
102 `ALUPipeSpec` is a similar construct, but it serves a different role than the above class.
104 [source code](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/pipe_data.py;h=71363049ba5a437a708e53dfbc3370f17aa394d1;hb=HEAD)
105 , it appears to define bits in one or more *register files*,
106 for both input input the stage and output from the stage.
108 class ALUPipeSpec(CommonPipeSpec):
109 regspec = (ALUInputData.regspec, ALUOutputData.regspec)
110 opsubsetkls = CompALUOpSubset
112 This structure is passed to the constructor of the module-under-test.
113 That constructor, ultimately, has the effect of creating a set of
114 inputs (`dut.i`) and outputs (`dut.o`) that matches the register field
117 See [lines 9 (input) and 19 (output) of the source listing](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/pipe_data.py;h=71363049ba5a437a708e53dfbc3370f17aa394d1;hb=HEAD).
119 class ALUInputData(IntegerData):
120 regspec = [('INT', 'ra', '0:63'), # RA
121 ('INT', 'rb', '0:63'), # RB/immediate
122 ('XER', 'xer_so', '32'), # XER bit 32: SO
123 ('XER', 'xer_ca', '34,45')] # XER bit 34/45: CA/CA32
124 def __init__(self, pspec):
125 super().__init__(pspec, False)
127 self.a, self.b = self.ra, self.rb
129 class ALUOutputData(IntegerData):
130 regspec = [('INT', 'o', '0:63'),
131 ('CR', 'cr_a', '0:3'),
132 ('XER', 'xer_ca', '34,45'), # bit0: ca, bit1: ca32
133 ('XER', 'xer_ov', '33,44'), # bit0: ov, bit1: ov32
134 ('XER', 'xer_so', '32')]
135 def __init__(self, pspec):
136 super().__init__(pspec, True)
140 **NOTE:** these are actually separate and distinct registers!
141 For example, the POWER XER register defines two carry bits at positions
142 34 and 45 in a 64-bit word. However, when referencing these bits via
143 `dut.i.xer_ca`, they occupy bits 0 and 1. The process reverses for
144 outputs; bits 0 and 1 of the `dut.o.xer_ca` field have to be re-distributed
145 to XER register bits 34 and 45 again.
147 It is the responsibility of any pipelines to **understand and respect
148 this subdivision**. For example, in the
149 [SPR main_statge.py at lines 78 to 86](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/spr/main_stage.py;h=f4261b62a2b2d104c9edfa88262f27a97d9498a3;hb=HEAD#l76)
150 the implementation of PowerISA `mfspr` *manually* copies the XER `so`,
151 `ov/32` and `ca/32` bits into the output, based on hard-coded explicit
152 knowledge inside this code, of their positions.
155 with m.Case(SPR.XER):
157 comb += o[63-XER_bits['SO']].eq(so_i)
159 comb += o[63-XER_bits['OV']].eq(ov_i[0])
160 comb += o[63-XER_bits['OV32']].eq(ov_i[1])
162 comb += o[63-XER_bits['CA']].eq(ca_i[0])
163 comb += o[63-XER_bits['CA32']].eq(ca_i[1])
166 [Microwatt](https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L831)
167 does exactly the same thing:
169 if decode_spr_num(e_in.insn) = SPR_XER then
170 -- bits 0:31 and 35:43 are treated as reserved
171 -- and return 0s when read using mfxer
172 result(63 downto 32) := (others => '0');
173 result(63-32) := v.e.xerc.so;
174 result(63-33) := v.e.xerc.ov;
175 result(63-34) := v.e.xerc.ca;
176 result(63-35 downto 63-43) := "000000000";
177 result(63-44) := v.e.xerc.ov32;
178 result(63-45) := v.e.xerc.ca32;
181 #### Instantiating the Module Under Test
183 Looking at [line 41 through 54](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;h=5e70d1e885b41ca50d69f57e9ee94b568d001c2e;hb=HEAD#l41),
184 we see the module we want to test actually instantiated.
186 m.submodules.dut = dut = ALUMainStage(pspec)
188 Since register inputs and outputs are frequently accessed, it's worthwhile
189 defining a set of aliases for those signals.
191 # convenience variables
194 ca_in = dut.i.xer_ca[0] # CA carry in
195 ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
196 so_in = dut.i.xer_so # SO sticky overflow
198 ca_o = dut.o.xer_ca.data[0] # CA carry out
199 ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
200 ov_o = dut.o.xer_ov.data[0] # OV overflow
201 ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
204 Although this somewhat obscures the intent of the code,
205 it will save typing which reduces opportunity for error.
207 Lines 56 through 62 connect all the input signals of the submodule to
210 # setup random inputs
211 comb += [a.eq(AnyConst(64)),
213 ca_in.eq(AnyConst(0b11)),
214 so_in.eq(AnyConst(1))]
218 Starting at [line 64](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/formal/proof_main_stage.py;h=5e70d1e885b41ca50d69f57e9ee94b568d001c2e;hb=HEAD#l64)
219 we find the start of properties which must apply to the submodule.