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...
Հիմնական հեղինակներ: | , , |
---|---|
Ձևաչափ: | 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. |
---|