mirror of
https://github.com/YosysHQ/yosys
synced 2025-10-31 03:32:29 +00:00
0fda8308bc
Modifies smt2 backend to recognize `$anyconst` etc. assigned to a wire with the `maximize` or `minimize` attribute and emit `; yosys-smt2-maximize` or `; yosys-smt2-minimize` directives as appropriate. Modifies `backends/smt2/smtbmc.py` and `smtio.py` to recognize those directives and emit a `(maximize ...)` or `(minimize ...)` command at the end of `smt_forall_assert()`, as described in the paper "νZ - An Optimizing SMT Solver" by Nikolaj Bjørner et al. Adds an example `examples/smtbmc/demo9.v` to show how it can be used.
13 lines
256 B
Verilog
13 lines
256 B
Verilog
module demo9;
|
|
(* maximize *) wire[7:0] h = $anyconst;
|
|
wire [7:0] i = $allconst;
|
|
|
|
wire [7:0] t0 = ((i << 8'b00000010) + 8'b00000011);
|
|
wire trigger = (t0 > h) && (h < 8'b00000100);
|
|
|
|
always @* begin
|
|
assume(trigger == 1'b1);
|
|
cover(1);
|
|
end
|
|
endmodule
|
|
|