YosysHQ / yosys

Yosys Open SYnthesis Suite
https://yosyshq.net/yosys/
ISC License
3.45k stars 883 forks source link

$divfloor not supported by write_smt2 #3330

Closed programmerjake closed 2 years ago

programmerjake commented 2 years ago

$divfloor isn't supported by write_smt2, apparently it was forgotten though $modfloor does work.

Steps to reproduce the issue

Compile commit 0b1a1a576 (git master when issue was created) Run the following yosys script:

read_verilog -icells -formal <<EOF
module uut;
    wire [7:0] a = $anyconst, b = $anyconst, y;

    \$divfloor #(
        .A_WIDTH(8),
        .B_WIDTH(8),
        .Y_WIDTH(8),
        .A_SIGNED(0),
        .B_SIGNED(0),
    ) divfloor (
        .A(a),
        .B(b),
        .Y(y)
    );

    always @* begin
        assume(b == 4);
        assert(a >> 2 == y);
    end
endmodule
EOF
prep
write_smt2 -wires

Expected behavior

generate smtlib2 code

Actual behavior

...
; SMT-LIBv2 description generated by Yosys 0.17+33 (git sha1 0b1a1a576, gcc 9.4.0-1ubuntu1~20.04.1 -fPIC -Os)
Creating SMT-LIBv2 representation of module uut.
ERROR: Unsupported cell type $divfloor for cell uut.divfloor.
Xiretza commented 2 years ago

I don't think SMT-LIB has an operator for that (bvsdiv is truncating division: https://smtlib.cs.uiowa.edu/logics-all.shtml), so it'd have to be implemented by hand - that's why I left it out in #1885.