Siemens Enhances Software Verification Tool with Formal Methods

Siemens Digital Industries Software has introduced two groundbreaking enhancements in C++ software verification, marking a significant advancement in the field. The latest iteration of the Catapult tool now incorporates C++ formal property checking and reachability coverage analysis, offering a comprehensive solution for high-level design verification.

The Formal Assert tool, specifically designed to complement the Siemens Catapult software, aims to bring established formal verification methods from the RTL world to high-level design. This integration enables designers to utilize formal methods to validate that a high-level design representation adheres to a given specification. With Catapult Formal Assert, designers can ascertain the occurrence or non-occurrence of specific properties, such as value ranges or signal values, enhancing the overall verification process.

Formal CoverCheck, the counterpart to Catapult Coverage software, extends the capabilities of Siemens' simulation-based tool by conducting reachability analysis on coverage gaps. By generating waivers for formally proven unreachable items, this tool assists users in achieving comprehensive coverage closure on their HLS design source efficiently. The combined use of Formal Assert and CoverCheck streamlines the verification process and ensures the integrity of the design.

Mo Movahed, Vice President and General Manager for High-Level Design, Verification, and Power at Siemens Digital Industries Software, emphasized the significance of these tools in advancing verification and design methodologies. By integrating formal methods into C++ verification, semiconductor teams can leverage the power of High-Level Synthesis and Verification, propelling innovation in the industry.

The adoption of high-level design and synthesis is on the rise across various applications and markets, driven by the substantial verification throughput gains offered by Catapult HLS software. This shift has underscored the need to bridge the gap between RTL and High-Level Design verification methodologies, as the latter lacks a well-established infrastructure for metrics-driven verification. The introduction of Catapult Formal Assert and CoverCheck addresses this need, empowering verification teams to meet specific design targets effectively.