posted on 2007-11-01, 00:00authored byRandal Bryant
Abstract: "A logic simulator can prove the correctness of a digital circuit if it can be shown that only circuits fulfilling the system specification will produce a particular response to a sequence of simulation commands. This paper presents the theoretical foundations of several related approaches to formal circuit verification based on logic simulation. These approaches exploit the three-valued modeling capability found in most logic simulators, where the third value X indicates a signal with unknown digital value."