Towards model checking BSV in Uppaal
Hörður Hauksson · 2013
In recent years the complexity of hardware design for parallel processes has increased considerably. Despite advances in structural abstractions of description languages none has the ability to simulate reactive systems and model check in a graphical manner. In this thesis we argue for the viability of translating between two seemingly different languages, the high level hardware description language Bluespec SystemVerilog and the modelling language of Uppaal, an integrated environment for validating and verifying real time systems. We propose a scheme for mapping constructs between the two languages and provide a prototype of a translator from a shallow version of BSV to Uppaal.; Honnun smarasa hefur a siðari arum orðið sifellt floknari. Likon fyrir samsiða keyrslur hafa reynst serlega erfið viðureignar og honnunargalla hefur oftar en ekki fyrst orðið vart a framleiðslustigi rasa eða við notkun þeirra. Þratt fyrir framfarir i gerð skilgreiningamala gefur ekkert þeirra faeri a myndraenni framsetningu við að greina likon. I þessari ritgerð leiðum við rok að þvi að þýða megi a milli skilgreiningamalsins Bluespec SystemVerilog (BSV) og Uppaal, sem er taeki til að sannreyna magþraða kerfi a myndraenan hatt og finna veikleika i honnun þeirra. Sýnt er fram a að þýða megi milli þessara mala og sett er fram frumgerð að þýðanda sem þýðir ur einfaldaðri utgafu af BSV yfir i likanamal Uppaal.