does UVM support assertion

[chenyong]

Hi,

Does UVM support assertion? I found the assertions with sequence, such as "a |=> b" could only works in interface. When I write assertions within driver/monitor, there are always syntax errors. thanks

[steve]

Hi,

SystemVerilog "concurrent" assertions can't live inside classes (uvm_component, uvm_driver, etc..) as they are declarative statements that exist for the lifetime of a simulation, whereas classes are dynamic in nature. They belong in the world of modules and interfaces.

You can, however use "immediate" assertions in your uvm code when you do procedural checking, e.g. in a scoreboard:

chk_scbd_match: assert (item.data == scbd.data) ...

which gives the added benefit of vplan traceability and assertion coverage.

Regards,

Steve

[chenyong]

thanks Steve. do you think there will be an opportunity with other techniques to "fit" "concurrent" assertions in the UVM in the future?

[dave_59]

Technically, most UVM scoreboards are already a concurrent assertion. It's just a matter of which SystemVerilog syntax is used to model it.

The concurrent assertions section of SystemVerilog is designed to merge formal tools with dynamic simulation, and that requires some level of underlying synthesis technology. So until SystemVerilog synthesis technology comes into the 21st century and starts synthesizing classes, you are not going to see concurrent assertions in classes.

[chenyong]

thanks for your kind reply.

[aji.cvc]

Hi Dave,

Technically, most UVM scoreboards are already a concurrent assertion. It's just a matter of which SystemVerilog syntax is used to model it.

The concurrent assertions section of SystemVerilog is designed to merge formal tools with dynamic simulation, and that requires some level of underlying synthesis technology. So until SystemVerilog synthesis technology comes into the 21st century and starts synthesizing classes, you are not going to see concurrent assertions in classes.

While the origin of concurrent SVA is from formal, why not let it grow beyond? We hear of this compliant from every training class we held, i.e. from lots of real users. Technically speaking - this is very much do-able inside a simulator/dynamic engine. A long standing proof is Specman with its E (IEEE 1647) having supported such construct (known as TE - Temporal Expressions) for over 10 years now. E has no formal verif origin.

We from CVC have been trying to bring this to SV-AC without much success - we believe real users need to "shout" for it to being considered.

BTW - recently (2009) added SVA "checker" construct could provide a way/entry for this. There are/were discussions allowing "checker" inside classes - but temporal was disallowed, this could be further extended IMHO.

Warm Regards

Ajeetha, CVC

www.cvcblr.com/blog