Synthesis of synchronous assertions with guarded atomic actions

The SystemVerilog standard introduces SystemVerilog Assertions (SVA), a synchronous assertion package based on the temporal-logic semantics of PSL. Traditionally assertions are checked in software simulation. We introduce a method for synthesizing SVA directly into hardware modules in Bluespec SystemVerilog. This opens up new possibilities for FPGA-accelerated testbenches, hardware/software co-emulation, dynamic verification and fault-tolerance. We describe adding synthesizable assertions to a cache controller, and investigate their hardware cost.

• Type: Conference
• Year: 2005
• Where: MEMOCODE
• Authors: Michael Pellauer, Mieszko Lis, Don Baltus, Rishiyur S. Nikhil
• Keywords: Bluespec SystemVerilog, MEMOCODE 2005, Synchronous Assertion Package, SystemVerilog Assertions