pono only checks first property in a design

[nakengelhardt]

When using the pono solver, it only checks one property. It will mention this at the beginning, e.g. Solving property: both_ex.v:19.25-20.30.

We don't have a testcase that exposes this problem yet.

[nakengelhardt]

Testcase:

[tasks]
btormc
pono

[options]
mode bmc
depth 5
expect fail

[engines]
btormc: btor btormc
pono: btor pono

[script]
read_verilog -sv multi_assert.v
prep -top test

[file multi_assert.v]
module test();
always @* begin
assert (1);
assert (0);
end
endmodule

[tmeissner]

I also have stumbled over this behavior some time ago, but was not sure, if that is by intention. pono has an option to set the index of the property to check, but I didn't found any option to solve all properties.

[nakengelhardt]

Yes, looking at the options code for pono the intention seems to be not to check more than one property at a time. Yosys' write_btor does have an option for creating a single bad that is an and of all the assertions. It'll do as a workaround until I can figure out a better solution, but it removes the ability to find out which property failed so that's not great either.