Automatic formal verification of Clock Domain Crossing signals

TLDR

This is the first paper discussing fully automatic, on‑the‑fly formal verification of CDC signals. The paper presents an approach that uses formal methods to verify CDC issues in a fully automatic way. The authors discuss CDC schemes and their formal checks, synthesize them into assertion logic, and propose a fully automatic, on‑the‑fly formal CDC approach. Experiment results show that the automatic formal CDC takes much less time than conventional post‑CDC formal CDC while still proving a significant number of CDC checks.

Abstract

In this paper, we present an approach that uses formal methods to verify clock domain crossing (CDC) issues in a fully automatic way. First, we discuss various CDC schemes and the corresponding checks that need to be formally verified. Then we demonstrate how to synthesize them into assertion logic. After that a fully automatic, on-the-fly formal CDC approach is proposed. To the best of our knowledge, this is the first paper discussing fully automatic, on-the-fly formal verification of CDC signals. Experiment results show that our automatic formal CDC, when compared with the conventional post-CDC formal CDC, takes much less time, but still prove significant number of CDC checks.