Towards model checking the hardware description language BSV

As electronic applications are supposed to be compact, fast and at the same time use as little energy as possible, hardware components are increasingly replacing software in such devices. As it is difficult and very expensive to test hardware once it has been created, it becomes more and more important to have the right tools to investigate its properties already in the design phase or before it is permanently turned into hardware. For this purpose formal methods like model checking play an important role. Bluespec System Verilog (BSV) is a high level hardware description language that was developed at Massachusetts Institute of Technology in association with Bluespec Inc. It is an object oriented language that can be compiled directly into hardware code (synthesizable). It is also equipped with a standard compiler that compiles into executable code that allows it to be simulated by providing the computation traces before the actual hardware is created. Some effort has been made to verify properties of BSV programs by means of theorem provers but so far the model checking approach has not been used for this purpose. In this talk we make the first step towards translating BSV into the real time system description language Uppaal. This allows a for a model checking of BSV designs before the final electronic product is produced