Documentation/notes_on_formal_proofs.mdwn

   1 # Notes on Formal Proofs
   2
   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.
   7
   8 In the discussion below, I'll be referring to the following URLs:
   9
  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)
  12
  13 ## Pipeline Stage Architecture
  14
  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):
  19
  20                (from previous stage)
  21            OpSubset        Operand Inputs (originally from Register File)
  22               |                   |
  23               V                   V
  24            +-------------------------+
  25            | Pipeline Stage          |
  26            +-------------------------+
  27               |                   |
  28               V                   V
  29            OpSubset        Result Outputs
  30         (to next stage / register file logic)
  31
  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).
  38
  39 ## class Driver
  40
  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."
  45
  46
  47 ### `__init__`
  48
  49 The `__init__` method is the constructor for the class.
  50 It prevents `Elaboratable`'s constructor from running.
  51 (lkcl: not quite)
  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).
  55
  56 ### `elaborate` method
  57
  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.
  64
  65 #### `CompALUOpSubset`
  66
  67 `CompALUOpSubset` is, ultimately, an `nmigen`
  68 [record](https://github.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*.  (Hence the *Op* in the class name.)  I won't disclose
  71 the fields here, because they're liable to change at any time.  What is
  72 important to know here is that this record exists for one purpose: to
  73 ensure that when the interface to the ALU pipeline stage changes for
  74 any reason, *all* consumers of that interface are updated consistently.
  75
  76 Because this is a record, its fields may be introspected.  This happens
  77 frequently; it is usually the case that an Op-type record is passed
  78 unchanged from stage to stage.  However, `nmigen` does not seem to support
  79 testing records for equality in formal assertions.  (lkcl: it does) To
  80 express this constraint without needing to update a pile of use-sites
  81 every time the interface changes, you'll find logic
  82 [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).
  83
  84 (lkcl: which has been established why:
  85 <https://bugs.libre-soc.org/show_bug.cgi?id=429#c3> and it is down
  86 to FPPipeContext not being a Record, but its member variable - op -
  87 *is* a Record).
  88
  89 **NOTE:** Instantiating one of these records
  90 (lkcl: FPPipeContext is not a Record, see above)) *does not* provide
  91 these inputs to the module under test.  It merely makes the fields of
  92 this record available to the formal verification solver so it can fiddle
  93 the bits as it explores the design space.  The record must be connected
  94 directly to the module via a signal assignment:
  95 [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)
  96
  97           comb += dut.i.ctx.op.eq(rec)
  98
  99 #### `ALUPipeSpec`
 100
 101 `ALUPipeSpec` is a similar construct, but it serves a different role than the above class.
 102 Looking at its
 103 [source code](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/pipe_data.py;h=71363049ba5a437a708e53dfbc3370f17aa394d1;hb=HEAD)
 104 , it appears to define bits in one or more *register files*,
 105 for both input input the stage and output from the stage.
 106
 107      class ALUPipeSpec(CommonPipeSpec):
 108          regspec = (ALUInputData.regspec, ALUOutputData.regspec)
 109          opsubsetkls = CompALUOpSubset
 110
 111 This structure is passed to the constructor of the module-under-test.
 112 That constructor, ultimately, has the effect of creating a set of
 113 inputs (`dut.i`) and outputs (`dut.o`) that matches the register field
 114 names.
 115
 116 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).
 117
 118      class ALUInputData(IntegerData):
 119          regspec = [('INT', 'ra', '0:63'), # RA
 120                     ('INT', 'rb', '0:63'), # RB/immediate
 121                     ('XER', 'xer_so', '32'), # XER bit 32: SO
 122                     ('XER', 'xer_ca', '34,45')] # XER bit 34/45: CA/CA32
 123          def __init__(self, pspec):
 124              super().__init__(pspec, False)
 125              # convenience
 126              self.a, self.b = self.ra, self.rb
 127
 128      class ALUOutputData(IntegerData):
 129          regspec = [('INT', 'o', '0:63'),
 130                     ('CR', 'cr_a', '0:3'),
 131                     ('XER', 'xer_ca', '34,45'), # bit0: ca, bit1: ca32
 132                     ('XER', 'xer_ov', '33,44'), # bit0: ov, bit1: ov32
 133                     ('XER', 'xer_so', '32')]
 134          def __init__(self, pspec):
 135              super().__init__(pspec, True)
 136              # convenience
 137              self.cr0 = self.cr_a
 138
 139 **NOTE:** these are actually separate and distinct registers!
 140 For example, the POWER XER register defines two carry bits at positions
 141 34 and 45 in a 64-bit word.  However, when referencing these bits via
 142 `dut.i.xer_ca`, they occupy bits 0 and 1.  The process reverses for
 143 outputs; bits 0 and 1 of the `dut.o.xer_ca` field have to be re-distributed
 144 to XER register bits 34 and 45 again.
 145
 146 It is the responsibility of any pipelines to **understand and respect
 147 this subdivision**.  For example, in the
 148 [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)
 149 the implementation of PowerISA `mfspr` *manually* copies the XER `so`,
 150 `ov/32` and `ca/32` bits into the output, based on hard-coded explicit
 151 knowledge inside this code, of their positions.
 152
 153             # XER is constructed
 154             with m.Case(SPR.XER):
 155                 # sticky
 156                 comb += o[63-XER_bits['SO']].eq(so_i)
 157                 # overflow
 158                 comb += o[63-XER_bits['OV']].eq(ov_i[0])
 159                 comb += o[63-XER_bits['OV32']].eq(ov_i[1])
 160                 # carry
 161                 comb += o[63-XER_bits['CA']].eq(ca_i[0])
 162                 comb += o[63-XER_bits['CA32']].eq(ca_i[1])
 163
 164 Note that
 165 [Microwatt](https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L831)
 166 does exactly the same thing:
 167
 168             if decode_spr_num(e_in.insn) = SPR_XER then
 169                 -- bits 0:31 and 35:43 are treated as reserved
 170                 -- and return 0s when read using mfxer
 171                 result(63 downto 32) := (others => '0');
 172                 result(63-32) := v.e.xerc.so;
 173                 result(63-33) := v.e.xerc.ov;
 174                 result(63-34) := v.e.xerc.ca;
 175                 result(63-35 downto 63-43) := "000000000";
 176                 result(63-44) := v.e.xerc.ov32;
 177                 result(63-45) := v.e.xerc.ca32;
 178             end if;
 179
 180 #### Instantiating the Module Under Test
 181
 182 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),
 183 we see the module we want to test actually instantiated.
 184
 185           m.submodules.dut = dut = ALUMainStage(pspec)
 186
 187 Since register inputs and outputs are frequently accessed, it's worthwhile
 188 defining a set of aliases for those signals.
 189
 190           # convenience variables
 191           a = dut.i.a
 192           b = dut.i.b
 193           ca_in = dut.i.xer_ca[0]   # CA carry in
 194           ca32_in = dut.i.xer_ca[1] # CA32 carry in 32
 195           so_in = dut.i.xer_so      # SO sticky overflow
 196
 197           ca_o = dut.o.xer_ca.data[0]   # CA carry out
 198           ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32
 199           ov_o = dut.o.xer_ov.data[0]   # OV overflow
 200           ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32
 201           o = dut.o.o.data
 202
 203 Although this somewhat obscures the intent of the code,
 204 it will save typing which reduces opportunity for error.
 205
 206 Lines 56 through 62 connect all the input signals of the submodule to
 207 the formal verifier.
 208
 209           # setup random inputs
 210           comb += [a.eq(AnyConst(64)),
 211                    b.eq(AnyConst(64)),
 212                    ca_in.eq(AnyConst(0b11)),
 213                    so_in.eq(AnyConst(1))]
 214
 215 #### Properties
 216
 217 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)
 218 we find the start of properties which must apply to the submodule.
 219