Specifying and Verifying Systems with Multiple Clocks

San Jose, California October 13-October 15

DOI Bookmark:

http://doi.ieeecomputersociety.org/10.1109/ICCD.2003.1240872

2003 IEEE International Conference on ...

	This Article
	PURCHASE ARTICLE: $19 PDF HTML IEEE Xplore Subscribers
	Share
	Email this Article to a friend
	Bibliographic References
	ASCII Text BibTex RefWorks Procite/RefMan/Endnote
	Add to:
	Digg Furl Spurl Blink Simpy Google Del.icio.us Y!MyWeb
	Search
	Similar Articles Articles by Edmund M. Clarke Articles by Daniel Kroening Articles by Karen Yorav

	ASCII Text	x
	Edmund M. Clarke, Daniel Kroening, Karen Yorav, "Specifying and Verifying Systems with Multiple Clocks," Computer Design, International Conference on, pp. 48, 2003 IEEE International Conference on Computer Design (ICCD'03), 2003.

	BibTex	x
	@article{ 10.1109/ICCD.2003.1240872, author = {Edmund M. Clarke and Daniel Kroening and Karen Yorav}, title = {Specifying and Verifying Systems with Multiple Clocks}, journal ={Computer Design, International Conference on}, volume = {0}, year = {2003}, issn = {1063-6404}, pages = {48}, doi = {http://doi.ieeecomputersociety.org/10.1109/ICCD.2003.1240872}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }

	RefWorks Procite/RefMan/Endnote	x
	TY - CONF JO - Computer Design, International Conference on TI - Specifying and Verifying Systems with Multiple Clocks SN - 1063-6404 SP EP A1 - Edmund M. Clarke, A1 - Daniel Kroening, A1 - Karen Yorav, PY - 2003 KW - null VL - 0 JA - Computer Design, International Conference on ER -

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.

Citation:

Edmund M. Clarke, Daniel Kroening, Karen Yorav, "Specifying and Verifying Systems with Multiple Clocks," iccd, pp.48, 2003 IEEE International Conference on Computer Design (ICCD'03), 2003

Peer Review Notice | Give Us Feedback

Usage of this product signifies your acceptance of the Terms of Use.