A methodology to take credit for high-level verification during RTL verification

DOI10.1007/S10703-017-0299-2zbMath1386.68100OpenAlexW2756079799MaRDI QIDQ1696592

Robert Kurshan, Frederic Doucet

Publication date: 14 February 2018

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-017-0299-2

zbMATH Keywords

high-level synthesisrefinementabstractioncoverageSystemCmicro-architecturehigh-level verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Esterel

Cites Work

• Unnamed Item
• Statecharts: a visual formalism for complex systems
• The Esterel synchronous programming language: Design, semantics, implementation
• Verification of system level model transformations
• Parameterized Model Checking of Rendezvous Systems
• Verification Technology Transfer
• Decidability of Parameterized Verification
• Parameterized Systems in BIP: Design and Model Checking
• Modular refinement of hierarchic reactive machines

This page was built for publication: A methodology to take credit for high-level verification during RTL verification