The RASSP Digest - Vol. 3, September 1996
A Formal Model of Digital Systems Compatible with VHDL
by Philip A. Wilsey, Sheetanshu L. Pandey and Kothanda Umamageswaran
Abstract
Hardware Description Languages (HDLs) play an important role in the design and verification of digital devices. Unfortunately most HDLs are informally defined and thus, they are frequently defined only partially, with some aspects of the language subject to varying interpretation. The formal models project is developing formal models and theories for the standard hardware description language VHDL. Included in the project are a collection of theories for defining (i) when a VHDL description is well-typed, (ii) equivalent static structures within the language standard, (iii) the semantics of VHDL's evaluation (or simulation time) behaviors, and (iv) semantic preserving rewriting operators that are used to optimize the analysis and parallel simulation of VHDL.
1. Project Overview
Besides a formal syntax definition, few formal semantic models for Hardware Description Languages (HDLs) are ever constructed. Furthermore, informal (English) specifications of “so called” standard languages allow for numerous interpretations where only one is desired. This paper reports our efforts to construct formal models for the hardware description language VHDL. In particular, the project develops the following models and theories (Figure 1):
- Static Model: The static model is a set theoretic definition of post-elaborated VHDL models. Included in the static model are axioms that define when a VHDL model is well-typed (e.g., the data type of the target and expression in a signal assignment statement match).
- Equivalence Axioms: The equivalence axioms formally define equivalent structures in VHDL. The structures of VHDL included in the equivalence axioms are only those that are formally described to be equivalent in the language standard. For example, the language standard defines the equivalent process statement representation for a concurrent signal assignment statement.
- Reduction Algebra: While equivalence axioms define equivalent structures, the reduction algebra defines operators that transform between equivalent VHDL structures. The operators of the reduction algebra thus implement transforms that satisfy the constraints of the equivalence axioms. A mechanized theorem prover has been used to show that the rewriting operators correctly adhere to the constraints of the equivalence axioms.
- Dynamic Model: The dynamic model is a reduced form, set theoretic model derived from the static model. The dynamic model is derived from the static model using operators from the reduction algebra. Using the PVS theorem prover, this reduction has been shown to be complete and idempotent. Included in the dynamic model is a formal, declarative specification of the dynamic behaviors described by a VHDL model (hereafter called the dynamic semantics). The dynamic semantics is formed using an interval temporal logic and defines only the (signal and variable) state space defined by a specific VHDL model.
- Rewriting Operators: The rewriting operators are a collection of transforms that we use to optimize VHDL for parallel simulation. The transforms are shown to preserve the dynamic semantics of VHDL and are embedded in a VHDL analyzer/optimizer/code generator for optimizing the performance of the QUEST project time warp simulator. Initially, we have developed 16 rewriting operators to merge VHDL process statements and early experiments have shown speedups as high as 2.2.
In the remainder of this paper, we briefly describe our technology transfer activities (Section 2) and highlight the significance of the static model technology developed as part of this project (Section 3). Additional details on other aspects of this project can be found in the papers enumerated in the bibliography at the end of this paper. The project is also summarized on the web at the following URL: http://www.ece.uc.edu/~paw/rassp.
2. Technology Transfer
The formal modeling project includes efforts to support the transfer of technology into the practicing community of VHDL-based design and analysis of digital systems. These activities include the application of the formal models to optimize parallel simulation (described above in the rewriting operators) and the insertion of the technology into other VHDL analysis activities at the University of Cincinnati (Figure 2). In particular:
- The static model, well-formedness axioms, and reduction algebra are being used to aid VHDL analysis. The well-formedness axioms are being used in the type-checker of the SAVANT VHDL analyzer; the static model and reduction algebra is being used to define a reduced form intermediate representation (AIRE) that is being jointly developed with John Willis. The AIRE project is planning to develop and standardize the VHDL intermediate form. A VHDL intermediate file format is also planned.
- The dynamic model is being used to define the TyVIS parallel VHDL simulation kernel. The rewriting operators are being used by the VHDL optimizer/code generator in the SAVANT/QUEST projects.
3. Impact of the Static Model and Its Reduction
Many of the transforms that are formally developed in the static model exist in an informal form in the VHDL language reference manual. Some exist solely as additional reductions that can be used to simplify and optimize CAD tool construction. For example a simulation code generator can be greatly streamlined by the use of these transforms. More precisely, assume that a front end analyzer has been constructed to parse VHDL into the static model form and further, that a set of reduction procedures have been implemented to rewrite the model form according to the reduction algebra. By reducing the VHDL into its core constituent elements, a simulation code generator need only recognize the, much smaller, core language elements (the entire set of concurrent statements can be eliminated from the code generator's vocabulary).
The reduction algebra also simplifies the construction of a dynamic semantics for VHDL. In fact, several of the operators in the reduction algebra were developed specifically to simplify the construction of the dynamic model. For example, rewriting signal assignment statements so that the right-hand-side (rhs) is simply an expression instead of a waveform is a direct consequence of a desire to simplify construction of the dynamic semantics.
In addition, in the construction of the dynamic semantic model, we have also experienced unexpected benefits from the static model and its transformations. In particular, the representation of transport delays in signal assignment statements as inertial delay with a reject pulse limit of 0 nanoseconds has allowed us to derive a new approach for marking transaction lists. In particular, we have been able to develop a marking scheme that relies on constraints on time intervals rather than on a sequential algorithm that update transaction lists.
Finally, we expect to see additional benefits in the optimization of CAD tools as the formal models develop. For example, the static model and its transforms might well impact the design space explored by a synthesis tool. As another example, the new marking scheme described in the previous paragraph may significantly impact the performance of parallel simulation subsystems. While we expect to see additional benefits, further developments of the semantic models and the associated transforms must be developed and applied in the construction and optimization of CAD tools. We are exploring these avenues in several other research projects.
Bibliography
[1] S.L. Pandey, D.M. Benz, and P.A. Wilsey, “Formalizing the Static Structures of HDLs for the Optimization of CAD Tools,” IEEE Trans. on Computer-Aided Design of Integrated Circuits and Systems. (submitted).
[2] S. Pandey, K. Umamageswaran, and P.A. Wilsey, “A Complete Reduction Algebra for VHDL,” International Conference on Formal Methods in Computer-Aided Design (FMCAD), November 1996. (submitted).
[3] S. L. Pandey, K. R. Subramanian, and P. A. Wilsey, “A Semantic Model of VHDL for Validating Rewriting Algebras,” EuroMicro '96, September 1996. (forthcoming).
[4] P. A. Wilsey, D. M. Benz, and S. L. Pandey, “A Model of VHDL for the Analysis, Transformation, and Optimization of Digital System Designs,” Conference on Hardware Description Languages (CHDL'95), 611-616, August 1995.
[5] T. McBrayer and P. A. Wilsey, “Process Combination to Increase Event Granularity in Parallel Logic Simulation,” 9th International Parallel Processing Symposium, 572-578, April 1995.
[6] P. A. Wilsey, “Formal Models of Digital Systems Compatible with VHDL,” Working Document, Computer Architecture Design Laboratory, University of Cincinnati, 1994 (revised 1995, 1996). (available on the www at http://www.ece.uc.edu/~paw/rassp).
Philip A. Wilsey, Sheetanshu L. Pandey
and Kothanda Umamageswaran
Computer Architecture Design Laboratory
Dept. of ECECS, PO Box 210030
University of Cincinnati
Cincinnati, OH 45221-0030
paw@ece.uc.edu
Newsletter Index
The RASSP Digest - Vol. 3, September 1996
newsletter/html/96sep/news_20.html