From: lkcl Date: Sun, 22 Sep 2019 17:56:58 +0000 (+0100) Subject: (no commit message) X-Git-Tag: convert-csv-opcode-to-binary~4007 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=44070b31b63eb4feeacb717c995b8450802d1ec5;p=libreriscv.git --- diff --git a/nlnet_2019_formal.mdwn b/nlnet_2019_formal.mdwn index a7551d77f..cce0c3ea4 100644 --- a/nlnet_2019_formal.mdwn +++ b/nlnet_2019_formal.mdwn @@ -43,7 +43,7 @@ EUR 50,000. # Explain what the requested budget will be used for? -Working with mathematically-minded Software Engineers, every module in the Libre RISCV SoC will have a "formal proof unit test written". This is an unusual dedisn choice: most hardware designs will have monte carlo and corner case unit tests etc. written which, unfortunately, are both complex and often incomplete. +Working with mathematically-minded Software Engineers, every module in the Libre RISCV SoC will have a "formal proof unit test written". This is an unusual design choice: most hardware designs will have monte carlo and corner case unit tests etc. written which, unfortunately, are both complex and often incomplete. Examples include the IEEE754 Floating Point Unit, where in the 1990s Intel managed to introduce an actual hardware division bug. We seek to formally *prove* that the output from the FP Divide unit outputs the correct answer, for all possible inputs. @@ -75,6 +75,8 @@ In addition, we will be using an unusual choice of HDL: a python based tool. We Luckily we have several examples already, in the form of the work carried out by the developer of the Kestrel 53000 series of CPUs. +The other main challenge is that as the size of the code being tested goes up, the CPU resources required go up exponentially. At the low level it is fine: tests can take several hours on a standard high end desktop. However as things progress to larger levels we may actually need access to Beowulf Clusters or other supercomputing resources. + ## Describe the ecosystem of the project, and how you will engage with relevant actors and promote the outcomes? As mentioned in the 2018 submission, the Libre RISC-V