From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Tue, 2 Aug 2022 13:44:55 +0000 (+0100)
Subject: add to resources formal proof for VAMP CPU
X-Git-Tag: opf_rfc_ls005_v1~907
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=75368c1ddb0d546b808433ee09c88be9bb51b240;p=libreriscv.git

add to resources formal proof for VAMP CPU
---

diff --git a/resources.mdwn b/resources.mdwn
index a517af850..d3c0151d3 100644
--- a/resources.mdwn
+++ b/resources.mdwn
@@ -325,6 +325,15 @@ Some learning resources I found in the community:
 * <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>
 
+VAMP CPU
+
+* Formal verification of a fully IEEE compliant floating point unit
+https://publikationen.sulb.uni-saarland.de/bitstream/20.500.11880/25760/1/ChristianJacobi_ProfDrWolfgangJPaul.pdf
+* https://www-wjp.cs.uni-sb.de/forschung/projekte/VAMP/?lang=en
+* the PVS/hw subfolder is under the 2-clause BSD license:
+    https://www-wjp.cs.uni-sb.de/forschung/projekte/VAMP/PVS/hw/COPYRIGHT
+* https://alastairreid.github.io/RelatedWork/papers/beyer:ijsttt:2006/
+
 ## Automation
 
 * <https://www.ohwr.org/project/wishbone-gen>