Converting formal verification testbench drivers with nondeterministic inputs to simulation monitors

A system comprising:

• a memory having computer readable instructions;
• and
• one or more processors for executing the computer readable instructions, the computer readable instructions controlling the one or more processors to perform operations comprising:
• configuring a sequential circuit simulation monitor to have a design under test (DUT) input interface configured to be coupled to a DUT in a simulation environment;
• selecting a value for random inputs associated with an original formal verification driver to drive a next stage logic of the sequential circuit simulation monitor, a state of the next stage logic being used by the sequential circuit simulation monitor to generate sequential inputs that correspond to the nondeterministic inputs permitted by the original formal verification driver;
• and
• using the sequential circuit simulation monitor to identify an input sequence from the simulation environment not permitted by the original formal verification driver based on the sequential inputs.

A computer program product comprising a computer readable storage medium having program instructions embodied therewith, the program instructions executable by a processor to cause the processor to perform operations comprising:

• configuring a sequential circuit simulation monitor to have a design under test (DUT) input interface configured to be coupled to a DUT in a simulation environment;
• selecting a value for random inputs associated with an original formal verification driver to drive a next stage logic of the sequential circuit simulation monitor, a state of the next stage logic being used by the sequential circuit simulation monitor to generate sequential inputs that correspond to the nondeterministic inputs permitted by the original formal verification driver;
• and
• using the sequential circuit simulation monitor to identify an input sequence from the simulation environment not permitted by the original formal verification driver based on the sequential inputs.