Akella, Venkatesh Gopalakrishnan, Ganesh
Description
Journal ArticleControl intensive ICs pose a significant challenge to the users of formal methods in designing hardware. These ICs have to support a wide variety of requirements including synchronous and asynchronous operations, polling and interrupt-driven modes of operation, multiple concurrent threads of execution, complex computations, and programmability. In this paper, we illustrate the use of formal methods in the design of a control intensive IC called the "Intel 8251" Universal Synchronous/Asynchronous Receiver/Transmitter (USART), using our formal hardware description language 'hopCP'. A feature of hopCP is that it supports communication via asynchronous ports (distributed shared variables writable by exactly one process), in addition to synchronous message passing. We show the usefulness of this combination of communication constructs. We outline static analysis algorithms to determine safe usages of asynchronous ports, and also to discover other static properties of the specific
Text
Unknown
College of EngineeringComputing, School of
©University of Utah