From 842bc30f5a44971c1551ed88cadb6e70d5329f8d Mon Sep 17 00:00:00 2001 From: Tim Hutt Date: Tue, 17 Sep 2024 09:28:34 +0100 Subject: [PATCH] Update README.md Co-authored-by: Alexander Richardson Signed-off-by: Tim Hutt --- README.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/README.md b/README.md index d8edcca03..79ca3f6d1 100644 --- a/README.md +++ b/README.md @@ -36,7 +36,7 @@ What is Sail? engineer-friendly language, much like earlier vendor pseudocode, but more precisely defined and with tooling to support a wide range of use-cases.

-Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate an executable emulators, show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate theorem-prover definitions for +Given a Sail specification, the tool can type-check it, generate documentation snippets (in LaTeX or AsciiDoc), generate executable emulators, show specification coverage, generate versions of the ISA for relaxed memory model tools, support automated instruction-sequence test generation, generate theorem-prover definitions for interactive proof (in Isabelle, HOL4, and Coq), support proof about binary code (in Islaris), and (in progress) generate a reference ISA model in SystemVerilog that can be used for formal hardware verification.