From: lkcl Date: Sun, 12 Jan 2020 20:59:39 +0000 (+0000) Subject: (no commit message) X-Git-Tag: convert-csv-opcode-to-binary~3809 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=dec015d0b6c9d58acc36b49e450a9650eee1047c;p=libreriscv.git --- diff --git a/nlnet_2019_formal.mdwn b/nlnet_2019_formal.mdwn index 4d2a06c7f..e26dc38d1 100644 --- a/nlnet_2019_formal.mdwn +++ b/nlnet_2019_formal.mdwn @@ -1,4 +1,4 @@ -# NL.net proposal +# NL.net proposal 2019-10-046 ## Project name @@ -153,3 +153,7 @@ all picked up the story. The list is updated and maintained here: * * * + +# Management Summary + +The Libre RISC-V SoC Project, https://nlnet.nl/project/Libre-RISCV/, is funded by NLNet to reach ASIC-proven status. As of Dec 2019 It has been in development for a year, and writing comprehensive unit tests has been both a critical part of that process and a major part of the time taken. Formal Mathematical Proofs turn out to be critical for several reasons: firstly, they are simpler to read and much more comprehensive (100% coverage), saving hugely on development and maintenance; secondly, they're mathematically inviolate. From a security and trust perspective, both aspects are extremely important. Firstly: security mistakes are often accidental due to complexity: a reduction in complexity helps avoid mistakes. Secondly: independent auditing of the processor is a matter of running the formal proofs. This proposal therefore not only saves on development time, it helps us meet the goal of developing a privacy-respecting processor in a way that is *independently* verifiable.