From 5e9006bba9e4a0be80c6cf5c9b1b0acfb289f2c8 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jean-Fran=C3=A7ois=20Nguyen?= <jf@jfng.fr>
Date: Fri, 2 Sep 2022 07:45:16 +0200
Subject: [PATCH] Update README.

---
 README.md      | 26 ++++++++++++++++++++++++--
 pyproject.toml |  2 +-
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index 298e003..dd0b87f 100644
--- a/README.md
+++ b/README.md
@@ -1,6 +1,20 @@
-# power-fv
+# POWER-FV – Assertion-based formal verification library for OpenPOWER processors
 
-(TODO)
+## Disclaimer
+
+*This project is currently in an experimental state. In particular:
+- it has only been tried on the Microwatt CPU
+- it assumes an in-order scalar core
+- its instruction coverage is limited to the Scalar Fixed-point Compliancy Subset
+- the correctness of its own specifications hasn't yet been verified*
+
+## Overview
+
+POWER-FV is a formal verification library that can be used to check the compliance of a processor with the OpenPOWER ISA. It provides an interface to trace the execution of a processor, which is monitored by a testbench and compared against a given specification.
+
+Testbenches and behavioral models are implemented in Python using [Amaranth HDL](https://github.com/amaranth-lang/amaranth), and [SymbiYosys](https://github.com/YosysHQ/sby) for its formal verification flow. Processor cores may use any HDL supported by Yosys.
+
+POWER-FV's design is heavily inspired by the [riscv-formal](https://github.com/YosysHQ/riscv-formal) framework, developed by Claire Wolf (YosysHQ).
 
 ## Prerequisites
 
@@ -8,6 +22,12 @@
 - [Yosys](https://github.com/YosysHQ/yosys)
 - [SymbiYosys (sby)](https://github.com/YosysHQ/sby)
 
+If VHDL support is needed:
+- [GHDL](https://github.com/ghdl/ghdl)
+- [ghdl-yosys-plugin](https://github.com/ghdl/ghdl-yosys-plugin)
+
+The [OSS CAD Suite](github.com/YosysHQ/oss-cad-suite-build) can provide pre-built binaries of these tools.
+
 ## Installation
 
 ```python3
@@ -15,4 +35,6 @@ pip3 install poetry --user
 poetry install
 ```
 
+## Examples
+
 See the `cores` folder for usage examples.
diff --git a/pyproject.toml b/pyproject.toml
index 6f62656..40a4fd1 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -1,7 +1,7 @@
 [tool.poetry]
 name = "power-fv"
 version = "0.1.0"
-description = "Amaranth HDL library for formal verification of POWER processors"
+description = "Assertion-based formal verification library for OpenPOWER processors"
 authors = ["Jean-François Nguyen <jf@jfng.fr>"]
 license = "BSD"