This is just a quick reminder that the "witness_check" define command has an option called "auto". When set to "auto" Incisive Formal and Enterprise Verifier ("IFV" & "IEV") will run the trace as usual, but if the trace status is "Fail" or "Explored" it will initiate the running of the trigger. This setting may result in a little longer runtimes, but it eliminates the need to manually turn on triggers separately after running traces.
Witness_check setting summary:
Example usage from the tools' command prompt:
Formalverifier> define witness_check auto
Follow us on Twitter: http://twitter.com/teamverify, @teamverify