Verification Results in Liberouter Project

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

HOLEČEK Jan KRATOCHVÍLA Tomáš ŘEHÁK Vojtěch ŠAFRÁNEK David ŠIMEČEK Pavel

Year of publication 2004
Type R&D Presentation
MU Faculty or unit

Faculty of Informatics

Citation
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.