YosysHQ / sby

SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
Other
388 stars 73 forks source link

Feature request: One VCD file on error #60

Open ZipCPU opened 5 years ago

ZipCPU commented 5 years ago

Current behavior

When BMC fails, a VCD waveform is left in *task/engines?/trace.vcd

When Induction fails, a VCD waveform is left in *task/engines?/trace_induct.vcd

When viewing a VCD trace for a BMC failure, and the design passes BMC, GTKWave struggles with a none-existent trace. Likewise when viewing a VCD trace for an induction failure and you get a BMC failure, GTKWave struggles again with the absence of the open VCD file.

Suggested feature

Upon completion of any induction pass with an UNKNOWN result, copy (not move) the induction trace to where the BMC trace would be. That way you only ever need to keep one GTKWave window open.

dlmiles commented 1 year ago

I run into this code/build/test loop headache too and problems amplify on Windows (compared to Linux) with file/directory locking of open file/dir handles.

I would agree with the concept of a unified output directory collecting and copying failures together (not with the moving of files from their original source), maybe with a new option --collect-failure-output=failures to create a failures/* tree. Also agree if useful concatenation of VCD files into one large file (with added signals to indicate original file name, test kind and a strobe signal at point of the failure claim) , so its possible to seek next rising edge in tooling. Also a summary of the failure claim, in a format an IDE/tooling can parse to obtains error message and accompanying VCD proof with time index, then popup or inter-communicate with gtkwave to open and seek. This aspect would be for tooling to implemented IDE/VSCODE/gtkwave.

But the 'gtkwave struggles' would be better improved at the gtkwave end IMHO.