From: Luke Kenneth Casson Leighton Date: Sun, 18 Apr 2021 10:16:58 +0000 (+0100) Subject: reorganise docs (shorten URL) X-Git-Tag: DRAFT_SVP64_0_1~1069 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=42fd142884363f878b0fb6437701fc7114aa5f63;p=libreriscv.git reorganise docs (shorten URL) --- diff --git a/Documentation/SOC/index.mdwn b/Documentation/SOC/index.mdwn deleted file mode 100644 index 26c45d581..000000000 --- a/Documentation/SOC/index.mdwn +++ /dev/null @@ -1,6 +0,0 @@ -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]] diff --git a/Documentation/gtkwave_tutorial.mdwn b/Documentation/gtkwave_tutorial.mdwn deleted file mode 100644 index 6a1132d11..000000000 --- a/Documentation/gtkwave_tutorial.mdwn +++ /dev/null @@ -1,173 +0,0 @@ -[[!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. diff --git a/Documentation/gtkwave_tutorial/2020-08-15_12-04.png b/Documentation/gtkwave_tutorial/2020-08-15_12-04.png deleted file mode 100644 index d89a0789e..000000000 Binary files a/Documentation/gtkwave_tutorial/2020-08-15_12-04.png and /dev/null differ diff --git a/Documentation/index.mdwn b/Documentation/index.mdwn deleted file mode 100644 index 08276920a..000000000 --- a/Documentation/index.mdwn +++ /dev/null @@ -1,40 +0,0 @@ -# Documentation - -A draft version of the specification is available at - -## 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]] diff --git a/Documentation/notes_on_formal_proofs.mdwn b/Documentation/notes_on_formal_proofs.mdwn deleted file mode 100644 index 1186868c8..000000000 --- a/Documentation/notes_on_formal_proofs.mdwn +++ /dev/null @@ -1,220 +0,0 @@ -# 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://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: - 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. - diff --git a/docs.mdwn b/docs.mdwn new file mode 100644 index 000000000..78e360292 --- /dev/null +++ b/docs.mdwn @@ -0,0 +1,40 @@ +# Documentation + +A draft version of the specification is available at + +## 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]] diff --git a/docs/SOC/index.mdwn b/docs/SOC/index.mdwn new file mode 100644 index 000000000..26c45d581 --- /dev/null +++ b/docs/SOC/index.mdwn @@ -0,0 +1,6 @@ +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]] diff --git a/docs/gtkwave_tutorial.mdwn b/docs/gtkwave_tutorial.mdwn new file mode 100644 index 000000000..6a1132d11 --- /dev/null +++ b/docs/gtkwave_tutorial.mdwn @@ -0,0 +1,173 @@ +[[!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. diff --git a/docs/gtkwave_tutorial/2020-08-15_12-04.png b/docs/gtkwave_tutorial/2020-08-15_12-04.png new file mode 100644 index 000000000..d89a0789e Binary files /dev/null and b/docs/gtkwave_tutorial/2020-08-15_12-04.png differ diff --git a/docs/notes_on_formal_proofs.mdwn b/docs/notes_on_formal_proofs.mdwn new file mode 100644 index 000000000..1186868c8 --- /dev/null +++ b/docs/notes_on_formal_proofs.mdwn @@ -0,0 +1,220 @@ +# 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://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: + 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. + diff --git a/index.mdwn b/index.mdwn index 6f9b670c9..980497822 100644 --- a/index.mdwn +++ b/index.mdwn @@ -179,5 +179,5 @@ are quite welcome. # Documentation - - [Source Code](/Documentation/index) + - [Source Code](/docs/) - [Architecture](3d_gpu/architecture) diff --git a/sidebar.mdwn b/sidebar.mdwn index 87d10afac..205e2bf03 100644 --- a/sidebar.mdwn +++ b/sidebar.mdwn @@ -5,7 +5,7 @@ | [[conferences]] | | [[HDL_workflow]] | | [Simple-V OpenPOWER Draft](/openpower/sv/) | -| [Documentation](/Documentation/index) | +| [Documentation](/docs/) | | [Bugs and Tasks][2] | | [Mailing Lists][3] | | [List Archives][4] |