Counter Examples from Questa Formal

SystemVerilog
, , , , ,
1

Hi,

I want to prove some properties using OVL_SVA and Questa formal. Does anyone know how I can get counter examples (through the command line and not the GUI) in cases where the proof fails (fires)? Right now Im using “formal generate testbenches” command, but that does not directly give me the counter examples.

Thanks!

2

In reply to armit:

Assuming you can get a waveform/FSDB for a failure, it should be possible. Best is to ask Mentor support.

Regards
Srini