From 5343911263ea10dc9d0fd308297314b4b42989d2 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 4 Jul 2022 13:54:49 +0200 Subject: Mention smtlib2_module in README.md and CHANGELOG --- CHANGELOG | 7 ++++--- README.md | 12 ++++++++++++ 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 ============================================================== -- cgit v1.2.3