diff options
| author | Peter Sewell | 2019-01-13 09:45:59 +0000 |
|---|---|---|
| committer | Peter Sewell | 2019-01-13 09:45:59 +0000 |
| commit | a3da2efb3ef08e132e16db0c510b1b8fe4ee600c (patch) | |
| tree | 6ef395c8a910eed766386838f532ad736d4c67f8 /README.md | |
| parent | af5e6e4d11d9df0bd2058ef3cc5b69d877c001ef (diff) | |
update README
Diffstat (limited to 'README.md')
| -rw-r--r-- | README.md | 14 |
1 files changed, 14 insertions, 0 deletions
@@ -12,6 +12,20 @@ language, but with lightweight dependent typing for numeric types and bitvector lengths, which are automatically checked using Z3. It has been used for several papers, available from <http://www.cl.cam.ac.uk/~pes20/sail/>. +<p> + +Given a Sail definition, the tool will type-check it and generate +executable emulators, in C and OCaml, theorem-prover definitions for +Isabelle, HOL4, and Coq, and definitions to integrate with our +<a href="http://www.cl.cam.ac.uk/users/pes20/rmem">RMEM</a> tool for +concurrency semantics. This is all work in progress, and some +theorem-prover definitions do not yet work for the more complex +models; see the most recent papers and the ARMv8.5-A model for +descriptions of the current state. +<p> + + <img src="https://www.cl.cam.ac.uk/~pes20/sail/overview-sail.png"> +<p> This repository contains the implementation of Sail, together with some Sail specifications and related tools. |