Download technical descriptions of OneSpin products and apps
OneSpin® 360 DV Floating Point Unit App
OneSpin’s Floating Point Unit (FPU) App is the industry’s first and only solution for the formal verification of floating-point hardware compliant to IEEE 754 standard. The FPU App includes a reliable, extensively tested model of floating-point arithmetic operations, optimized for formal analysis. Engineers can setup the app within minutes and uncover deep, obscure corner case bugs with minimal effort. The proven ability of FPU App to find bugs even on already verified production designs is testament to its maturity, effectiveness, and unprecedented exhaustive coverage of floating-point arithmetic operands.
OneSpin® 360 DV-Inspect™
360 DV-Inspect automatically inspects the RTL code once it has been compiled, without the need for any testbench setup. This code inspection comprises Easy Lint and exhaustive formal analysis with interactive debugging, eliminating an extensive amount of early simulation and stimulus creation while identifying issues before they result in serious bugs. Thus, DV-Inspect lends itself as a sign-off criterion for handing off an RTL block to functional verification and integration into automated daily regression runs.
OneSpin® 360 DV-Verify™
OneSpin 360 DV-Verify extends the DV- Inspect platform with coverage-driven Assertion-Based Verification (ABV). Many entry-level formal apps allow for assertion generation for specific problems without a need for deep formal knowledge. For AMBATM protocols, formal VIPs allow for exhaustive verification of all protocol rules, including providing the needed protocol constraints and interesting cover points. For register maps specified in formats such as IP-XACTTM, the Register Checking App 3(CSR) automates the exhaustive verification that the RTL correctly implements the specified register map. Data transport verification for blocks like FIFOs or bus bridges can be highly automated with the Scoreboard App, exhaustively finding any corruption in the data stream efficiently. A Connectivity App allows for fast chip-level connectivity analysis and X-propagation issues can be automatically examined with the X-Prop App. A generic Verification Planning Integration App allows to integrate the formal assertion results with verification planning tools, enabling a single verification plan for formal and simulation-based verification.
OneSpin® 360 DV Verification Planning Integration App
In a systematic verification flow, requirements tracking and coverage plays an indispensable role. Generally, this starts from requirements specification, where individual requirements are broken down into features, implementations, verification goals and metrics. In order to achieve these goals, verification engineers are taking different approaches, like writing testbenches for simulation environment or properties for assertion- basedformalverification. For each approach taken, to keep track of what requirements have been met users are generating coverage databases from simulation and formal environments. Because these are coming from different vendors, the big challenge is how can these coverage databases can be merged into one and to annotate the results into existing verification plans.
OneSpin® 360 EC-FPGA™ Tool Qualification Kit
OneSpin® 360 EC-FPGA™ is an automatic sequential equivalence checker that prevents field programmable gate array (FPGA) design flows from introducing synthesis, place-and-route and other implementation errors. Safety standards require rigorous verification before production to minimize the risk of failures in the field. With the most advanced formal technology, EC-FPGA detects corner-case design flow bugs with a process that is orders of magnitude more efficient and rigorous than gate-level simulation. With this TÜV-SÜD certified Tool Qualification Kit (TQK), users can deploy EC-FPGA seamlessly in their safety-critical flow to achieve a new level of productivity and standard compliance, without additional qualification effort.
OneSpin® 360 EC-FPGA™
The OneSpin 360 EC-FPGATM solution ensures that advanced FPGA synthesis optimizations, used to achieve competitive functionality, performance, power consumption, and cost targets, do not introduce synthesis and optimization errors. It eliminates gate-level simulation and finds corner-case design flow bugs. It supports all sequential synthesis optimizations including complex sequential retiming. 360 EC is in use at multiple companies, as an accuracy gold standard to test their design solutions.
OneSpin® 360 Fault Injection App™
OneSpin’s Fault Injection App (FIA) automates the definition and handling of fault injection scenarios, removing the need for ad hoc verification flows or environments, thereby cutting on engineering effort and promoting reusability across projects and teams.
OneSpin® 360 Fault Propagation App™
OneSpin’s Fault Propagation Analysis (FPA) App automatically identifies non-propagatable faults, allowing their safe elimination prior to pre and post simulation, thereby cutting on simulation and debug time while increasing the nominal fault coverage. This App utilizes dedicated formal algorithms and has two highly automated modes requiring minimal user intervention: fast mode and deep mode. The FPA App in fast mode analyzes the whole fault population of large designs to find the majority of safe faults, as illustrated in Figure below.
OneSpin® 360 DV-Quantify™
OneSpin’s Quantify measures the quality of a formal verification test bench. It provides precise, actionable information on what parts of the design-under-test (DUT) are verified, and it highlights RTL code that could still hide bugs. Additionally, Quantify reveals potential issues in the test bench that might corrupt metrics and give a false sense of confidence.
OneSpin® 360 SystemC/C++ Extension™
High-Level Synthesis (HLS) transforms algorithmic and potentially untimed design models often written in SystemC and C++ to fully timed Register Transfer Level (RTL) design blocks. The primary verification requirement is to allow thorough verification of algorithmic code prior to synthesis, in order to ensure that the abstract algorithm implementation is tested and fully optimized against the original specification, as well as avoiding long debug cycles.