From: lkcl Date: Sat, 8 Feb 2020 17:01:58 +0000 (+0000) Subject: (no commit message) X-Git-Tag: convert-csv-opcode-to-binary~3508 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b0dbea9c50018964cfd91ac598a5db502376ed8;p=libreriscv.git --- diff --git a/why_a_libresoc.mdwn b/why_a_libresoc.mdwn index 161040d3d..8a643f1d0 100644 --- a/why_a_libresoc.mdwn +++ b/why_a_libresoc.mdwn @@ -16,7 +16,7 @@ Our LibreSOC will not have backdoors that plague modern [processors](https://www There is a very real need for reliable safety critical processors (think airplane, smart car, nuclear power plant, pacemaker...). LibreSOC posits that it is impossible to trust a processor in a safety critical environment without both access -to that processor's source and a cycle accurate HDL simulator that guarantees developers their code behaves as they -expect. An ISA level simulator is no longer satisfactory. +to that processor's source, a cycle accurate HDL simulator that guarantees developers their code behaves as they +expect, and formal correctness proofs. An ISA level simulator is no longer satisfactory. Refer to this [IEEE article](https://ieeexplore.ieee.org/document/4519604) by Cyberphysical System expert Ed-Lee for more details.