Being able to understand and to write assertions is now a must in the Industry. Pierre has been working with assertions for the last 3 years. He has used assertions for both dynamic (using simulation) and static verification (using formal analysis).

• He has written assertions at the same time as he designed some modules (inside the RTL code). This approach was useful to verify properly some non trivial functions inside his code, which would be difficult to verify outside his block. As an added benefit, it also provided a clear description of the design intent for these particular functions. Furthermore, some of the interface requirements were also described with assertions inside the RTL code.
• He has written assertions to verify other designer’s module (outside the RTL, in a vunit file). These assertions were intended to verify various modules at the block level but provided the added benefit for the verification of these modules at the top level.
• He also wrote assertions and assumptions which were developed for Formal Analysis. The assertions were written so they can be used for dynamic test, as well.

The assertion language which was used by Pierre is PSL but he has also taken, recently, a training course with System Verilog, which is similar to PSL.