How to Formalize FPGA Hardware Design

HOLEČEK, Jan, Tomáš KRATOCHVÍLA, Vojtěch ŘEHÁK, David ŠAFRÁNEK a Pavel ŠIMEČEK. How to Formalize FPGA Hardware Design. Praha: CESNET, z.s.p.o., 2004. CESNET Technical Report No. 04/2004.

Základní údaje

Originální název

How to Formalize FPGA Hardware Design

Název česky

Kterak formalizovat hardwarový design FPGA čipů

Autoři

HOLEČEK, Jan (203 Česká republika), Tomáš KRATOCHVÍLA (203 Česká republika), Vojtěch ŘEHÁK (203 Česká republika, garant), David ŠAFRÁNEK (203 Česká republika) a Pavel ŠIMEČEK (203 Česká republika)

Vydání

Praha, CESNET Technical Report No. 04/2004, 2004

Nakladatel

CESNET, z.s.p.o.

---

Další údaje

Jazyk

angličtina

Typ výsledku

Audiovizuální tvorba

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Česká republika

Utajení

není předmětem státního či obchodního tajemství

Odkazy

URL

Kód RIV

RIV/00216224:14330/04:00010387

Organizační jednotka

Fakulta informatiky

Klíčová slova anglicky

formal verification; programmable hardware; FPGA; Cadence SMV; VHDL

Štítky

Cadence SMV, formal verification, FPGA, programmable hardware, VHDL

---

Anotace

V originále

In this report, a formal view of an FPGA hardware design is presented. An approach of how elementary FPGA design entities can be modeled in terms of Kripke structures is presented here. The report is also focused on capturing the problems of modeling synchronous parts of hardware design together with its asynchronous parts.

Česky

V této zprávě nahlížíme z formálního hlediska na HW design pro FPGA čipy a modelujeme ho jako Kripkeho strukturu. Dále je zde zpracován problém společného modelování synchronních a asynchronních částí designu.

---

Návaznosti

GA201/03/0509, projekt VaV	Název: Automatizovaná verifikace paralelních a distribuovaných systémů Investor: Grantová agentura ČR, Automatizovaná verifikace paralelních a distribuovaných systémů
MSM 000000001, záměr	Název: Vysokorychlostní síť národního výzkumu a její nové aplikace
MSM 143300001, záměr	Název: Nesekvenční modely výpočtů - kvantové a souběžné distribuované modely výpočetních procesů Investor: Ministerstvo školství, mládeže a tělovýchovy ČR, Nesekvenční modely výpočtů -- kvantové a souběžné distribuované modely výpočetních procesů