diff --git a/README.md b/README.md
index 83fe2b4..47aa3a8 100644
--- a/README.md
+++ b/README.md
@@ -22,7 +22,7 @@ first build the Rust compiler `ver2gal` (see the `compiler/` directory) and run:
 ```
 Where `<CHIP>` is either `gal16v8` or `gal22v10`. The generate JEDEC file will
 be generated in the current directory as `output.jed`. Note this program _must_
-be run in the same directory as the `shrink_sop.tcl` script
+be run in the same directory as the `shrink_sop.tcl` script.
 
 This JEDEC file can be optionally be verified programmatically using the
 scripts and Verilog models found the `models/` directory. 
diff --git a/models/README.md b/models/README.md
new file mode 100644
index 0000000..4584f8b
--- /dev/null
+++ b/models/README.md
@@ -0,0 +1,25 @@
+Model-Based Verification Checking
+=================================
+
+To assist with verification checking, _yosys4gal_ includes Verilog models of
+the supported GAL16V8 and GAL22V10 chips. These Verilog read in the
+tool-generated fuse map and the behavior should match that of the original
+Verilog. The provided script performs this check using yosys' SAT solver:
+```
+./prove_equiv.tcl -- <JEDEC FILE> <PCF CONSTRAINTS> <VERILOG FILES...>
+```
+
+Limitations
+-----------
+The models only support the functionality of the GAL chips which is supported
+in _yosys4gal_. I.e. the GAL16V8 model only supports registered mode and the
+GAL22V10 model doesn't support asynchronous set/reset. Also note that a failure
+to prove equivalence does not imply inequivalence. In particular, yosys can
+struggle to synthesize the GAL22V10 model correctly. The false positive rate,
+however, should be zero.
+
+Dependencies
+------------
+- `yosys` 0.38 or higher
+- `jedutil` from MAME utilities
+- `xxd` from Vim