A graphical analysis tool for hardware design

Mariusz Pawel Pytel

AbstractIn order to meet requirements imposed by a rapid grow in complexity of chips, existing design and verification methodologies have to be extended and a new ones created.

The main objective of this master thesis is to investigate possibilities for improvement in creation and verification of high-level hardware description language models. GEZEL is an example of such a high-level hardware description language, which models hardware according to the semantics of the finite-state machine with datapath (FSMD). This feature of the language allows use of symbolic model checkers like NuSMV in the automated validation process. Both, GEZEL and NuSMV are presented in the report, and their parts relevant to the project explained.

As a part of the project a graphical tool was developed that visualizes hardware models and supports hardware architect in development process. The tool is able to check, whether model obey well-formedness conditions and provides means for full functional check by generation of NuSMV representation of the model, which further can be validated using this symbolic model checker.
Keywordshardware descriptions, graphical representation, model-checking, verification, GEZEL, NuSMV
TypeMaster's thesis [Academic thesis]
Year2007
PublisherInformatics and Mathematical Modelling, Technical University of Denmark, DTU
AddressRichard Petersens Plads, Building 321, DK-2800 Kgs. Lyngby
SeriesIMM-Thesis-2007-111
NoteSupervised by Assoc. Prof. Michael R. Hansen, IMM, DTU.
Electronic version(s)[pdf]
BibTeX data [bibtex]
IMM Group(s)Computer Science & Engineering