Detail projektu

Využití metod a nástrojů formální verifikace při vývoji pokročilých číslicových systémů

Období řešení: 01.01.2013 — 31.12.2013

Zdroje financování

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

- plně financující (2013-01-01 - 2013-12-31)

O projektu

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.

Popis anglicky
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.

Klíčová slova
formální verifikace, číslicové systémy

Klíčová slova anglicky
formal verification, digital circuits

Označení

FR1086/2013/G1

Originální jazyk

čeština

Řešitelé

Zachariášová Marcela, Ing., Ph.D. - hlavní řešitel
Kajan Michal, Ing. - spoluřešitel
Kotásek Zdeněk, doc. Ing., CSc. - spoluřešitel

Odpovědnost: Zachariášová Marcela, Ing., Ph.D.