User guide

20-57
Using OpenVera Assertions
• You cannot mix a template instantiation and unit instantiation
within the same OVA pragma using the multi-line C++ and
modified C++ pragma specification formats. You can, however,
specify a template instantiation and a unit instantiation using
separate single-line C pragmas.
The following example demonstrates how to implement template
instantiation using the template-based checker library:
The example calls the check_bool template from the OVA checker
library. Note that the default clock, (// ova clock posedge clk;),
must be a local signal, and can be boolean expression. It works only
for the "check_bool" and "forbid_bool" templates, and does not
work with other templates.
module test();
reg [3:0] x;
reg [3:0] y;
reg clk;
wire a,b;
wire error;
wire req,ack;
// some verilog code
// ova clock posedge clk;
// ova check_bool(!req || ack,,negedge clk);
/* ova for (i=0;i<4;i=i+1) {
check_bool(x[i]==past(y[3-i]) );
}
*/
// ova_begin
// clock negedge clk;
// forbid_bool u1 // instance name
// (error, // signal to check
// "ERROR_ASSERTED"); // message to display upon failure
// ova_end
// more verilog code
endmodule // module test
Default clock specification
Uses implicit clock
expression picked up from
default clock space
Default clock specification
Uses default clock
(negedge clock)