Add example verification results

doc/manual.md

@@ -13,7 +13,7 @@ Options:
   -o --output=<dir>         Write output files to directory.
   -s --spec=<spec.sg>       Generate spec model for verification.
   -t --template=<template>  Specify template [default: standard].
-  -l --lib=<file>           Load additional library file(s).
+  -l --lib=<dir>            Load additional library file(s).
 ```
 
 where the input circuit `circuit.v` is a gate-level Verilog netlist.
@@ -30,12 +30,7 @@ circuits. Second, they contain definitions for cells inside the generated sync
 model (and must therefore be imported by sync simulators/verifiers that use
 the generated circuit).
 
-The tool can load additional library files using `--lib` which can either
-accept individual files or glob patterns. In the latter case, make sure you
-enclose the glob pattern in single quoates to prevent the shell from expanding
-it.
-
-For example, use `--lib 'myproject/libraries/*'` and **not** `--lib myproject/libraries/*`
+The tool can load additional (user) library files using `--lib`.
 
 #### Templates
 
@@ -53,5 +48,9 @@ specification.
 To generate a specification model, run the tool as follows:
 
 ```
-./generator.py --spec myspec.sg circuit.v
+./generator.py --spec myspec.sg --output generated circuit.v
 ```
+
+The tool generates both circuit and spec models when `--spec` is used. It is
+therefore best to accompany this with `--output` to write generated files to a
+given directory instead of printing them to the terminal.

doc/tutorial.md

@@ -192,3 +192,28 @@ verification properties).
 Both files can now be passed to a sync formal verification tool to verify spec
 compliance. If the verification tool does not support loading `.lib` files,
 corresponding Verilog files are provided in the directory `gates`.
+
+As an example, we provide the output log produced by a commercial verification
+tool running on `circuit.v` and `spec.v`:
+
+```
+Verification mode:
+  circuit1.u1.persistency_ro : Pass - Trigger: Pass (6)
+  circuit1.u1.compliance_ro_rise : Pass - Trigger: Pass (6)
+  circuit1.u1.persistency_ai : Pass - Trigger: Pass (16)
+  circuit1.u1.persistency__U2_QN : Pass - Trigger: Pass (10)
+  circuit1.u1.compliance_ai_fall : Pass - Trigger: Pass (22)
+  circuit1.u1.compliance_ai_rise : Pass - Trigger: Pass (16)
+  circuit1.u1.deadlock_free : Pass
+  circuit1.u1.compliance_ro_fall : Pass - Trigger: Pass (12)
+Assertion Summary:
+  Total                  :   8
+  Pass                   :   8
+  Not_Run                :   0
+```
+
+In the above:
+
+- Internal/output signals `ro`, `ai` and `_U2_QN` passed persistency checks
+- Output signals `ro` and `ai` passed compliance checks
+- The circuit passed deadlock checks

generator.py

@@ -23,7 +23,7 @@
   -o --output=<dir>         Write output files to directory.
   -s --spec=<spec.sg>       Generate spec model for verification.
   -t --template=<template>  Specify template [default: standard].
-  -l --lib=<file>           Load additional library file(s).
+  -l --lib=<dir>            Load additional library file(s).
 
 """
 
@@ -192,9 +192,11 @@ def main():
                                  args["--template"])
 
     if args['--lib']:
-        lib_paths = [built_in_libs, args['--lib']]
+        user_libs = os.path.join(args['--lib'], '*')
     else:
-        lib_paths = [built_in_libs]
+        user_libs = None
+
+    lib_paths = [built_in_libs] + ([user_libs] if user_libs else [])
 
     lib = load_lib(*lib_paths)