add to resources formal proof for VAMP CPU
authorLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Tue, 2 Aug 2022 13:44:55 +0000 (14:44 +0100)
committerLuke Kenneth Casson Leighton <lkcl@lkcl.net>
Tue, 2 Aug 2022 13:44:55 +0000 (14:44 +0100)
resources.mdwn

index a517af850f62cd71b36286c0cac7f5f8c1171427..d3c0151d36ec36f423854a2cfa204edfb319450b 100644 (file)
@@ -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>