Verification Results in Liberouter Project

• 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
• 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

• Automated Verification of Parallel and Distributed Systems
• Non-sequential Models of Computing -- Quantum and Concurrent Distributed Models of Computing