Procedural Concurrent Assertions - SVA: The Power of Assertions in SystemVerilog - page 327

Exercises

14.1. Add some procedural assertions to represent your understanding of the intent
of following code examples.

1.

module m #(W=8, D=32) (
input logic clk,
input logic [W-1:0] d_in,
output logic [W-1:0] d_out

);

logic [D * W-1:0] sh;
assign d_out = sh[D * W-1:(D-1) * W];
always @( posedge clk) begin
sh <= {sh[(D-1) * W-1:0], d_in};

end
endmodule :m

2.

typedef logic [31:0] natT;
module m(
input logic clk, rst_n, load, incr,
input natT a_in, b_in,
output natT d_out

);

natT a, b;
assign d_out = a;
always @( posedge clk or negedge rst_n) begin
if (!rst_n) begin
a<=0;
b<=0;
end else if (load) begin
a <= a_in;
b <= b_in;
end else if (incr) begin
a<=a+b;
b<=a;

end

end
endmodule :m

14.2. For each of the following procedures, determine whether or not a clock is
inferred. If so, give the inferred clock. If not, explain why not. Assume the following
declarations throughout:

logic clk, en, rst_n;
logic [7:0] a, b, d_in;
event ev;
clocking CLK @( posedge clk); endclocking

1.

always @( edge clk) begin
a <= d_in;
A_STABLE: assert (a != d_in)