add smtlib2_comb_expr

[programmerjake]

adds a smtlib2_comb_expr attribute that allows you to pass a smtlib2 expression through to the output of write_smtlib2. This is useful to allow using smtlib2 types other than bool/bitvector, such as real numbers or floating-point.

Corresponding PR for nmigen:
https://gitlab.com/nmigen/nmigen/-/merge_requests/7

https://bugs.libre-soc.org/show_bug.cgi?id=835

[jix]

As I mentioned on IRC before, while I do think this feature is quite useful, I'm not convinced that this is the right approach to implement it in yosys. Having had a closer look now, I still think that adding a new builtin cell type is not required here. I've opened a draft PR (#3342) that shows the approach I would use instead.

[programmerjake]

As I mentioned on IRC before, while I do think this feature is quite useful, I'm not convinced that this is the right approach to implement it in yosys. Having had a closer look now, I still think that adding a new builtin cell type is not required here. I've opened a draft PR (#3342) that shows the approach I would use instead.

hmm, that could work, though I'd have to refactor the 8kloc of code I already wrote:
https://gitlab.com/nmigen/nmigen/-/merge_requests/7

also, I'm not sure having the model be in the form of an implicit assumption is the best idea...what happens if we write something that's accidentally never true?

having it instead just be a cell that computes a bool which we explicitly assert/assume using yosys's existing techniques allows smtbmc to give us the exact conditions under which the assumption fails.
if we went with the implicit assertion idea, then smtbmc would need a bunch of extension to add the new assumption type, which imho would be waay more complex than taking my approach.

[jix]

also, I'm not sure having the model be in the form of an implicit assumption is the best idea...what happens if we write something that's accidentally never true?

having it instead just be a cell that computes a bool which we explicitly assert/assume using yosys's existing techniques allows smtbmc to give us the exact conditions under which the assumption fails.

In that case the presat check would still fail, but this does leave the case where you accidentally exclude only some possible inputs. I agree that it's much better to use explicit assumptions to place restrictions on the considered inputs. Note that in the example I've only used smt2 to assert the otherwise unconstrained outputs to be equal to an expression of the inputs, which does not have this problem and is what you end up on the smt2 output side anyway. Moving the part that constrains the outputs from the user written smt2 to the smt2 generated by write_smt2 for such a blackbox (so you cannot accidentally assume anything not following this pattern) would be possible and should be done.

This is completely separate, however, from the issue I have with adding a new builtin cell instead of using blackbox modules and the points regarding this, that I brought up in #3342.

if we went with the implicit assertion idea, then smtbmc would need a bunch of extension to add the new assumption type, which imho would be waay more complex than taking my approach.

I don't understand what you're saying here, as my PR is a working prototype that does not require any changes to smtbmc. If you mean allowing explicit named assumptions that restrict the considered inputs (which is not how I intended it to be used) it could be handled using the existing documented interface of representing assumptions in smt2 (in help write_smt2) and also not require any changes to smtbmc. (In any case I do think having actual assumptions and assertions be external to any user smt2, as you suggest and as I did in my example, is sufficient and preferable, as it, e.g., also allows manipulating them using other yosys passes such as chformal.) Beyond that I'm not sure what you could mean here, can you elaborate?

[programmerjake]

This is completely separate, however, from the issue I have with adding a new builtin cell instead of using blackbox modules and the points regarding this, that I brought up in #3342.

Hmm, I think the blackbox idea might be better, though I think the attribute value should just be the expression that gets assigned to the output. this would practically require that the module only has one output, unless we want to parse the attribute string.

something like:

(* smtlib2_output_expr = "((_ int2bv 10)\n(to_int (* 3.1415926535 (bv2int a))))" *)
(* blackbox *)
module mul_by_pi(out, a);
    input [9:0] a;
    output [9:0] out;
endmodule

if we went with the implicit assertion idea, then smtbmc would need a bunch of extension to add the new assumption type, which imho would be waay more complex than taking my approach.

I don't understand what you're saying here, as my PR is a working prototype that does not require any changes to smtbmc. If you mean allowing explicit named assumptions that restrict the considered inputs (which is not how I intended it to be used) it could be handled using the existing documented interface of representing assumptions in smt2 (in help write_smt2) and also not require any changes to smtbmc. (In any case I do think having actual assumptions and assertions be external to any user smt2, as you suggest and as I did in my example, is sufficient and preferable, as it, e.g., also allows manipulating them using other yosys passes such as chformal.) Beyond that I'm not sure what you could mean here, can you elaborate?

I meant that if you have complex assertions embedded in the hierarchy instead of in explicit smtbmc assertions, then when they fail because the user messed up, then the assertions are hard to debug because smtbmc doesn't expect the hierarchy assumptions to fail, so doesn't have code to help with debugging that, unlike normal assumptions.

[jix]

Hmm, I think the blackbox idea might be better, though I think the attribute value should just be the expression that gets assigned to the output. this would practically require that the module only has one output, unless we want to parse the attribute string.

Yeah I do want the user to specify just an expression for each output. Indeed that would need either some limited parsing or multiple attributes or something similar. I haven't found the time to explore the design space here, that's why I went with the "let the user specify the raw constraint" approach for my draft PR, so I could show the differences I wanted to focus on to quickly have something more concrete to discuss those.

I would want something here that can a) allow defining internal variables using (let ...) that can be reused for multiple outputs and b) can be extended to handle smt2 internal state (specify the smt2 type, give an expression for the initial value, make the current value available like an input and allow specifying the next state's value like an output). That doesn't have to be part of a first merged version, I'm also ok with limiting this to just a single output, but I want to make sure that the design we end up using can accommodate all that without breaking existing code each time we add such functionality.

I meant that if you have complex assertions embedded in the hierarchy

Ah, that wasn't what I intended.

[programmerjake]

I had an idea: why don't we put the smtlib2 expression attribute on the output wires rather than on the module?

I would want something here that can a) allow defining internal variables using (let ...) that can be reused for multiple outputs

imho that should be left for a future extension. it could be something like defining wires with a special attribute on those wires with the smtlib2 expression. we'd need to correctly handle dependencies between expressions, preferably without needing to parse them (maybe declaration order? idk if yosys preserves that all that well).

and b) can be extended to handle smt2 internal state (specify the smt2 type, give an expression for the initial value, make the current value available like an input and allow specifying the next state's value like an output). That doesn't have to be part of a first merged version, I'm also ok with limiting this to just a single output, but I want to make sure that the design we end up using can accommodate all that without breaking existing code each time we add such functionality.

imho we just add the new functionality by using different attribute names when we need something other than just plain combinatorial assignment. backward compatibility should be relatively easy that way.

[programmerjake]

we'd need to correctly handle dependencies between expressions, preferably without needing to parse them (maybe declaration order? idk if yosys preserves that all that well).

the PR I'm working on for nmigen constructs a dependency tree and groups expressions into nested (let ...) expressions based on the max depth from the leaves for each expression.

https://gitlab.com/nmigen/nmigen/-/blob/b5aa5009cf555a40ed9cf90fa61dd4f7e2e376ad/nmigen/hdl/smtlib2.py#L342

Example output:
https://gitlab.com/nmigen/nmigen/-/blob/825abd75d54d66cfa096e3684d58b1de702f5b16/tests/test_hdl_smtlib2.py#L2677

(let (
(var2 ((_ extract 1 0) A))) 
(let (
(var8 ((_ extract 0 0) var2)) 
(var14 ((_ extract 1 1) var2))) 
(let (
(var9 (= #b1 var8)) 
(var15 (= #b1 var14))) 
(let (
(var12 (ite var9 1 0)) 
(var17 (ite var15 2 0))) 
(let (
(var18 (+ var12 var17))) 
var18)))))

[jix]

why don't we put the smtlib2 expression attribute on the output wires rather than on the module?

I like that, it's simple and it's also clear that even should we extend the overall feature, we would not want to put anything besides the output defining expression in such an attribute, so no risk of wanting backwards incompatible changes later on :)

imho that should be left for a future extension.

Yeah, my "That doesn't have to be part of a first merged version" was referring to the whole paragraph.

imho we just add the new functionality by using different attribute names when we need something other than just plain combinatorial assignment. backward compatibility should be relatively easy that way.

In general, you can easily end up with some_attribute and some_attribute_v2 that way, where the v2 would make some_attribute completely redundant but it still cannot be removed, or similar things where the old syntax/behavior needs to be special cased. While sometimes necessary, you can't plan ahead for everything after all, I try to at least consider future extensions I already have in mind.

For this, though, I have no remaining concerns with your solution of using attributes on the outputs.

[programmerjake]

I switched the implementation to use attributes on the outputs and an attribute on the module.

example:

yosys/tests/various/smtlib2_module.v

Lines 1 to 10 in cd57c5a

	(* smtlib2_module *)
	module smtlib2(a, b, add, sub, eq);
	input [7:0] a, b;
	(* smtlib2_comb_expr = "(bvadd a b)" *)
	output [7:0] add;
	(* smtlib2_comb_expr = "(bvadd a (bvneg b))" *)
	output [7:0] sub;
	(* smtlib2_comb_expr = "(= a b)" *)
	output eq;
	endmodule

I also added a test that compares the generated smt2 to the expected output, avoiding the need to run a smtlib2 solver (which iirc yosys doesn't want a dependency on)

[programmerjake]

I have no idea why it's broken on macos, the build log doesn't contain any useful information (that would be in the .log file that yosys's testing framework hides), and I don't have a macos computer to test on. Help would be appreciated.

[nakengelhardt]

The error is in sed:

sed -i 's/; SMT-LIBv2 description generated by Yosys .*/; SMT-LIBv2 description generated by Yosys $VERSION/'smtlib2_module.smt2
sed: 1: "smtlib2_module.smt2": bad flag in substitute command: 't'

(I've had trouble with sed on macOS in the past as well, it's different from gnu sed.)

[programmerjake]

The error is in sed:

Ah, thanks! Turns out macos's sed has issues with -i, so I changed it to output to another file rather than modify it in-place. Hopefully this will fix it.

[programmerjake]

Thanks! if you're interested, Libre-SOC can figure out how to pay you eur 500 for your work...also, if you're interested in helping out more there is currently around eur 5-6000 available.