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 ou...

Ամբողջական նկարագրություն

Մատենագիտական մանրամասներ
Հիմնական հեղինակներ: Clarke, E, Kroening, D, Yorav, K
Ձևաչափ: Conference item
Հրապարակվել է: IEEE 2003
Նկարագրություն
Ամփոփում: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.