Formal verification is state-of-the-art domain of applied computer science. In the Liberouter project we use various formal methods, especially model checking, to prove the correctness of the Liberouter hardware and software design against its specification.

In our Formal verification team we formalize the specification of components under verification using modal and temporal logics. We also develop tools which automatize the process of translation of VHDL sources into languages accepted by verification tools.

The following schema shows the unit structure of projects we have verified. Clicking on darkned boxes the verification results for a particular unit can be seen in the form of Verification report.

Related documents

November 2004	Verification Process of Hardware Design in Liberouter Project (pdf, ps, xml)
October 2004	How to Formalize FPGA Hardware Design (pdf, ps, xml)
September 2004	Verification Results in Liberouter Project (pdf, ps, xml)
November 2003	Verification of COMBO6 VHDL Design (pdf, ps, xml)
January 2003	Packet header matching in Combo6 IPv6 router (pdf, ps, xml)
June 2002	Model checking in IPv6 Hardware Router Design (pdf, ps, xml)