Yosys Formal : VCD Trace Dump

Users
1

Hi,

We are currently on an evaluation license of the Tabby CAD suite for formal. The VCD for a failing trace contains only a small set of signals making it harder to debug. Is there an option to dump specific signals/modules via the sby config file ?

2

SBY traces include everything in the design. If you are only seeing a small number of signals then most likely the rest of the design has been optimised away.

3

Thanks @KrystalDelusion . I’ve another issue related to reset assertion.

I see a counter trace vcd generated for a failing property. Upon vcd inspection, reset never appears to be asserted leading the tool to start in a random state.

Here’s the code :

logic i_rst;
logic [2:0] rst_count = 0;

always @(posedge clk) begin
if (rst_count < 4) begin
i_rst <=1;
rst_count <= rst_count + 1;
end
else
i_rst <=0;
end
initial assume(rst_count == 0);
initial assume(i_rst == 1);

I’m still new to formal , please correct me if I’m making novice mistakes :slight_smile:

4

The reset assumption there should be fine, but if you are running prove mode and the failure is during induction these are not guaranteed to start at reset and you may require a higher depth.