vcd file includes blank traces

[mattvenn]

I recall previous behaviour was that untouched signals were dropped from the vcd. Now untouched signals are present in the vcd but have no value - which IMO is more confusing.

`default_nettype        none
module counter (input wire clock);

    reg [2:0] f_counter1 = 0;
    reg [2:0] f_counter2 = 0;

        always @(posedge clock) begin
        f_counter1 <= f_counter1 + 1;
        f_counter2 <= f_counter2 + 1;
        assert(f_counter2 != 3);
    end

endmodule

[options]
mode prove
depth 5

[engines]
smtbmc

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

[files]
counter.v

counter.zip

[ZipCPU]

Which signal in the trace above are you referencing? f_counter1? or some other signal?

[mattvenn]

Yes

…

On Fri, 12 Jun 2020, 22:53 Dan Gisselquist, ***@***.***> wrote: Which signal in the trace above are you referencing? f_counter1? or some other signal? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#91 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAE223DDCRBX2BJTTW2IE33RWKITFANCNFSM4N4HAERA> .

[ZipCPU]

I'm confused then. f_counter1 shows in your trace. It shows as the low line rather than both simply because this is considered an "upgrade" of gtkwave. You can see this if you examine f_counter2 and see what happens when it switches to all zeros.

[mattvenn]

f_counter1 shows in the trace but there is no data. It is incrementing every time like f_counter2.

Previously I've noticed that signals that are not used in the formal process are not present in the vcd (unless using keep).

The above is an example of an unused signal trace being kept but containing no data.

[ZipCPU]

Ok, I see it now, it's not that f_counter1 isn't present, it's that it has the wrong value.

Yeah, that looks like a bug.

Dan

[nakengelhardt]

It's the call to opt_clean in preparing the model that does this; there were a bunch of changes to opt_clean recently but before I track down which one, I'd rather understand first if it's doing what it is supposed to, and what the preferred outcome would be.

If you just want f_counter1 to disappear again, changing it to opt_clean -purge would do that. But I think the better solution would be to treat any public net like an output when creating the model, so that both it and its behavior is kept. @clairexen is there an easy way to do that?

[nakengelhardt]

Here's an ugly hotfix for if you want proper traces:

[script]
read -formal counter.v
hierarchy -top counter
proc
setattr -set keep 1 w:\\*
prep

This sets the (* keep *) attribute on all public wires, which stops opt_clean from removing the things driving them.