Скачать с ютуб How Much Formal Verification is Enough? by Nicolae Tusinschi​, Formal Verification, Siemens EDA в хорошем качестве

How Much Formal Verification is Enough? by Nicolae Tusinschi​, Formal Verification, Siemens EDA

In hardware verification world there is a question that is being asked always – how much verification is enough? It applies to all verification techniques. Several techniques developed means to measure it with functional and code coverage and it does apply to formal verification without reserves. The question we tackle with current talk is: how much formal verification is enough? One would suggest a flow that should answer the question, starting with requirements specification, planning, testbench development, prove properties, coverage measure and sign-off. This approach has its pitfalls like missing requirements leading to missing properties, verification pitfalls: over and under constraining, mistakes in assertion writing, all leading to a negative outcome of verification: re-design and re-verification. With current presentation we will walk you through an automated and formal check on the properties to check for completeness where all possible input sequences are examined, all outputs are verified at all times. The complete property set forms an abstract model of the system where all design behavior is exposed and can back-out undocumented specification from the abstract model building a closed-loop verification process using SystemVerilog Assertions. The GapFree verification method is ideal for high-consequence systems where the complete verification is required and is unique among formal property verification tool capabilities. BIO: Nicolae Tusinschi is a product manager for formal verification solutions at Siemens EDA. He holds a Master’s degree combined between the University of Southampton and the University of Kaiserslautern. After a Master’s thesis at Continental, Nicolae joined OneSpin, where he worked in QA, then as a product specialist and later served as product owner for design verification tools at OneSpin. His key projects include integrating simulation coverage with formal metrics, leveraging coverage results in the verification process, formal verification of RISC-V cores.