Executable protocol specification in ESL

8Citations
Citations of this article
5Readers
Mendeley users who have this article in their library.
Get full text

Abstract

Hardware specifications in English are frequently ambiguous and often self-contradictory.We propose a new logic ESL which facilitates formal specification of hardware protocols. Our logic is closely related to LTL but can express all regular safety properties. We have developed a protocol synthesis methodology which generates Mealy machines from ESL specifications. The Mealy machines can be automatically translated into executable code either in Verilog or SMV. Our methodology exploits the observation that protocols are naturally composed of many semantically distinct components. This structure is reflected in the syntax of ESL specifications.We use a modified LTL tableau construction to build a Mealy machine for each component. The Mealy machines are connected together in a Verilog or SMV framework. In many cases this makes it possible to circumvent the state explosion problem during code generation and to identify conflicts between components during simulation or model checking.We have implemented a tool based on the logic and used it to specify and verify a significant part of the PCI bus protocol.

Cite

CITATION STYLE

APA

Clarke, E., German, S., Lu, Y., Veith, H., & Wang, D. (2000). Executable protocol specification in ESL. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 1954, pp. 197–216). Springer Verlag. https://doi.org/10.1007/3-540-40922-x_13

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free