The annual osmosis event is a dynamic platform for exchanging successes achieved through applying formal techniques to overcome verification challenges. It offers a unique opportunity to connect and engage with our accomplished research and development (R&D) experts and participants.
Conference program*
| Time | Topic | Presenter |
|---|---|---|
| 08:30 - 09:30 | Registration | |
| 09:30 - 09:45 | Welcome and Introduction | Chris Giles - Siemens |
| 09:45 - 10:30 | Formally verifying security properties of CHERI hardware and software | Thomas Bauereiss – University of Cambridge, CHERI Alliance
Louis-Emile Ploix – University of Oxford, CHERI Alliance
|
|
10:30 - 11:00
|
Coffee Break | |
| 11:00 - 11:30 |
Adaptable FWHW Formal Co-Verification of SoC RISC-V Components
The increasing shift towards the RISC-V open-source instruction set architecture requires the development of new design techniques. In recent years, it has been demonstrated that RISC-V designs can be generated in a modular and scalable manner by utilizing metamodeling techniques. However, verifying these designs presents a significant challenge, because the verification must consider both Register Transfer Level (RTL) components and firmware components such as drivers. Furthermore, the interaction between firmware and hardware components is susceptible to various issues, including incorrect transaction sequences, synchronization problems, encoding mismatches, and reserved values. Traditionally, verifying the interaction between hardware and firmware requires simulation/emulation tools and verification engineers with expertise in both firmware and hardware. To overcome these challenges, this work introduces an automated formal verification approach for FWHW Co-verification of peripherals such as timers and interrupt controllers, and their respective drivers in generated RISC-V designs. This verification process employs formal verification methods. This methodology enables the detection of bugs in both hardware and firmware because it consists of the verification of individual components that can be reused later in the integration process. By implementing this methodology in the early design stages, developers can identify and address potential issues more efficiently and avoid later corrections.
|
Bryan Olmos - Infineon
|
| 11:30 - 12:30 |
Panel: Transforming Formal Verification from Challenge to Competitive Advantage
For years Formal tools have leveraged machine learning techniques like Reinforcement Learning under-the-hood to achieve disproportionate performance gains vs. other approaches. Building on this, how can generative AI / LLMs and agentic AI technologies benefit the tools’ performance and end-users’ productivity?
|
Moderator: Chris Giles – Siemens
Panelists:
Cedric Walravens – ICsense, Tobias Ludwig – Lubis EDA, Vladislav Palfy – Siemens, Dominik Strasser – Siemens
|
| 12:30 - 14:00 |
Lunch
|
|
| 14:00 - 14:30 |
Harnessing AI for real-world hardware verification: A hands-on look at Questa One Property Assist AI
AI is generating enormous excitement in engineering—but how can it be applied to perform practical, high-value tasks, and how trustworthy is it in sensitive workflows? In this session, we’ll explore Siemens EDA’s Property Assist AI solution, a cutting-edge agentic tool that leverages local, private large language models (LLMs) to streamline the hardware verification process. Attendees will see how AI can help engineers work faster, reduce errors, and enhance productivity, all while maintaining security and control over proprietary data. Join us to discover actionable ways AI can transform verification workflows in your projects.
|
Matthew Taylor – Doulos |
| 14:30 - 15:00 |
Ground truth in the age of AI: abstract models as the anchor of verification
AI can support design, where creativity is valuable. Verification, in contrast, demands determinism. Both processes, however, must share a common ground truth. Abstract models provide this anchor, and through formal methods we can establish a sound link to RTL. We show how our property generator enables this connection, ensuring AI-driven design and verification remain grounded in the same truth.
|
Tobias Ludwig – Lubis EDA
|
| 15:00 - 15:30 | Stimulus free verification of a clock bridge design using static and formal | Kanthi Palaniappan – Nokia |
| 15:30 - 16:00 |
Coffee Break
|
|
| 16:00 - 16:30 | Boosting Verification of an IEEE compliant FPU with Formal and AI capabilities |
Zvi Ben-Yosef – NextSilicon |
| 16:30 - 17:00 |
Combining Performance and Formal Security Guarantees for Hardware Accelerators
Security and data-dependent optimizations are often seen as conflicting, resulting in overly cautious countermeasures. For instance, optimizations that introduce fast computation paths, such as multiplying by zero, may create dangerous timing side channels. Therefore, recent methods suggest disabling such optimizations in favor of security when processing confidential information. We present a novel framework that hardens hardware accelerators against data-dependent timing vulnerabilities. Our approach takes the confidentiality levels of the operands into account and enables dynamic performance optimization, even when private data is involved. The proposed framework is based on formal verification, which ensures exhaustive security guarantees. Case studies on four different accelerator architectures show that accelerators optimized by our framework significantly outperform conservative security mechanisms. |
Lucas Deutschmann - RPTU University Kaiserslautern-Landau |
| 17:00 - 17:45 | Technology spotlight: the latest in Siemens Formal Verification Suite | Chris Giles – Siemens |
| 19:00 - 23:00 | Complimentary Dinner |
*Agenda is subject to change without notice.
On-demand presentations
Check out on-demand presentations from prior osmosis.