Project detail

Application of methods and techniques of formal verification in the design of advanced digital circuits

Duration: 01.01.2013 — 31.12.2013

Funding resources

Ministerstvo školství, mládeže a tělovýchovy ČR - Fond rozvoje vysokých škol (FRVŠ)

- whole funder (2013-01-01 - 2013-12-31)

On the project

Projekt je zaměřen na přípravu a vytvoření nových podpůrných studijních a demonstračních materiálů v třech stávajících kurzech dvouletého magisterského studijního programu Informační technologie.  Jedná se o kurzy Hardware-software Codesign (HSC), Návrh externích adaptérů a vestavěných systémů (NAV) a Pokročilé číslicové systémy (PCS).


Cílem projektu je přiblížit studentům techniky formální verifikace číslicových systémů, především verifikace založené na tzv. formálních tvrzeních (angl. assertions), které se používají pro zápis specifikace systému. Zavedení technik využívajících formální přístup přináší do procesu verifikace nový pohled, výrazně odlišný od verifikačních technik založených na testování, které typicky generují náhodné vstupní vektory a sledují odezvy systému.
Součástí vytvořených materiálů budou i příklady použití formální verifikace připravené s využitím moderních verifikačních nástrojů používaných v praxi, které má fakulta k dispozici.

Description in English
This project is aimed at creating new supplementary study and demonstration materials in three current courses of two-year master degree programme Information Technology. The courses are as follows: Hardware/software Codesign (HSC), Design of External Adapters and Embedded Systems (NAV) and Advanced Digital Systems (PCS).


Primary goal of the project is to expound the students the techniques of formal verification used in the area of digital systems design, especially verification based on assertions. Assertions are used to describe specification of the system.
Implementing formal verification methods and steps into the verification process benefits of new abstract view which is completely different from verification methods based on testing producing pseudo-random input vectors to the system and observing its output.
The set of materials will also comprise from use cases of formal verification prepared to be used with the latest verification tools used in the industry. These tools are available at the faculty in its license subscription.

Keywords
formální verifikace, číslicové systémy

Key words in English
formal verification, digital circuits

Mark

FR1086/2013/G1

Default language

Czech

People responsible

Kajan Michal, Ing. - fellow researcher
Kotásek Zdeněk, doc. Ing., CSc. - fellow researcher
Zachariášová Marcela, Ing., Ph.D. - principal person responsible

Responsibility: Zachariášová Marcela, Ing., Ph.D.