Search code examples
verilogyosys

Is it possible to use $display to print some values when proving with yosys-smtbmc?

In verilog $display() function is usefull in simulation to see the value of constants or macro like this example :

/* Display parameters in simulation */
initial
begin
    $display("CLK_PER_NS     : %d", CLK_PER_NS );
    $display("PULSE_PER_NS   : %d", PULSE_PER_NS);
    $display("MAX_COUNT      : %x", `MAX_COUNT);
    $display("MAX_COUNT_SIZE : %x", `MAX_COUNT_SIZE);
end

But when I launch yosys-smtbmc with cover, bmc or prove, nothing is displayed in console.

Is it possible to do it ?

My sby script (example is from my github project here):

[options]
#mode cover
mode bmc
#mode prove
depth 150

[engines]
smtbmc

[script]
read -formal per2bpm.v
prep -top per2bpm

[files]
../../hdl/per2bpm.v
Solution

  • No, this isn't supported at the moment. In general formal verification with Yosys gives you a similar feature set to synthesis (what it presents to the solver is essentially a circuit) with the addition of assert/assume/cover etc. Adding display would be possible using something that read the solver output, but would also be quite a substitantial piece of work to implement properly.