"4346" . . "\u010Cl\u00E1nek se zab\u00FDv\u00E1 probl\u00E9mem ov\u011B\u0159ov\u00E1n\u00ED model\u016F re\u00E1ln\u00FDch hardwarov\u00FDch syst\u00E9m\u016F specifikovan\u00FDch pomoc\u00ED jazyka VHDL. Zp\u016Fsob verifikace je zalo\u017Een na p\u0159ekladu VHDL program\u016F do jazyka Cadence SMV. V\u00FDsledky uveden\u00E9 v tomto \u010Dl\u00E1nku se zam\u011B\u0159uj\u00ED na re\u00E1lnou verifikaci hardwarov\u00FDch obvod\u016F s asynchronn\u00EDmi komponentami. \u010Cl\u00E1nek uv\u00E1d\u00ED dva p\u0159\u00EDstupy v\u010Detn\u011B experiment\u00E1ln\u00EDho ov\u011B\u0159en\u00ED."@cs . "[D21C78DE98BF]" . "RIV/63839172:_____/07:00000636" . "The paper considers the problem of model checking real-life VHDL- based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, i.e. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project."@en . "\u0160afr\u00E1nek, David" . "\u0158eh\u00E1k, Vojt\u011Bch" . "formal verification; model checking; VHDL; asynchronous clock domains"@en . "16"^^ . "148;164" . "Verifying VHDL Designs with Multiple Clocks in SMV"@en . "DE - Spolkov\u00E1 republika N\u011Bmecko" . "2007" . . . "Verifikace VHDL program\u016F s v\u00EDce hodinami pomoc\u00ED SMV"@cs . . . . . . . "Verifying VHDL Designs with Multiple Clocks in SMV" . . . . "457811" . "The paper considers the problem of model checking real-life VHDL- based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, i.e. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project." . . "0302-9743" . "Verifying VHDL Designs with Multiple Clocks in SMV" . . "Verifying VHDL Designs with Multiple Clocks in SMV"@en . "6"^^ . . "RIV/63839172:_____/07:00000636!RIV08-MSM-63839172" . "Vojnar, Tom\u00E1\u0161" . . "Matou\u0161ek, Petr" . "Lecture Notes in Computer Science" . "Verifikace VHDL program\u016F s v\u00EDce hodinami pomoc\u00ED SMV"@cs . . . "6"^^ . . "Z(MSM6383917201)" .