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.
