updates/018_2019may27_nlnet_grant_approved.mdwn

   1 # First NLNet Grant approved to fund development of the Libre RISC-V SoC
   2
   3 The application for funding from NLnet, from back in November of last year,
   4 has been approved.  It means that we have EUR $50,000 to pay for full-time
   5 engineering work to be carried out over the next year, and to pay for
   6 "bounty" style tasks.  For the right people, with the right skills, there
   7 is money now available.
   8
   9 However this is not all: by splitting the tasks up into separate groups,
  10 and using a second European-based individual as the applicant, we can
  11 apply for a second grant (also of up to EUR $50,000).  In the next couple
  12 of days we will put in an application for "Formal Mathematical Proofs"
  13 of the processor design.
  14
  15 There are several reasons for doing so.  The primary one is down to the
  16 fact that we anticipate this (commercial, libre) product to be closely
  17 and independently examined by third parties, to verify for themselves
  18 that it does not contain spying backdoor co-processors, as well as the
  19 usual security and correctness guarantees.  If there exists *formal
  20 mathematical proofs* that the processor and its sub-components operate
  21 correctly, that independent 3rd party verification task is a lot easier.
  22
  23 In addition, it turns out that when writing unit tests, using formal
  24 mathematical proofs makes for *complete* code coverage - far better
  25 than any other "comprehensive" multiple unit test technique could ever
  26 hope to achieve - with less code and not just better accuracy but *100%
  27 provable* accuracy.  Additional, much simpler unit tests can then be written
  28 which are more along the lines of "HOWTOs" - examples on how to use the
  29 unit.
  30
  31 This is one of those "epiphany" moments that, as a Software Engineer of
  32 25 years experience, has me stunned and wondering why on earth this is
  33 not more generally and widely deployed in software. The answer I believe
  34 is down to the nature of what a processor actually is.
  35
  36 A processor is developed much more along the lines of how Functional Programming
  37 works.  Functional Programming can have formal mathematical proofs applied
  38 to it because for any given inputs, the output is *guaranteed* to be the same.
  39 This of course breaks down when the function has "side-effects" (such as
  40 reading from a file or accesses other external state outside of the "control"
  41 of the function).  And in the design of a processor, by the very nature
  42 of hardware, you simply cannot create a verilog module that has access to
  43 "files" or to "global variables".
  44
  45 In addition, hardware is based purely on boolean logic, and on if/else
  46 constructs.  In essence, then the *entire hardware design* has to be made
  47 according to far simpler rules than "normal" software is expected to conform
  48 to.  Even memory accesses in hardware have to be implemented according to
  49 these strict rules (we're *implementing* LOAD and STORE instructions, here,
  50 not *using* those LOAD and STORE instructions).
  51
  52 Consequently, adding in formal proofs is a little bit easier, brings
  53 huge benefits as well in terms of code readability, reliability, and
  54 time-cost savings, and has the crucial advantage of being aligned with
  55 the overall privacy goal *and* with NLnet's funding remit.
  56
  57 # Summary from the past couple of months
  58
  59 The past few months have seen a *lot* of activity.  The IEEE754 ADD unit
  60 has been completed, both as a Finite State Machine (FSM) and as a fully
  61 pipelined design, both of which have parameters that allow them to do
  62 FP16, FP32 or FP64.  The DIV unit has been implemented as an FSM, and
  63 will stay that way for now.  MUL has been completed, however needs to
  64 be turned into an FMAC (3 operands: Multiply and Accumulate).
  65
  66 A provisional pipeline API has been developed, which the IEEE754 FPU
  67 is using.  It includes data "funneling" (multiplexing) blocks that allow
  68 for the creation of what Mitch Alsup calls a "Concurrent Computation Unit".
  69 It's basically an array of matched operand latches and result latches
  70 (as input and output, respectively), in front of a single pipeline.
  71 This arrangement allows a batch of operations to be presented to the
  72 CDC6600 style "Dependency Matrices".
  73
  74 Jacob has been working on a fascinating design: a dynamically partitionable
  75 Adder and Multiplier Unit.  Given that we are doing a Vector Processing
  76 front-end onto SIMD back-end operations, it makes sense to save gates by
  77 allowing the ADD and MUL units to be able to optionally handle a batch
  78 of 8-bit operations, or half the number of 16-bit operations, or a quarter
  79 of the number of 32-bit operations or one eighth of the number of 64-bit
  80 operations.  In this way, a lot less gates are required than if they
  81 were separate units.  The unit tests demonstrate that the code that Jacob
  82 has written provide RISC-V mul, mulh, mulhu and mulhsu functionality.
  83
  84 The augmented 6600 Scoreboard took literally six weeks to correctly implement
  85 Read-after-Write and Write-after-Read hazards.  It required extraordinary
  86 and excruciating patience to get right.  Adding in Write-after-Write
  87 however only took two days, as the infrastructure to do so had already been
  88 developed.
  89
  90 Currently being implemented is "branch shadowing" - this is not the
  91 same as branch *prediction*: that is a different algorithm which, when
  92 *combined* with "branch shadowing", provides the feature known as branch
  93 *speculation*.  This is the source of a lot of confusion about Out-of-Order
  94 designs in general.  It seems to be assumed that an OoO design *has* to
  95 have branch speculation: it doesn't.  It's just that, given all the
  96 pieces, adding in branch speculation is actually quite straightforward,
  97 and provides such a high performance increase that it is hard to justify
  98 leaving it out.
  99
 100 One huge surprise came out of a recent discussion with Mitch Alsup.  It
 101 has been assumed all along that turning this design from a single-issue
 102 to multi-issue would be difficult, or require significant gates and latency
 103 to do so.  The "simple" approach to do multi-issue, using the Dependency
 104 Matrices, would be to analyse a batch of instructions, and if there are
 105 no overlaps (no registers in common), allow that batch to proceed in
 106 parallel.  This is a naive approach.
 107
 108 Mitch pointed out that in his work on the AMD Opteron (the processor
 109 family that AMD had to publish "Intel equivalent" speed numbers for,
 110 because it was so much more efficient and effective than Intel's designs)
 111 each instruction "accumulated" the dependencies of all prior instructions
 112 being issued in the same batch.  This works because read and write
 113 dependencies are *transitive* (google it...)
 114
 115 What that means, in practical terms, is that we have a way to create a
 116 design that could, if ramped up, "take on the big boys".  To make that
 117 clear: there's no technical barrier that would prevent us from creating
 118 a quad issue (or higher) design.
 119
 120 There is still a heck of a lot to get done, here.  However, it has to
 121 be said that actually adding an instruction decoder onto the 6600 style
 122 Dependency Matrices is relatively straightforward, this being RISC, after
 123 all.  It is possible, then, that we may have a subset of functionality
 124 operational far sooner than anticipated.