Checkers - SVA: The Power of Assertions in SystemVerilog - page 182

1 module m_seqprotocol #( parameter int bothedges = 0,
2 parameter type dataType = logic )
3 ( input logic start, complete, clk, reset,
4 dataType dataIn, dataOut);
5 if (bothedges) begin :L
6 default clocking dclk @clk; endclocking
7 end
8 else begin :L
9 default clocking dclk @( posedge clk); endclocking
10 end
11 default disable iff reset;
12
13 property match(x, y);
14 x |=> !x until_with y;
15 endproperty : match
16
17 var type (dataIn) last_dataIn;
18
19 always @L.dclk
20

if ($sampled(start))

last_dataIn <= $sampled(dataIn);

21

22
23 a_initial_no_complete:
24

assert property ($fell(reset) |-> !complete until_with start);

25
26 a_seq_data_check: assert property (
27 complete |-> dataOut == last_dataIn);
28 a_no_start: assert property (match(start, complete));
29 a_no_complete: assert property (match(complete, start));
30 endmodule : m_seqprotocol

Fig. 9.3 Sequential protocol specification as a module

￿ The module should explicitly take care of distinguishing between the single and
double edge clocking modes.

There are more drawbacks besides those illustrated in the sequential protocol
example:

￿ Modules cannot accept sequences and properties as their arguments (ports). This
ability is important for verification code, for example, when some external event
is defined as a sequence.
￿ Modules cannot be instantiated within procedural code, and therefore cannot be
used for checking correctness of the data within procedural flow.
￿ Modules cannot infer the clocking event and reset from their instantiation context.
This makes their instantiation more verbose than necessary.