write_smt2 - write design to SMT-LIBv2 file
write_smt2 [options] [filename]
Write a SMT-LIBv2  description of the current design. For a module with name
'<mod>' this will declare the sort '<mod>_s' (state of the module) and the
functions operating on that state.
The '<mod>_s' sort represents a module state. Additional '<mod>_n' functions
are provided that can be used to access the values of the signals in the module.
By default only ports, registers, and wires with the 'keep' attribute set are
made available via such functions. With the -nobv option, multi-bit wires are
exported as separate functions of type Bool for the individual bits. Without
-nobv multi-bit wires are exported as single functions of type BitVec.
The '<mod>_t' function evaluates to 'true' when the given pair of states
describes a valid state transition.
The '<mod>_a' function evaluates to 'true' when the given state satisfies
the asserts in the module.
The '<mod>_u' function evaluates to 'true' when the given state satisfies
the assumptions in the module.
The '<mod>_i' function evaluates to 'true' when the given state conforms
to the initial state. Furthermore the '<mod>_is' function should be asserted
to be true for initial states in addition to '<mod>_i', and should be
asserted to be false for non-initial states.
For hierarchical designs, the '<mod>_h' function must be asserted for each
state to establish the design hierarchy. The '<mod>_h <cellname>' function
evaluates to the state corresponding to the given cell within <mod>.
this will print the recursive walk used to export the modules.
disable support for BitVec (FixedSizeBitVectors theory). without this
option multi-bit wires are represented using the BitVec sort and
support for coarse grain cells (incl. arithmetic) is enabled.
disable support for memories (via ArraysEx theory). this option is
implied by -nobv. only $mem cells without merged registers in
read ports are supported. call "memory" with -nordff to make sure
that no registers are merged into $mem read ports. '<mod>_m' functions
will be generated for accessing the arrays that are used to represent
create '<mod>_n' functions for all public wires. by default only ports,
registers, and wires with the 'keep' attribute are exported.
use the given template file. the line containing only the token '%%'
is replaced with the regular output of this command.
 For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David
R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf
Consider the following module (test.v). We want to prove that the output can
never transition from a non-zero value to a zero value.
module test(input clk, output reg [3:0] y);
always @(posedge clk)
y <= (y << 1) | ^y;
For this proof we create the following template (test.tpl).
; we need QF_UFBV for this poof
; insert the auto-generated code here
; declare two state variables s1 and s2
(declare-fun s1 () test_s)
(declare-fun s2 () test_s)
; state s2 is the successor of state s1
(assert (test_t s1 s2))
; we are looking for a model with y non-zero in s1
(assert (distinct (|test_n y| s1) #b0000))
; we are looking for a model with y zero in s2
(assert (= (|test_n y| s2) #b0000))
; is there such a model?
The following yosys script will create a 'test.smt2' file for our proof:
hierarchy -check; proc; opt; check -assert
write_smt2 -bv -tpl test.tpl test.smt2
Running 'cvc4 test.smt2' will print 'unsat' because y can never transition
from non-zero to zero in the test design.