DVCon speaker compares assertion languages

"The obvious and pragmatic answer is that there are two standard languages because there are two committees," Havlicek said. However, he noted that the two committees had complementary goals, resulting in two languages that address complementary engineering needs.

PSL arose from Accellera's Formal Verification Technical Committee (FVTC), which began in 2000. That group considered several property languages and chose IBM's Sugar language as its base. The result was PSL, which was donated to the IEEE last year and is now undergoing standardization as IEEE P1850.

SVA, on the other hand, came from Accellera's SVA Committee, which absorbed technology not considered or rejected by FVTC — including the Superlog language, Motorola's CBV, Synopsys' OpenVera, and Intel's ForSpec. The resulting assertions are included in the SystemVerilog language that is now undergoing standardization as IEEE P1800.

PSL, Havlicek said, was intended as a "comprehensive property language for static verification, with a subset suitable for dynamic verification." SVA, in contrast, is a "rich property language for dynamic verification with a subset suitable for static verification."

Further, PSL is an extensible language framework designed to work with multiple HDLs, while SVA is comprised of assertions integrated directly into Verilog, so that hardware designers can include in-line assertions with their HDL code.

Because of the divergence, Havlicek noted, "there was a call by a number of people to align the languages." As a result of work at Accellera, he said, there is now full alignment on the formal semantics and partial alignment on the syntax. In the process, he noted, "we found bugs in both languages."

What's possible today, Havlicek said, is a mapping of "reduced" SystemVerilog concurrent assertions into the PSL foundation language. That means the SystemVerilog concurrent assertions would have to leave out local variables and recursive properties, which are not used by PSL, and would have to specify clocks explicitly, similar to PSL clock operations.

The result is something close enough for automatic translation. As Havlicek said, it will "look more like dialects of the same language."

Havlicek noted, however, that PSL has an optional branching extension that does not correspond to anything in SystemVerilog, and that SVA includes "immediate" assertions that do not map to anything in PSL.

"I can easily see someone using both of these languages," Havlicek said. "But for the vast majority of practical properties, you could write in either one."