From: lkcl Date: Thu, 23 Jan 2020 21:51:06 +0000 (+0000) Subject: (no commit message) X-Git-Tag: convert-csv-opcode-to-binary~3744 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f8f1995055378e2c2839c3ca38bebb59ff900c17;p=libreriscv.git --- diff --git a/HDL_workflow.mdwn b/HDL_workflow.mdwn index 7e0e584f3..3a63d6024 100644 --- a/HDL_workflow.mdwn +++ b/HDL_workflow.mdwn @@ -237,7 +237,7 @@ Thanks to Samuel Falvo we learned that writing unit tests as a formal proof is n No this is not a joke or hypothetical. -The ieee754fpu requires several hundreds of thousands of tests to be run, and even then we cannot be absolutely certain that all possible combinations of input have been tested. With 2^128 permutations to try with 2 64 bit FP numbers it is simply impossible to even try. +The ieee754fpu requires several hundreds of thousands of tests to be run (currently needing several days to run them all), and even then we cannot be absolutely certain that all possible combinations of input have been tested. With 2^128 permutations to try with 2 64 bit FP numbers it is simply impossible to even try. This is where formal proofs come into play.