Proceedings 21st International Conference on Computer Design (2003)
San Jose, California
Oct. 13, 2003 to Oct. 15, 2003
Edmund M. Clarke , Carnegie Mellon University
Daniel Kroening , Carnegie Mellon University
Karen Yorav , Carnegie Mellon University
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.
E. M. Clarke, K. Yorav and D. Kroening, "Specifying and Verifying Systems with Multiple Clocks," Proceedings 21st International Conference on Computer Design(ICCD), San Jose, California, 2003, pp. 48.