User guide

20-55
Using OpenVera Assertions
In the previous example, the bind statement (// ova bind
my_mutex(clk,{a,b});)
calls independent OVA code located
outside Verilog module. You can instantiate the independent OVA
code as many times as needed anywhere in the Verilog code. The
context of the OVA code within the Verilog code is automatically
inferred based upon the location of the bind statement.
module test();
reg [3:0] x;
wire clk;
wire a,b;
// ova bind my_mutex(clk,{a,b});
wire error;
// verilog code
endmodule // module test
/* ova
unit error_check (logic clk, logic error);
clock posedge clk {
event e1 : error == 1;
}
assert a1 : forbid(e1);
endunit
bind module test : error_check(clk,error) ;
unit my_mutex (logic clk, logic [1:0] x);
clock posedge clk {
event e1 : x != 2'b11;
}
assert a1 : check(e1);
endunit
*/
Two units are defined:
error_check and my_mutext
Binding from outside a module
Binding from inside a module