| |
Stephen Longfield and Rajit Manohar
VLSI systems are commonly specified using sequential executable
functional specifications, but implemented in a highly concurrent
manner. Alhough the methods to transform between the sequential
specification and concurrent implementation have been well-studied,
there are still substantial difficulties in verifying that the concurrent
implementation corresponds to the sequential specification after low-level
optimization. The majority of methods for doing this verification
have focused on strong semantic models for reasoning about systems and
their specifications, but these models can add significant unnecessary
complexity. In this paper, we explore a weak but effective method for
reasoning about implementation relations. We show how a sequential
embedding of a concurrent program can be generated, and how that
embedding can be used to dramatically reduce the reachable state space
of the verification problem while maintaining the semantic model of
interest.
|
|
