search

dz333 / secverilog

4 stars 0 forks source link

Generating Z3 constraints re-uses dump::(ostream&out) and incorrectly formats some Predicates #1

Closed dz333 closed 2 years ago

dz333 commented 2 years ago

SecVerilog uses the built-in iVerilog dump(ostream&out) functions to generate z3 constraints.

However this can lead to some bugs, e.g.:

if (domX <= domY) {
   y = x;
}

With a lattice where Domain domX is the label of x and Domain domY is the label of y, generates the constraint:

(assert (and (<= (domX) (domY))  (not(leq (Domain domX)  (Domain domY)))))

However, this causes typechecking to fail due to invalid z3 syntax. The parentheses around domX and domY are unnecessary for this (although should be used when the dump is normally used by the iverilog compiler).

Therefore, we should use a unique "dump" function for when printing z3 constraints, or add an optional to the dump function that says which output syntax to use.