Abstract
This chapter presents an embedding of the dynamic semitics of VHDL in PVS. The semantics is embedded by defining a set of equivalence axioms between VHDL descriptions. We present a shallow embedding of the semantics that consists of a set of functions that describe the transformations that a signal undergoes during the simulation process.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Notes
The compete set of axioms and the theorems can be found on the WWW [48]
It is equal to the initial value of the signal before the first sequential statement of every process statement.
Author information
Authors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer Science+Business Media New York
About this chapter
Cite this chapter
Umamageswaran, K., Pandey, S.L., Wilsey, P.A. (1999). A Framework for Proving Equivalences using PVS. In: Formal Semantics and Proof Techniques for Optimizing VHDL Models. Springer, Boston, MA. https://doi.org/10.1007/978-1-4615-5123-2_10
Download citation
DOI: https://doi.org/10.1007/978-1-4615-5123-2_10
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-4613-7331-5
Online ISBN: 978-1-4615-5123-2
eBook Packages: Springer Book Archive