diff options
author | Jannis Harder <me@jix.one> | 2022-07-04 13:54:49 +0200 |
---|---|---|
committer | Jannis Harder <me@jix.one> | 2022-07-04 13:54:49 +0200 |
commit | 5343911263ea10dc9d0fd308297314b4b42989d2 (patch) | |
tree | b655f824defb74bc62ab40ca57c5296eb06115b5 /README.md | |
parent | 59b96bb1f82b6cf83e004488267e5576dbcfad4b (diff) | |
download | yosys-5343911263ea10dc9d0fd308297314b4b42989d2.tar.gz yosys-5343911263ea10dc9d0fd308297314b4b42989d2.tar.bz2 yosys-5343911263ea10dc9d0fd308297314b4b42989d2.zip |
Mention smtlib2_module in README.md and CHANGELOG
Diffstat (limited to 'README.md')
-rw-r--r-- | README.md | 12 |
1 files changed, 12 insertions, 0 deletions
@@ -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 ============================================================== |