From 6d54ef7a7daf119a4238792e584a930eaf494436 Mon Sep 17 00:00:00 2001 From: "pham.michael.98@a029fe8ac2da19fcd7269c492cf0410b2e5fd4cc" Date: Mon, 23 Sep 2019 15:24:00 +0100 Subject: [PATCH] Add new section for formal verification and learning resources --- resources.mdwn | 22 ++++++++++++++++++++-- 1 file changed, 20 insertions(+), 2 deletions(-) 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): + + + + + -- 2.30.2