Assertion Statements - SVA: The Power of Assertions in SystemVerilog - page 73

1 module top;
2 bit sys_clk;
3 global clocking GCLK @( edge sys_clk);
4 endclocking
5 // code to animate sys_clk in simulation
6 ...
7 mod1 mod1_inst();
8 mod2 mod2_inst();
9 endmodule
10 module mod1();
11 logic a, b;
12 ...
13 m_check m_check_inst(a, b);
14 endmodule
15 module mod2();
16 logic x, y, clk;
17 global clocking @( posedge clk);
18 endclocking
19 ...
20 m_check m_check_inst(x, y);
21 module m_check( input logic a, b);
22

a_simple: assert property (@$global_clock a |=> b);

endmodule

23

Fig. 4.9 Global clocking declaration

Global Clocking

SystemVerilog provides the capability to specify a clocking event for the entire or
parts of the elaborated model as the primary system clock , called also global clock .
This is done with a global clocking declaration, which is a special form of clocking
block declaration. Its purpose is to provide relation to the primary system clock
used in formal verification and emulation. There can be several global clocking
specifications in the design affecting different parts of the design hierarchy, but at
any hierarchical level at most one of them is effective and can be referred to using
the $global_clock system function.
Figure 4.9 illustrates the syntax of a global clocking declaration. One global
clocking is specified in Line 3 within the module top . This declaration says that
the event edge sys_clk is the primary system clocking event for the underlying
hierarchy until another global clocking declaration is encountered (if any). Since
the model has a global clocking declaration, the system function $global_clock
may be used to reference the system clocking event. Such a reference appears in
Line 22 . In this model, module m_check is instantiated in mod1 and in mod2 .Inthe
instance mod1_inst $global_clock resolves to the global clocking in the nearest
parent module which is top and behaves the same way as the hierarchical reference
top.GCLK . However, in the instance mod2_inst , $global_clock resolves to the
hierarchically nearest specification in Line 17 within the module mod2 . It behaves