From 3b02b2c927e0d5d79aaa1fb43ca7472cb326c3d9 Mon Sep 17 00:00:00 2001 From: lkcl Date: Wed, 5 Oct 2022 18:09:05 +0100 Subject: [PATCH] --- nlnet_2022_ongoing/discussion.mdwn | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) 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 ** 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 -- 2.30.2