(no commit message)

diff --git a/nlnet_2019_formal.mdwn b/nlnet_2019_formal.mdwn
index 9b59dda5f6dc377243265b8c367940bd0c91e14b..a04486dca60bfbcaabd7f2428a6ddd2a7be466cf 100644 (file)
--- a/nlnet_2019_formal.mdwn
+++ b/nlnet_2019_formal.mdwn
@@ -64,17 +64,19 @@ The formal correctness testing requires specialist expertise involving formal lo
 
 # Compare your own project with existing or historical efforts.
 
-There do exist high level formal RISCV Cotrectness proofs in various forms. One of these is the SymbioticEDA formal RISCV proof which can for example test the Register File, and test that the integer operation is correct and so on, working its way through all operations one by one.  This however is at a high level.
+There do exist high level formal RISCV Correctness proofs in various forms. One of these is the SymbioticEDA formal RISCV proof which can for example test the Register File, and test that the integer operation is correct and so on, working its way through all operations one by one.  This however is at a high level.
 
 The Kestrel 53000 Series of embedded controllers have some formal unit tests written in verilog, at the lowest level. We are following their development and porting to nmigen closely, and consulting with their part time developer.
 
-A massive comprehensive suite of formal correctness proofs for a processor of the scope and size of the Libre RISCV SoC is just not normally done. The only reason we are considering it is because of the dramatic simplification of unit tests, and the mathematically inviolate guarantees it brings for endusers.
+A massive comprehensive suite of formal correctness proofs for a processor of the scope and size of the Libre RISCV SoC is just not normally done. The only reason we are considering it is because of the dramatic simplification of unit tests that the approach brings, and the mathematically inviolate guarantees it brings for endusers and developers.
 
 ## What are significant technical challenges you expect to solve during the project, if any?
 
-This project is critically dependent on having software engineers that have the mathematical acumen for formal logic correctness proofs. This is quite rare.
+This project is critically dependent on having software engineers that have the mathematical acumen for formal logic correctness proofs. This is quite a rare combination.
 
-In addition, we will be using an unusual choice of HDL: a python based tool. We will need to train engineers to adapt to the unique mathematics, or train mathematicians to the unique software quirks.
+In addition, we are using an unusual choice of HDL: a python based tool called nmigen. Fortunately its backend is yosys, which has well known industry recognised links to formal proof libraries, through symbiyosys.
+
+We will need to train engineers to adapt to the unique mathematics, or train mathematicians to the unique software quirks.
 
 Luckily we have several examples already, in the form of the work carried out by the developer of the Kestrel 53000 series of CPUs.