Assertions and cover directives specify and validate the expected behavior of a design. They are written directly in the source code to observe signal values over a period of time.
Assertions declare that something must always hold (assertion failure implies a bug in design)
Cover directives declare that something should occur (cover success measures coverage)
The PSL cover directives and SystemVerilog cover statements are forms of Functional Coverage. Specification of properties and their use in assertions and functional coverage is the essential element of designing modern systems and their verification algorithms. Aldec Simulators support three popular languages serving this purpose:
Property Specification Language (PSL)
PSL is the most thorough, yet easy to learn property language. To help it coexist with other languages, it comes in flavors that blend nicely with VHDL, Verilog, SystemVerilog or SystemC code. The Simple Subset of PSL (section of the language guaranteed to simulate) was even incorporated in the most recent version of VHDL standard (IEEE Std 1076™-2008). The feature of PSL most interesting for current VHDL or Verilog users is its ability to be placed both in the separate verification units managed by a Verification Engineer and directly in the HDL code managed by a Design Engineer.
OpenVera Assertions (OVA)
OVA blends better with Verilog code than with VHDL code, although it can be used with both. OpenVera was donated to the Accellera group working on SystemVerilog, leading to many similarities between OpenVera Assertions and SystemVerilog Assertions.
SystemVerilog Assertions (SVA)
SVA is a part of SystemVerilog and blends well with Verilog code, both at the module binding level and in the behavioral code. Verification modules written in SVA can also be bound to VHDL components in the mixed-language simulator environment.
Assertions Bundle is shipped by default in the high-end configurations of Aldec Simulators. Once the bundle is available, all the related graphical tools become available as well: all assertions defined in the design can be displayed in dedicated Assertion Viewer that allows changing properties of individual assertions, setting assertion breakpoints, and adding assertions to other debugging tools such as Waveform Viewer or Advanced Dataflow that provide powerful debugging features.