Writing assertions concurrently with the RTL design and keeping these assertions closely tied to the RTL code has been found to bring significant benefits in both the design and verification processes for digital hardware. The primary benefit is that assertions help to detect more functional bugs, detect them earlier in the process and detect them closer to their original cause. This leads in turn to fewer bugs remaining undetected into production, shorter verification timescales and faster debugging.
A secondary benefit is that the very act of formulating and writing assertions can give the designer a better understanding of the design, and hence uncover bugs in the specification or else avoid introducing bugs into the design in the first place. Once written, bound to the RTL code and proven, assertions play the role of formal comments. Unlike conventional comments, assertions are executable and continue to monitor the design for functional correctness long after they’ve ceased being the focus of attention.
Assertions bring the possibility of increased metrication to the verification process. Assertions directly increase observability of the state of the design during verification. By measuring and controlling the density of assertions and logging assertion passes as well as failures, it is possible to bring some science to the task of knowing when functional verification is complete.
Finally, the introduction of PSL as a standard property language provides a low cost, low risk way of bringing immediate benefits to the design and verification process, yet at the same time opens the door to the introduction of new verification tools such as static property checkers.
Next: Development of PSL/Sugar
