Verification Results in Liberouter Project
Jan Holeček, Tomáš Kratochvíla, Vojtěch Řehák, David Šafránek, Pavel Šimeček · 2004
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.