sby doesn't report full path of generated cover trace file names

[tudortimi]

In cover mode, sby prints messages from the engines when a cover trace is available: Writing trace to VCD file: engine_0/trace0.vcd. It's not possible to simply take this name and send it to GTKWave, as the work directory name is missing. User have to add the workdir as a prefix themselves.

Contrast this to prove mode, where the last message in case of a fail is summary: counterexample trace: <workdir>/engine_0/trace.vcd, which contains the full path to the VCD file and can be directly opened in GTKWave.

[ZipCPU]

@tudortimi ,

The primary issue is the difference between the summary trace results and the results of the individual passes from each solve. When run in proof mode, a failure only results in a single VCD file and so it is listed in the summary with it's full path. If you look closer, you'll also see that same VCD file with it's partial path listed above as well, this is the result/output of the solver. When SymbiYosys is run in cover mode, there is no guarantee of a single cover() output--instead there might be many. As an example, one design I'm working with has nearly 300 cover checks. Not having an easy way of generating a cover() summary listing all the successes, cover() doesn't list VCD files upon success.

Dan

[tudortimi]

I know, but it would still be possible to list all of the generated cover traces at the end. I agree, though, that with a lot of cover properties the list could become pretty big. If this information were dumped into a log file (#79 😉 ), then it would be easier to sift through it.