+++ /dev/null
-The SOC is designed to be compliant with POWER 3.0B with somewhere near
-300 instructions excluding Vector instructions.
-
-# Decoder
-
-The page on the decoder is here: [[architecture/decoder]]
+++ /dev/null
-[[!img 2020-08-15_12-04.png size="800x" ]]
-
-This tutorial is about generating better GTKWave documents (*.gtkw)
-from Python. The goal is to ease analysis of traces generated by
-unit-tests, and at the same time to better understand the inner working
-of modules, for which we are writing such tests.
-
-# Stylish GTKWave Documents
-
-In this tutorial, you will learn how to:
-
-1. Use individual trace colors.
- For instance, use different color styles for input, output, debug and
- internal traces.
-2. Use numeric bases besides the default hex.
-3. Create collapsible trace groups
- Useful to hide and show, at once, groups of debug, internal and
- sub-module traces.
- Select the opening or closing brace, then use the T key.
-4. Add comments in the signal names pane
-5. Change the displayed name of a trace
-6. Use a sane default for initial zoom level
-7. Place markers on interesting places
-8. Put the generating file name as a comment in the file
-
-## Basic trace display
-
-First, we need a VCD file. Try:
-
- python -m nmutil.test.example_gtkwave
-
-Among other files, it will generate ``test_shifter.vcd``.
-
-Lets write a simple GTKW document. First, import the function:
-
- from nmutil.gtkw import write_gtkw
-
-Create a list of the traces you want to see. Some hints:
-
-1. Put all trace names in quotes.
-2. Use the same names as you would see in the trace pane of GTKWave
-3. If a trace is multi-bit, use array notation 'name[max:min]'
-
-For example:
-
- traces = [
- 'clk',
- # prev port
- 'op__sdir', 'p_data_i[7:0]', 'p_shift_i[7:0]', 'p_valid_i', 'p_ready_o',
- # internal signals
- 'fsm_state', 'count[3:0]', 'shift_reg[7:0]',
- # next port
- 'n_data_o[7:0]', 'n_valid_o', 'n_ready_i'
- ]
-
-Now, create the document:
-
- write_gtkw("simple.gtkw", "test_shifter.vcd", traces, module='top.shf')
-
-Remarks:
-
-1. ``simple.gtkw`` is the name of our GTKWave document
-2. ``test_shifter.vcd`` is the VCD file
-3. ``traces`` is a list of trace names
-4. ``top.shf`` is the hierarchy path of the module
-
-Now try:
-
- gtkwave simple.gtkw
-
-Notice:
-
-1. No need to press the "zoom to fit" button. The default zoom level is
-adequate for a 1 MHz clock.
-2. If you made a mistake, there will be no warning. The trace will
-simply not appear
-3. The reload button will only reload the VCD file, not the GTKW document. If you regenerate the document, you need to close and open a
-new tab, or exit GTKWave and run again: ``gtkwave simple.gtkw``
-4. If you feel tired of seeing the GTKWave splash window every time,
-do: ``echo splash_disable 1 >> ~/.gtkwaverc``
-5. If you modify the document manually, better to save it with another
-name
-
-## Adding color
-
-Go back to the trace list and replace the ``'op__sdir'`` string with:
-
- ('op__sdir', {'color': 'orange'})
-
-Recreate the document (you can change the file name):
-
- write_gtkw("color.gtkw", "test_shifter.vcd", traces, module='top.shf')
-
-If you now run ``gtkwave color.gtkw``, you will see that ``op__sdir``
-has the new color.
-
-## Writing GTKWave documents, with style
-
-Let's say we want all input traces be orange, and all output traces be
-yellow. To change them one by one, as we did with ``op__sdir``, would be
-very tedious and verbose. Also, hardcoding the color name will make it
-difficult to change it later.
-
-To solve this, lets create a style specification:
-
- style = {
- 'in': {'color': 'orange'},
- 'out': {'color': 'yellow'}
- }
-
-Then, change:
-
- ('op__sdir', {'color': 'orange'})
-
-to:
-
- ('op__sdir', 'in')
-
-then (notice how we add ``style``):
-
- write_gtkw("style1.gtkw", "test_shifter.vcd", traces, style, module='top.shf')
-
-If you now run ``gtkwave style1.gtkw``, you will see that ``op__sdir``
-still has the new color.
-
-Let's add more color:
-
- traces = [
- 'clk',
- # prev port
- ('op__sdir', 'in'),
- ('p_data_i[7:0]', 'in'),
- ('p_shift_i[7:0]', 'in'),
- ('p_valid_i', 'in'),
- ('p_ready_o', 'out'),
- # internal signals
- 'fsm_state',
- 'count[3:0]',
- 'shift_reg[7:0]',
- # next port
- ('n_data_o[7:0]', 'out'),
- ('n_valid_o', 'out'),
- ('n_ready_i', 'in'),
- ]
-
-Then
-
- write_gtkw("style2.gtkw", "test_shifter.vcd", traces, style, module='top.shf')
-
-If you now run ``gtkwave style2.gtkw``, you will see that input, output and internal signals have different color.
-
-# New signals at simulation time
-
-At simulation time, you can declare a new signal, and use it inside
-the test case, as any other signal. By including it in the "traces"
-parameter of Simulator.write_vcd, it is included in the trace dump
-file.
-
-Useful for adding "printf" style debugging for GTKWave.
-
-# String traces
-
-When declaring a Signal, you can pass a custom decoder that
-translates the Signal logic level to a string. nMigen uses this
-internally to display Enum traces, but it is available for general
-use.
-
-Some applications are:
-
-1. Display a string when a signal is at high level, otherwise show a
- single horizontal line. Useful to draw attention to a time interval.
-2. Display the stages of a unit test
-3. Display arbitrary debug statements along the timeline.
+++ /dev/null
-# Documentation
-
-A draft version of the specification is available at <https://ftp.libre-soc.org/power-spec-draft.pdf>
-
-## Codebase Structure
-
-The SOC is partitioned into three repositories. The subrepositories are intended as standalone projects useful outside of LibreSOC. For example, the IEE754 FPU repository is a general purpose IEEE754 toolkit for the construction of FSMs and arbitrary length pipelines.
-
-| Git Repo | Documentation | Description
-|----------|---------------|---------------|
-| [SOC](https://git.libre-soc.org/?p=soc.git;a=tree) | [[SOC Docs|3d_gpu/architecture]] | Main POWER9 GPU |
-| [FPU](https://git.libre-soc.org/?p=ieee754fpu.git;a=tree) | -- | Equivalent to hardfloat-3 |
-| [nmutil](https://git.libre-soc.org/?p=nmutil.git;a=tree) | -- | Equivalent to Chisel3.util |
-
-## Installing the Codebase
-
- pip3 install virtualenv requests
- mkdir ~/.virtualenvs && cd ~/.virtualenvs
- python3 -m venv libresoc
- source ~/.virtualenvs/libresoc/bin/activate
-
- cd ~; mkdir libresoc; cd libresoc
- git clone https://git.libre-soc.org/git/nmutil.git
- git clone https://git.libre-soc.org/git/ieee754fpu.git
- git clone https://git.libre-soc.org/git/soc.git
-
- cd nmutil; make install; cd ..
- cd ieee754fpu; make install; cd ..
- cd soc; make gitupdate; make install; cd ..
-
- python3 soc/src/soc/decoder/power_decoder.py
- yosys -p "read_ilang decoder.il; show dec31"
-
-## Gtkwave Tutorial
-
-[[Documentation/gtkwave_tutorial]]
-
-## Formal proof notes
-
-[[Documentation/notes_on_formal_proofs]]
+++ /dev/null
-# 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
-<https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/stageapi.py;hb=HEAD>)
-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://github.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:
-<https://bugs.libre-soc.org/show_bug.cgi?id=429#c3> 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.
-
--- /dev/null
+# Documentation
+
+A draft version of the specification is available at <https://ftp.libre-soc.org/power-spec-draft.pdf>
+
+## Codebase Structure
+
+The SOC is partitioned into three repositories. The subrepositories are intended as standalone projects useful outside of LibreSOC. For example, the IEE754 FPU repository is a general purpose IEEE754 toolkit for the construction of FSMs and arbitrary length pipelines.
+
+| Git Repo | Documentation | Description
+|----------|---------------|---------------|
+| [SOC](https://git.libre-soc.org/?p=soc.git;a=tree) | [[SOC Docs|3d_gpu/architecture]] | Main POWER9 GPU |
+| [FPU](https://git.libre-soc.org/?p=ieee754fpu.git;a=tree) | -- | Equivalent to hardfloat-3 |
+| [nmutil](https://git.libre-soc.org/?p=nmutil.git;a=tree) | -- | Equivalent to Chisel3.util |
+
+## Installing the Codebase
+
+ pip3 install virtualenv requests
+ mkdir ~/.virtualenvs && cd ~/.virtualenvs
+ python3 -m venv libresoc
+ source ~/.virtualenvs/libresoc/bin/activate
+
+ cd ~; mkdir libresoc; cd libresoc
+ git clone https://git.libre-soc.org/git/nmutil.git
+ git clone https://git.libre-soc.org/git/ieee754fpu.git
+ git clone https://git.libre-soc.org/git/soc.git
+
+ cd nmutil; make install; cd ..
+ cd ieee754fpu; make install; cd ..
+ cd soc; make gitupdate; make install; cd ..
+
+ python3 soc/src/soc/decoder/power_decoder.py
+ yosys -p "read_ilang decoder.il; show dec31"
+
+## Gtkwave Tutorial
+
+[[docs/gtkwave_tutorial]]
+
+## Formal proof notes
+
+[[docs/notes_on_formal_proofs]]
--- /dev/null
+The SOC is designed to be compliant with POWER 3.0B with somewhere near
+300 instructions excluding Vector instructions.
+
+# Decoder
+
+The page on the decoder is here: [[architecture/decoder]]
--- /dev/null
+[[!img 2020-08-15_12-04.png size="800x" ]]
+
+This tutorial is about generating better GTKWave documents (*.gtkw)
+from Python. The goal is to ease analysis of traces generated by
+unit-tests, and at the same time to better understand the inner working
+of modules, for which we are writing such tests.
+
+# Stylish GTKWave Documents
+
+In this tutorial, you will learn how to:
+
+1. Use individual trace colors.
+ For instance, use different color styles for input, output, debug and
+ internal traces.
+2. Use numeric bases besides the default hex.
+3. Create collapsible trace groups
+ Useful to hide and show, at once, groups of debug, internal and
+ sub-module traces.
+ Select the opening or closing brace, then use the T key.
+4. Add comments in the signal names pane
+5. Change the displayed name of a trace
+6. Use a sane default for initial zoom level
+7. Place markers on interesting places
+8. Put the generating file name as a comment in the file
+
+## Basic trace display
+
+First, we need a VCD file. Try:
+
+ python -m nmutil.test.example_gtkwave
+
+Among other files, it will generate ``test_shifter.vcd``.
+
+Lets write a simple GTKW document. First, import the function:
+
+ from nmutil.gtkw import write_gtkw
+
+Create a list of the traces you want to see. Some hints:
+
+1. Put all trace names in quotes.
+2. Use the same names as you would see in the trace pane of GTKWave
+3. If a trace is multi-bit, use array notation 'name[max:min]'
+
+For example:
+
+ traces = [
+ 'clk',
+ # prev port
+ 'op__sdir', 'p_data_i[7:0]', 'p_shift_i[7:0]', 'p_valid_i', 'p_ready_o',
+ # internal signals
+ 'fsm_state', 'count[3:0]', 'shift_reg[7:0]',
+ # next port
+ 'n_data_o[7:0]', 'n_valid_o', 'n_ready_i'
+ ]
+
+Now, create the document:
+
+ write_gtkw("simple.gtkw", "test_shifter.vcd", traces, module='top.shf')
+
+Remarks:
+
+1. ``simple.gtkw`` is the name of our GTKWave document
+2. ``test_shifter.vcd`` is the VCD file
+3. ``traces`` is a list of trace names
+4. ``top.shf`` is the hierarchy path of the module
+
+Now try:
+
+ gtkwave simple.gtkw
+
+Notice:
+
+1. No need to press the "zoom to fit" button. The default zoom level is
+adequate for a 1 MHz clock.
+2. If you made a mistake, there will be no warning. The trace will
+simply not appear
+3. The reload button will only reload the VCD file, not the GTKW document. If you regenerate the document, you need to close and open a
+new tab, or exit GTKWave and run again: ``gtkwave simple.gtkw``
+4. If you feel tired of seeing the GTKWave splash window every time,
+do: ``echo splash_disable 1 >> ~/.gtkwaverc``
+5. If you modify the document manually, better to save it with another
+name
+
+## Adding color
+
+Go back to the trace list and replace the ``'op__sdir'`` string with:
+
+ ('op__sdir', {'color': 'orange'})
+
+Recreate the document (you can change the file name):
+
+ write_gtkw("color.gtkw", "test_shifter.vcd", traces, module='top.shf')
+
+If you now run ``gtkwave color.gtkw``, you will see that ``op__sdir``
+has the new color.
+
+## Writing GTKWave documents, with style
+
+Let's say we want all input traces be orange, and all output traces be
+yellow. To change them one by one, as we did with ``op__sdir``, would be
+very tedious and verbose. Also, hardcoding the color name will make it
+difficult to change it later.
+
+To solve this, lets create a style specification:
+
+ style = {
+ 'in': {'color': 'orange'},
+ 'out': {'color': 'yellow'}
+ }
+
+Then, change:
+
+ ('op__sdir', {'color': 'orange'})
+
+to:
+
+ ('op__sdir', 'in')
+
+then (notice how we add ``style``):
+
+ write_gtkw("style1.gtkw", "test_shifter.vcd", traces, style, module='top.shf')
+
+If you now run ``gtkwave style1.gtkw``, you will see that ``op__sdir``
+still has the new color.
+
+Let's add more color:
+
+ traces = [
+ 'clk',
+ # prev port
+ ('op__sdir', 'in'),
+ ('p_data_i[7:0]', 'in'),
+ ('p_shift_i[7:0]', 'in'),
+ ('p_valid_i', 'in'),
+ ('p_ready_o', 'out'),
+ # internal signals
+ 'fsm_state',
+ 'count[3:0]',
+ 'shift_reg[7:0]',
+ # next port
+ ('n_data_o[7:0]', 'out'),
+ ('n_valid_o', 'out'),
+ ('n_ready_i', 'in'),
+ ]
+
+Then
+
+ write_gtkw("style2.gtkw", "test_shifter.vcd", traces, style, module='top.shf')
+
+If you now run ``gtkwave style2.gtkw``, you will see that input, output and internal signals have different color.
+
+# New signals at simulation time
+
+At simulation time, you can declare a new signal, and use it inside
+the test case, as any other signal. By including it in the "traces"
+parameter of Simulator.write_vcd, it is included in the trace dump
+file.
+
+Useful for adding "printf" style debugging for GTKWave.
+
+# String traces
+
+When declaring a Signal, you can pass a custom decoder that
+translates the Signal logic level to a string. nMigen uses this
+internally to display Enum traces, but it is available for general
+use.
+
+Some applications are:
+
+1. Display a string when a signal is at high level, otherwise show a
+ single horizontal line. Useful to draw attention to a time interval.
+2. Display the stages of a unit test
+3. Display arbitrary debug statements along the timeline.
--- /dev/null
+# 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
+<https://git.libre-soc.org/?p=nmutil.git;a=blob;f=src/nmutil/stageapi.py;hb=HEAD>)
+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://github.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:
+<https://bugs.libre-soc.org/show_bug.cgi?id=429#c3> 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.
+
# Documentation
- - [Source Code](/Documentation/index)
+ - [Source Code](/docs/)
- [Architecture](3d_gpu/architecture)
| [[conferences]] |
| [[HDL_workflow]] |
| [Simple-V OpenPOWER Draft](/openpower/sv/) |
-| [Documentation](/Documentation/index) |
+| [Documentation](/docs/) |
| [Bugs and Tasks][2] |
| [Mailing Lists][3] |
| [List Archives][4] |
projects / libreriscv.git / commitdiff
