From: pham.michael.98@a029fe8ac2da19fcd7269c492cf0410b2e5fd4cc Date: Mon, 23 Sep 2019 14:24:00 +0000 (+0100) Subject: Add new section for formal verification and learning resources X-Git-Tag: convert-csv-opcode-to-binary~3986 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6d54ef7a7daf119a4238792e584a930eaf494436;p=libreriscv.git Add new section for formal verification and learning resources --- diff --git a/resources.mdwn b/resources.mdwn index b20c3f40d..ba4b5b694 100644 --- a/resources.mdwn +++ b/resources.mdwn @@ -75,8 +75,8 @@ switching between different accuracy levels, in userspace applications. * OpenCL 2.2 SPIR-V Environment Specification: -Note: We are implementing hardware accelerated Vulkan (and possibly -OpenCL) while relying on other software projects to translate APIs to +Note: We are implementing hardware accelerated Vulkan and +OpenCL while relying on other software projects to translate APIs to Vulkan. E.g. Zink allows for OpenGL-to-Vulkan in software. # Graphics and Compute API Stack @@ -152,3 +152,21 @@ MAJOR NOTE: We are **not** allowed to say we are compliant with any of the Khronos standards until we actually make an official submission, do the paperwork, and pay the relevant fees. +## Formal Verification +Formal verification of Libre RISC-V ensures that it is bug-free in regards to what we specify. +Of course, it is important to do the formal verification as a final step in the development process before +we produce thousands or millions of silicon. + +Some learning resources I found in the community: + +* ZipCPU: + +ZipCPU provides a comprehensive tutorial for beginners and many exercises/quizzes/slides: + + +* Western Digital's SweRV CPU blog (I recommend looking at all their posts): + + + + +