Specifying and Verifying Systems with Multiple Clocks

Multiple clock domains are a challenge for hardware specification and verification. We present a method for specifying the relations between multiple clocks, and for modeling the possible behaviors. We can then verify a hardware design assuming that the clocks meet these constraints. We implement our ideas in the context of SAT based Bounded Model Checking (BMC), using ANSI–C programs to specify the functional behavior of the design.

• Type: Conference
• Year: 2003
• Where: ICCD
• Authors: Edmund M. Clarke, Daniel Kroening, Karen Yorav
• Keywords: Hardware, Hardware Design, ICCD 2003, Multiple Clock Domains, Multiple Clocks