Prospect™ is a Security Property verification environment developed for the Sentinel™ security language. The system accepts an HDL (Verilog or VHDL) design file and a set of Sentinel properties provided by Tortuga Logic, which it uses to create a Security Model Design and generate System Verilog Assertions (SVA) bound to the Security Model Design. The Prospect software then leverages commercial formal verification engines to prove or disprove the security properties written in Sentinel on its generated Security Model Design. The Prospect software ships with OneSpin Solutions Design Verify™ engine and properties are proved using their robust formal technology. If the Prospect software identifies an information flow (property failing) then information is presented in terms of debug waveforms, RTL annotation, and information leakage “hot-spots.” More details on the features and benefits of Prospect can be found below.

ProductAndTechArchitecture-HSA-cropped-825.png

Below are the major features and benefits of Prospect:

FEATURE

BENEFITS

Supports Verilog/VHDL/System Verilog and Netlists

Users can load in their existing design files. Provides netlist support for addressing security issues that come up late in the design lifecycle.

Optimization capabilities in terms of module "black-boxing" and refactoring of the Security Model Design based on Security Properties

Black boxing capabilities improve analysis of large designs. Optimizations of its Security Model Design provide quick convergence of security properties. This avoids the common issues of convergence with existing formal verification techniques.

Security Property Pass/Fail results with Debug feedback about vulnerabilities

Shows user where vulnerabilities in RTL are occurring. In case of an information flow, debug information is presented as Waveforms, RTL Annotation, and "Hot-spot" analysis (RTL locations leaking most information).

Expressive Security Property language

Sentinel allows for easily specifying complex security properties. Tortuga Logic's Sentinel is adapted based on hardware security market need and introduces new features catered directly towards hardware security architect's requirements.