Bounded model checking (BMC)
Beginner
Checking every possible input for the first few steps after the chip starts up, to see if anything goes wrong.
Novice
A formal check of the first clock cycles after start-up: the tool asks whether any input sequence of that length can break a rule. It finds bugs quickly but says nothing about cycle and beyond.
Expert
Copies the design’s logic times, one copy per cycle, into one large formula and hands it to a SAT solver. Returns the shortest counterexample and needs no variable ordering. A pass is a bounded result only.