From 5343911263ea10dc9d0fd308297314b4b42989d2 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Mon, 4 Jul 2022 13:54:49 +0200
Subject: Mention smtlib2_module in README.md and CHANGELOG

---
 README.md | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'README.md')

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
 ==============================================================
-- 
cgit v1.2.3