write_smt2 - write design to SMT-LIBv2 file

    write_smt2 [options] [filename]

Write a SMT-LIBv2 [1] 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>.

    -verbose
        this will print the recursive walk used to export the modules.

    -nobv
        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.

    -nomem
        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
        memories.

    -wires
        create '<mod>_n' functions for all public wires. by default only ports,
        registers, and wires with the 'keep' attribute are exported.

    -tpl <template_file>
        use the given template file. the line containing only the token '%%'
        is replaced with the regular output of this command.

[1] 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

---------------------------------------------------------------------------

Example:

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;
        endmodule

For this proof we create the following template (test.tpl).

        ; we need QF_UFBV for this poof
        (set-logic QF_UFBV)

        ; 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?
        (check-sat)

The following yosys script will create a 'test.smt2' file for our proof:

        read_verilog test.v
        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.