29 - 30 October, 2019

Holiday Inn Munich City Centre

Munich, Germany

Event Details

MP Associates, Inc.
WEDNESDAY October 30, 1:15pm - 2:45pm | Forum 6
EVENT TYPE: REGULAR SESSION
SESSION 7
Formal Verification
7.1Semi-formal Reformulation of Requirements for Formal Property Verification
Ambiguously specified requirements can be a source of risk for safety-critical electronic designs. Requirement specifications in natural language are also subject to misinterpretation. A method is proposed that reduces the risk of misinterpretations. Requirements are reformulated into semi-formal properties, which we call Natural Language Properties (NLPs). These statements are composed of natural language patterns which are then translated into SystemVerilog for formal verification. This reformulation is done by an independent verification engineer and then reviewed by the requirements engineer. Applying this technique for the verification of the CERN Radiation MOnitoring Electronics (CROME) led to the discovery of a safety-critical fault.
 Speaker: Katharina Ceesay-Seitz - CERN - European Organization for Nuclear Research
 Authors: Katharina Ceesay-Seitz - CERN - European Organization for Nuclear Research
Hamza Boukabache - CERN - European Organization for Nuclear Research
Daniel Perrin - CERN - European Organization for Nuclear Research
7.2Retrascope: Open-Source Model Checker for HDL Descriptions
Retrascope is a toolkit for static analysis and functional verification of hardware designs. The toolkit allows analyzing of HDL descriptions, reconstructing and visualization of the underlying models and using the derived models for test generation, property checking and other tasks. Retrascope is organized as an extendible framework with the ability to add new types of models as well as tools for their analysis and transformation. The primary application domain of the toolkit is functional verification of hardware at unit level. Several verification engines of the toolkit use model checking based approach for test generation. The tool is applicable to both Verilog and VHDL descriptions.
 Speaker: Sergey Smolov - Ivannikov Institute for System Programming of the RAS
 Authors: Alexander Kamkin - Ivannikov Institute for System Programming of the RAS
Mikhail Lebedev - Ivannikov Institute for System Programming of the RAS
Sergey Smolov - Ivannikov Institute for System Programming of the RAS
7.3ISO 26262:2018 Fault Analysis in Safety Mechanisms
ISO 26262-5 mandates the determination of hardware safety metrics, including SPFM and LFM. Latent and residual diagnostic coverage are also important metrics to assess the effectiveness of safety mechanisms. Achieving ASIL-D compliance is particularly challenging, and may require a detailed analysis of faults in the safety mechanisms. We propose a comprehensive, automated fault analysis method that covers safety mechanisms with and without error correction capabilities, and drastically reduces the need for expert judgements and fault simulation. This method is accurate and scalable to industrial projects. We present results of its application to a FIFO design implemented using an ECC-protected memory.
 Speaker: Jörg Grosse - OneSpin Solutions GmbH
 Authors: Jörg Grosse - OneSpin Solutions GmbH
Mark Hampton - OneSpin Solutions GmbH
Sergio Marchese - OneSpin Solutions GmbH
Jörg Koch - Renesas Electronics Europe GmbH