To prove that circuit is a NAND gate, exhaustive simulation requires 2n vectors
Hardware Verification - Application of formal techniques to chip designs Jacob Abraham (July 7, 2001)