Assertion Based Verification of Multiple-Clock GALS Systems
Shaked Flur, Ran Ginosar · 2008
Standard EDA ABV tools fall short of verifying multiple clock domain systems on chip (MCD SoC), asynchronous systems and Globally Asynchronous Locally Synchronous (GALS) systems. This paper describes a method for verifying asynchronous and multi-clock behavior in such systems using PSL and standard ABV tools. We convert STG (signal transition graphs), a common form for specifying asynchronous behavior, into PSL statements, employ standard ABV tools, and prove complete verification. The proposed ASE (automatic sequence extraction) algorithm was applied to a MCD SoC model that employed a network-on-chip (NoC) for asynchronous inter-modular communications.