This technical report presents current results of the formal verification of VHDL design of Liberouter and Scampi hardware accelerator card for packet routing, originating from the Liberouter project. We use the symbolic model checker Cadence SMV to prove desired properties of separate units of the design. We have verified many properties of the number of units. Moreover, we have also gained precious experiences concerning the fight with the state explosion problem.
Česky
Tato technická zpráva popisuje naše výsledky verifikace hardwarových návrhů komponent karet Liberouter a Scampi v rámci projektu Liberouter. Používáme symbolický model checker Cadence SMV, do jehož vstupního jazyka převádíme zdrojový VHDL kód přes Verilog. Tímto způsobem jsme ověřili mnoho vlastností HW komponent.
Návaznosti
GA201/03/0509, projekt VaV
Název: Automatizovaná verifikace paralelních a distribuovaných systémů
Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 000000001, záměr
Název: Vysokorychlostní síť národního výzkumu a její nové aplikace