Add README

README.md

@@ -0,0 +1,81 @@
+## Synchronous Model Generation Tool
+
+### Overview
+
+This repository contains a tool for creating equivalent synchronous circuits
+or *synchronous models* for asynchronous circuits.
+
+The models can be used as drop-in replacements for async circuits in
+conventional (sync) simulation and formal verification, enabling users to
+leverage existing (sync) tools, design flows, formalisms and knowledge to
+simulate and verify async circuits. They have the same interface, with added
+`clk` and `reset` pins.
+
+For more information on the tool please refer to:
+
+- The paper [Formal Verification of Mixed Synchronous Asynchronous Systems using
+Industrial Tools](https://github.com/tuura/sync-models-paper)
+
+- The accompanying [presentation
+slides](https://tuura.github.io/sync-models-paper/slides/)
+
+### How to Use
+
+The main tool is `generator.py`, a Verilog code generator based on
+[Jinja](http://jinja.pocoo.org).
+
+#### Usage
+
+```
+Usage:
+  generator.py <circuit.v> <spec.sg> <templates> <gendir>
+```
+
+To create a sync model, three inputs are required:
+
+1. An async circuit in gate-level Verilog
+2. Circuit specification as a state graph
+3. A code generation template (included in the directory `templates`)
+
+The tool generates two Verilog modules: a sync model (`circuit.v`) and an
+accompanying spec FSM (`spec.v`). An instance of the FSM is instantiated
+within the model and is simulated in tandem with the circuit to check for
+transition compliance (more details on this are in the paper).
+
+The input circuit and its spec can be created using tools such as
+[Workcraft](https://workcraft.org/).
+
+#### Templates
+
+The tool relies on template verilog files. This enables it to generate
+synchronous model variations that are optimized for different criteria (e.g.
+performance vs. debuggability) or more compatible with certain tools.
+
+At the moment, three templates are provided:
+
+1. Standard template (`templates/ifv`): tested with Cadence Incisive Formal
+and generally works well with all tools supporting the Verilog 1995 standard.
+
+2. High performance template (`templates/ifv-perf`): omits some checks,
+optimized for performance.
+
+3. Xprova's template (`templates/xprova`): generates model and properties for
+the formal verification tool [Xprova](https://github.com/xprova/xprova).
+
+### Formal Verification Tool: ESSET
+
+The repository contains a low-performance verification tool `verifier.py`
+referred to in the paper as the Exhaustive State Space Exploration Tool
+(ESSET). It's a compliance checker used mainly to cross-validate verification
+results with other tools.
+
+#### Usage
+
+```
+Usage:
+  verifier.py [options] <circuit.v> <spec.sg>
+
+Options:
+  -q --quiet      Suppress printing state exploration details.
+  -l --lib=<dir>  Load libraries from specific directory [default: libraries].
+  ```