SPIN as a Hardware Design Tool

This paper presents the application of SPIN to verify a hardware design modelled in PROMELA and verified with SPIN, showing the presense of hazard.

Abstract

This paper presents the application of SPIN to verify a hardware design. A hazardoues circuit is modelled in PROMELA and verified with SPIN. SPIN shows the presense of hazard. The circuit was corrected and verified. Keywords: hardware design and verification, protocol engineering, CASE tools, PROMELA, SPIN. 1 Introduction One engineering approach to design and analyze a large and complex hardware design is to decompose the design into modules or sub-designs, each of which can be developed and verified individually. In the final design, these modules interact or communicate with each other with a set of predefined rules: a protocol. While individual modules may have been proven to be correct, the composition of them does not necessarily exhibit the expected behavior. The design must still be validated or verified. In this paper, we argue that tools to validate computer protocols can be used to verify hardware designs. We illustrate this by modelling a simple circuit in PROMELA, a lang...