Add new section for formal verification and learning resources

diff --git a/resources.mdwn b/resources.mdwn
index b20c3f40d2534eb8fdc3fc04c13d48709d371121..ba4b5b694902d5d57b6c08ae650312d2fe49fc1e 100644 (file)
--- 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:
   <https://www.khronos.org/registry/OpenCL/specs/2.2/html/OpenCL_Env.html>
 
 * OpenCL 2.2 SPIR-V Environment Specification:
   <https://www.khronos.org/registry/OpenCL/specs/2.2/html/OpenCL_Env.html>
 

-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
 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.
 
 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: <http://zipcpu.com/>
+
+ZipCPU provides a comprehensive tutorial for beginners and many exercises/quizzes/slides: <http://zipcpu.com/tutorial/>
+
+
+* Western Digital's SweRV CPU blog (I recommend looking at all their posts): <https://tomverbeure.github.io/>
+
+<https://tomverbeure.github.io/risc-v/2018/11/19/A-Bug-Free-RISC-V-Core-without-Simulation.html>
+
+<https://tomverbeure.github.io/rtl/2019/01/04/Under-the-Hood-of-Formal-Verification.html>
+