Tech Tip: Save Steps With Automatic Witness Checks

8 Sep 2010 • Less than one minute read

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:

define witness_check off
define witness_check trace
define witness_check trigger (default)
define witness_check auto <-- option described above

Example usage from the tools' command prompt:

Formalverifier> define witness_check auto

Happy verifying!

Team Verify