(no commit message)

diff --git a/nlnet_2019_formal.mdwn b/nlnet_2019_formal.mdwn
index a7551d77f48991fe128436d1af27dd5901f1d3c9..cce0c3ea4cc7f3ac3c45c555fe0937752eba084f 100644 (file)
--- 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