Merge pull request #3398 from jix/mention_smtlib2_module

Mention smtlib2_module in README.md and CHANGELOG

2 files changed, 16 insertions, 3 deletions

diff --git a/CHANGELOG b/CHANGELOG
index 16c746957..97572c35d 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -4,9 +4,6 @@ List of major changes and improvements between releases
 
 Yosys 0.18 .. Yosys 0.18-dev
 --------------------------
- * Various
-    - Added support for $pos cell in btor backend
-
  * New commands and options
     - Added option "-rom-only" to "memory_libmap" pass
     - Added option "-smtcheck" to "hierarchy" pass
@@ -14,6 +11,10 @@ Yosys 0.18 .. Yosys 0.18-dev
     - Added option "-suffix" to "rename" pass
     - Added "gatemate_foldinv" pass
 
+ * Formal Verification
+    - Added support for $pos cell in btor backend
+    - Added the "smtlib2_module" and "smtlib2_comb_expr" attributes
+
  * GateMate support
     - Added LUT tree mapping
 
diff --git a/README.md b/README.md
index 0232a5ed0..f916b38ad 100644
--- a/README.md
+++ b/README.md
@@ -505,6 +505,18 @@ Verilog Attributes and non-standard features
   module. Modules with such cells will be reprocessed during the ``hierarchy``
   pass once the referenced module definition(s) become available.
 
+- The ``smtlib2_module`` attribute can be set on a blackbox module to specify a
+  formal model directly using SMT-LIB 2. For such a module, the
+  ``smtlib2_comb_expr`` attribute can be used on output ports to define their
+  value using an SMT-LIB 2 expression. For example:
+
+      (* blackbox *)
+      (* smtlib2_module *)
+      module submod(a, b);
+        input [7:0] a;
+        (* smtlib2_comb_expr = "(bvnot a)" *)
+        output [7:0] b;
+      endmodule
 
 Non-standard or SystemVerilog features for formal verification
 ==============================================================