Applying Model Checking in the Verification of a Clock Masking Unit
José M. N. Leitão, Ricardo Chaves, Marcelino B. Santos · 2019
As the number of microelectronic circuits populating the world is increasing, so is the number of critical applications relying on their well-function. Nevertheless, ensuring that a circuit complies with the specifications is still a challenge for design and verification engineers. While simulation-based verification stands out as the most widely adopted strategy, it can only offer limited compliance guarantees since it lacks exhaustiveness. Alternatively, formal verification methodologies and, in particular, model checking, provide the means to prove functional correctness. In this work, we walk trough the verification of a clock masking unit using the NuSMV model-checking tool. Finally, we discuss the applicability of this methodology to larger and more complex designs.