Verification Results in Liberouter Project
| Authors | |
|---|---|
| Year of publication | 2004 |
| Type | R&D Presentation |
| MU Faculty or unit | |
| 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: |