From: lkcl <lkcl@web>
Date: Wed, 5 Oct 2022 17:09:05 +0000 (+0100)
Subject: (no commit message)
X-Git-Tag: opf_rfc_ls005_v1~148
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3b02b2c927e0d5d79aaa1fb43ca7472cb326c3d9;p=libreriscv.git

---

diff --git a/nlnet_2022_ongoing/discussion.mdwn b/nlnet_2022_ongoing/discussion.mdwn
index d5df4452e..7a98ae756 100644
--- a/nlnet_2022_ongoing/discussion.mdwn
+++ b/nlnet_2022_ongoing/discussion.mdwn
@@ -1,6 +1,7 @@
 # questions 05 oct 2022
 
-context is from other [[nlnet_2022_opf_isa_wg/discussion]] on 2022-08-051
+context is from other [[nlnet_2022_opf_isa_wg/discussion]] on 2022-08-051.
+mailing list <https://lists.libre-soc.org/pipermail/libre-soc-dev/2022-October/005363.html>
 
 **
     Again there should be a breakdown of the main tasks, and the associated effort.
@@ -14,7 +15,8 @@ tasks, adapted (OpenCAPI is now a secret closed Standard, assigned to a
 group backed by Intel!)
 
 * 2-3 months: Dynamic Partitioned SIMD for nmigen 
-* 3-4 months: Completion of IEEE754 FP Formal Correctness Proofs
+* 5-6 months: Continuation of IEEE754 FP Formal Correctness Proofs, addition
+  of FP Rounding Modes and Power ISA Flags
 * 3-5 months: Completion of an In-Order Single-Issue core implementing SVP64
 * 3-4 months: Addition of the IEEE754 FPU to the Core
 * 3-4 months: Addition of other ALUs and pipelines
@@ -26,7 +28,7 @@ group backed by Intel!)
 * 2-3 months plus hosting costs: Establishment and management of CI
 * 2? months?: two Bitmain 250 FPGA porting (thanks to UOregon)
 
-lower estimate is around 33 months, upper limit is 44, so a EUR 100,000
+lower estimate is around 35 months, upper limit is 46, so a EUR 100,000
 budget @ EUR 3,000/mo is within target (just). may need adjusting or some
 tasks removing, to fit. we cannot risk committing to tasks at too low a
 rate to be able to attract interest and committment.
@@ -61,7 +63,8 @@ The concrete outcomes:
   3rd party extensions, of which the Dynamic SIMD Partitioning Library created under
   2019-02-012 would be the first big showcase.
 * A modern well-documented IEEE754 Floating-Point Library, with Formal Correctess
-  Proofs using modern FOSSHW tools (smt2, symbiyosis) is a big deal in its own right.
+  Proofs using modern FOSSHW tools (smt2, symbiyosis) is a big deal in its own right,
+  and something worth aiming for.
   The only
   other Libre Formal Proof is Academically developed 
   for an older version of IEEE754: we will