IC3 / PDR
Beginner
A modern proof method that builds up small facts about a design, one at a time, until they add up to a full proof.
Novice
IC3, also called property directed reachability (PDR), is a formal proof method. Instead of unrolling many cycles, it learns small facts that rule out states leading to a failure, until those facts add up to a full proof.
Expert
Keeps a series of frames, each a formula covering at least every state reachable in steps. It blocks each state that could lead to a violation with a small learned clause, and stops when two neighboring frames become identical. Runs many small, incremental SAT queries.