Support for Multiple SMT-LIB expressions

Users
1

Hello,

I have a question about the smtlib2_module feature. The documentation said we can use (*smtlib2_comb_expr = *) to place smtlib expression on output port inside the blackboxed verilog module. I tried some experiments and used multiple (*smtlib2_comb_expr = *)inside the module, but it seems like the yosys output of read_verilog and write_smt2only includes the smt expression closest to the output port and other parts are missing. I am wondering if yosys supports multiple smtlib expressions to be placed in verilog module or we could only use a single one of it.

Thank you very much for your help.

Katz

2

You can use multiple smtlib2_comb_expr in a single module, but only one per output port, since each of it fully defines the value of the corresponding output port. You can think of smtlib2_comb_expr as an assignment, i.e. the following two modules produce smt2 output that behaves equivalently:

(* smtlib2_module *)
module smtlib_example(
    input [7:0] a,
    input [7:0] b,
    (* smtlib2_comb_expr = "(bvmul a b)" *)
    output [7:0] x,
    (* smtlib2_comb_expr = "(bvadd a b)" *)
    output [7:0] y
);
endmodule

module verilog_example(
    input [7:0] a,
    input [7:0] b,
    output [7:0] x,
    output [7:0] y
);

    assign x = a * b;
    assign y = a + b;
endmodule

Multiple smtlib2_comb_expr on the same port are not supported for two reasons:

  1. Verilog specifies that the same attribute is specified multiple times for the same element, only the last value is used:

    If the same attribute name is defined more than once for the same language element, the last attribute value shall be used, and a tool can issue a warning that a duplicate attribute specification has occurred.

  2. If we would emit multiple definitions for the same output port to the resulting smt2 output, this would correspond to an implicit constraint that both definitions produce the same value. Implicit constraints without a corresponding assume statement can lead to unexpected, confusing and hard to debug behavior during FV. There is an alternative approach that I’ll describe below which avoids this, and for that reason we decided against including an attribute that would emit such implicit constraints.

If you want to describe a single output not by giving an smtlib2 definition, but by using multiple smtlib2 constraints, the best way is to do that is to write an smtlib2_module that takes all signals as inputs and produces a single bit valid output that is high exactly for those signal values that fulfill your constraints. You can then combine that with a wrapper module where you use the SV assume statement to restrict FV to scenarios where the constraint holds.

For example, as you discovered, this doesn’t work:

(* smtlib2_module *)
module smtlib_nonworking(
    input [7:0] a,
    input [7:0] b,
    (* smtlib2_comb_expr = "(bvmul a b)" *)
    (* smtlib2_comb_expr = "(bvadd a b)" *)
    output [7:0] x,
);
endmodule

If you only want to consider those cases where x is equal to both expressions, you can use this instead:

(* smtlib2_module *)
module smtlib_constraint(
    input [7:0] a,
    input [7:0] b,
    input [7:0] x,
    // We can combine multiple constraints using `and`
    (* smtlib2_comb_expr = """
        (and
            (= x (bvmul a b))
            (= x (bvadd a b))
        )
    """ *)
    output valid
);
endmodule

module smtlib_wrapper(
    input [7:0] a,
    input [7:0] b,
    output [7:0] x
);

    wire valid;

    // We create a symbolic output value
    assign x = $anyseq;

    // Check whether the output value fulfills our smtlib2 constraint
    smtlib_constraint constraint(.a(a), .b(b), .x(x), .valid(valid));

    // And add an assumption so FV will only consider output values that do
    // fulfill the constraint
    always @* enforce_smtlib_constraint: assume (valid);
endmodule

Note that I only checked the syntax of the examples and haven’t run any FV tasks, so let me know if this doesn’t work as intended.