A method and apparatus for critical and false path verification takes all
the potential false paths and captures the conditions that would make them
true paths (or false paths) as a Boolean expression (net list), for the
combinational logic only. The net list does not have to be at the gate
level, but can be a simplified gate level representation because the
verification process is only concerned with the logical behavior, not the
actual structure. This allows the simulation to execute more quickly.
Since the conditions are only captured between register elements, it can
be formally proved whether or not the path can be exercised. If no
register value can activate the path, then the analysis is done.
Otherwise, a simulation is performed to determine whether the register
values required to active the condition actually occur. If the Boolean
condition can be satisfied, the simulation is performed on the sequential
logic to justify those values. If the satisfiability engine fails to
finish, then the simulation is run on the combinatinal logic, and an
attempt is made to justify the values sequentially as well.
