From 75368c1ddb0d546b808433ee09c88be9bb51b240 Mon Sep 17 00:00:00 2001
From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Tue, 2 Aug 2022 14:44:55 +0100
Subject: [PATCH] add to resources formal proof for VAMP CPU

---
 resources.mdwn | 9 +++++++++
 1 file changed, 9 insertions(+)

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>
-- 
2.30.2