@MASTERSTHESIS\{IMM2007-05597,
    author       = "M. P. Pytel",
    title        = "A graphical analysis tool for hardware design",
    year         = "2007",
    keywords     = "hardware descriptions, graphical representation, model-checking, verification, {GEZEL,} NuSMV",
    school       = "Informatics and Mathematical Modelling, Technical University of Denmark, {DTU}",
    address      = "Richard Petersens Plads, Building 321, {DK-}2800 Kgs. Lyngby",
    type         = "",
    note         = "Supervised by Assoc. Prof. Michael R. Hansen, {IMM,} {DTU}.",
    url          = "http://www2.compute.dtu.dk/pubdb/pubs/5597-full.html",
    abstract     = "In 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."
}