Using Model Checking in Digital Circuit Verification
Qiang Song · Science Technology and Engineering · 2008
Formal approaches provide a new measure to the verification of circuit functions as a supplement to the conventional simulation approaches. The theoretical basis and implementation of model checking are represented which is under the category of formal verification. The computational tree logic CTL, the fix point algorithm of CTL, binary decision diagram BDD, and symbolic model checking are introduced. The model checking with SMV on a memory management unit (MMU) of a CISC processor is applied, which is proved the applicability of model checking in module level verification.