# Notes on Formal Proofs 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. After some study of the ALU proofs, however, I've come to see some basic patterns. Whether these patterns apply to other proofs throughout the rest of the code-base is unknown; I haven't gotten that far yet. 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. In the discussion below, I'll be referring to the following URLs: - [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) - [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) ## Pipeline Stage Architecture A pipeline stage appears to have the following overall architecture (there will almost certainly be exceptions to this that I'm not familiar with). (lkcl: no, there are absolutely none. no exceptions. at all. this is because there is a defined API): (from previous stage) OpSubset Operand Inputs (originally from Register File) | | V V +-------------------------+ | Pipeline Stage | +-------------------------+ | | V V OpSubset Result Outputs (to next stage / register file logic) Note that the **Pipeline Stage** is *purely combinatorial logic.* (lkcl: yes. this is noted in the pipeline API, see ) Any state between pipeline stages is instantiated through mechanisms not disclosed here. (IIRC, that logic is located in the `nmutil` package, but my memory is hazy here.) (lkcl: in the pipeline API. see stageapi.py). ## class Driver The `Driver` class is an `Elaboratable` class (an `nmigen` module) which specifies all the properties that the module under test (in this case, `ALUMainStage`) must satisfy to be considered "correct." ### `__init__` The `__init__` method is the constructor for the class. It prevents `Elaboratable`'s constructor from running. (lkcl: not quite) It's not yet clear to me why this is done. (lkcl: because whitequark found that people were forgetting to add an elaborate function, and wondering why their code failed to work). ### `elaborate` method Bluntly, this method is (depending on what you're familiar with) a macro or a monad. Its job is to build a *description* of the final output module by appending various objects to `comb`. In this case, the module's job is to specify the correct behavior of a production submodule, `ALUMainStage`. This is fairly basic `nmigen` material, so I won't spend any more time on this. #### `CompALUOpSubset` `CompALUOpSubset` is, ultimately, an `nmigen` [record](https://gitlab.com/nmigen/nmigen/blob/master/nmigen/hdl/rec.py#L89) which contains a number of fields related to telling the pipeline stage *what to do* and providing all the information it needs in order *to* "do". (Hence the *Op* in the class name.) I won't disclose the fields here, because they're liable to change at any time. What is important to know here is that this record exists for one purpose: to ensure that when the interface to the ALU pipeline stage changes for any reason, *all* consumers of that interface are updated consistently. Because this is a record, its fields may be introspected. This happens frequently: it is the case that an Op-type record is passed unchanged from stage to stage. However, `nmigen` does not seem to support testing records for equality in formal assertions. (lkcl: it does) To express this constraint without needing to update a pile of use-sites every time the interface changes, you'll find logic [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). (lkcl: which has been established why: and it is down to FPPipeContext not being a Record, but its member variable - op - *is* a Record). **NOTE:** Instantiating one of these records (lkcl: FPPipeContext is not a Record, see above)) *does not* provide these inputs to the module under test. It merely makes the fields of this record available to the formal verification solver so it can fiddle the bits as it explores the design space. The record must be connected directly to the module via a signal assignment: [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) comb += dut.i.ctx.op.eq(rec) #### `ALUPipeSpec` `ALUPipeSpec` is a similar construct, but it serves a different role than the above class. Looking at its [source code](https://git.libre-soc.org/?p=soc.git;a=blob;f=src/soc/fu/alu/pipe_data.py;h=71363049ba5a437a708e53dfbc3370f17aa394d1;hb=HEAD) , it appears to define bits in one or more *register files*, for both input input the stage and output from the stage. class ALUPipeSpec(CommonPipeSpec): regspec = (ALUInputData.regspec, ALUOutputData.regspec) opsubsetkls = CompALUOpSubset This structure is passed to the constructor of the module-under-test. That constructor, ultimately, has the effect of creating a set of inputs (`dut.i`) and outputs (`dut.o`) that matches the register field names. 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). class ALUInputData(IntegerData): regspec = [('INT', 'ra', '0:63'), # RA ('INT', 'rb', '0:63'), # RB/immediate ('XER', 'xer_so', '32'), # XER bit 32: SO ('XER', 'xer_ca', '34,45')] # XER bit 34/45: CA/CA32 def __init__(self, pspec): super().__init__(pspec, False) # convenience self.a, self.b = self.ra, self.rb class ALUOutputData(IntegerData): regspec = [('INT', 'o', '0:63'), ('CR', 'cr_a', '0:3'), ('XER', 'xer_ca', '34,45'), # bit0: ca, bit1: ca32 ('XER', 'xer_ov', '33,44'), # bit0: ov, bit1: ov32 ('XER', 'xer_so', '32')] def __init__(self, pspec): super().__init__(pspec, True) # convenience self.cr0 = self.cr_a **NOTE:** these are actually separate and distinct registers! For example, the POWER XER register defines two carry bits at positions 34 and 45 in a 64-bit word. However, when referencing these bits via `dut.i.xer_ca`, they occupy bits 0 and 1. The process reverses for outputs; bits 0 and 1 of the `dut.o.xer_ca` field have to be re-distributed to XER register bits 34 and 45 again. It is the responsibility of any pipelines to **understand and respect this subdivision**. For example, in the [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) the implementation of PowerISA `mfspr` *manually* copies the XER `so`, `ov/32` and `ca/32` bits into the output, based on hard-coded explicit knowledge inside this code, of their positions. # XER is constructed with m.Case(SPR.XER): # sticky comb += o[63-XER_bits['SO']].eq(so_i) # overflow comb += o[63-XER_bits['OV']].eq(ov_i[0]) comb += o[63-XER_bits['OV32']].eq(ov_i[1]) # carry comb += o[63-XER_bits['CA']].eq(ca_i[0]) comb += o[63-XER_bits['CA32']].eq(ca_i[1]) Note that [Microwatt](https://github.com/antonblanchard/microwatt/blob/master/execute1.vhdl#L831) does exactly the same thing: if decode_spr_num(e_in.insn) = SPR_XER then -- bits 0:31 and 35:43 are treated as reserved -- and return 0s when read using mfxer result(63 downto 32) := (others => '0'); result(63-32) := v.e.xerc.so; result(63-33) := v.e.xerc.ov; result(63-34) := v.e.xerc.ca; result(63-35 downto 63-43) := "000000000"; result(63-44) := v.e.xerc.ov32; result(63-45) := v.e.xerc.ca32; end if; #### Instantiating the Module Under Test 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), we see the module we want to test actually instantiated. m.submodules.dut = dut = ALUMainStage(pspec) Since register inputs and outputs are frequently accessed, it's worthwhile defining a set of aliases for those signals. # convenience variables a = dut.i.a b = dut.i.b ca_in = dut.i.xer_ca[0] # CA carry in ca32_in = dut.i.xer_ca[1] # CA32 carry in 32 so_in = dut.i.xer_so # SO sticky overflow ca_o = dut.o.xer_ca.data[0] # CA carry out ca32_o = dut.o.xer_ca.data[1] # CA32 carry out32 ov_o = dut.o.xer_ov.data[0] # OV overflow ov32_o = dut.o.xer_ov.data[1] # OV32 overflow32 o = dut.o.o.data Although this somewhat obscures the intent of the code, it will save typing which reduces opportunity for error. Lines 56 through 62 connect all the input signals of the submodule to the formal verifier. # setup random inputs comb += [a.eq(AnyConst(64)), b.eq(AnyConst(64)), ca_in.eq(AnyConst(0b11)), so_in.eq(AnyConst(1))] #### Properties 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) we find the start of properties which must apply to the submodule.