Conclusions

Abstract

In the previous chapters, a declarative semantics for VHDL was presented. Essentially, a set of time intervals spanning the simulation period was defined and constraints over the evaluation intervals of processes were established against this set. Intermediate sets were constructed defining transaction lists maintained by every process for each signal to which an assignment has been made in that process. However, the definition of the transaction lists was declarative and it was pointed out that this intermediate definition was not necessary but merely simplified the semantics. The embeddeing of the model in PVS was discussed, the validity of the model was proven, the need for a translation unit to convert VHDL source level descriptions to PVS language was argued, and a specific implementation of the translator using SAVANTwas shown. In addition, proofs methodologies were demonstrated using the embedding of the models in PVS. In particular, the validation of process folding and signal collapsing was presented. The aim of this project is to explore the diverse applications of the semantics and to demonstrate its utility in CAD tool optimization.