diff --git a/README.md b/README.md index 3214c9c..ed2dba9 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ WARP-V is an open-source CPU core generator written in TL-Verilog with support for RISC-V and MIPS I. It is a demonstration and exploration vehicle for the flexibility that is possible using the emerging "transaction-level design" methodology. It can implement a single-stage, low-power microcontroller or a mid-range 7-stage CPU. Even the instruction-set architectures (ISAs) is configurable. WARP-V is an evolving library of CPU components as well as various compositions of them. It is driven by a community interested in transforming the silicon industry through open-source hardware and revolutionary design methodology. -WARP-V includes CPU core logic only with no current support for virtual memory, caches, or IOs. RISC-V implementations are formally verified using open-source tools in continuous integration testing. +WARP-V includes CPU core logic only with no current support for virtual memory, caches, or IOs. RISC-V implementations are formally verified using open-source tools in continuous integration testing. They have been [formally verified also by Axiomise](https://semiwiki.com/eda/302631-accelerating-exhaustive-and-complete-verification-of-risc-v-processors/). # Links @@ -154,6 +154,7 @@ WARP-V RISC-V implementations are verified using the Upscale might be a good direction for future work.) +RISC-V WARP-V cores have also been [formally verified by Axiomise](https://semiwiki.com/eda/302631-accelerating-exhaustive-and-complete-verification-of-risc-v-processors/) with some [issues outstanding](https://github.com/darbaria/axiomise-warpv-formal-6-stage/issues).