- If signal “a” is high on a given positive clock edge, then within 1 to 4 clock cycles, the signal “b” should be high.
property p1 @(posedge clk)
a |-> ##[1:4]b;
endproperty
a1: assert property(p1)
2. If signal “a” is high on a given positive clock edge, then signal “b” will be high eventually starting from the next clock cycle.
property p2 @(posedge clk)
a |=> ##1 b;
endproperty
a2: assert property(p2)
3. If the signal “a” is high on given posedge of clock, then signal “b” should be high for 3 clock cycles followed by “c” should be high after ”b” is high for third time.
property p4 @(posedge clk)
a|-> ##1 b[->3] ##1 c;
endproperty
a4: assert property(p4)
4. Write an assertion checker to make sure that an output signal never goes X.
property p1;
@(posedge clk)
!$isinknown(output_signal);
endproperty
a1: assert property (p1)
else $error("assertion got failed")
5. When signal_a is asserted, signal_b must be asserted, and must remain up until one of the signals signal_c or signal_d is asserted.
property p1;
@(posedge clk) disable iff (rst)
sig_a |-> sig_b throughout (!sig_c && !sig_d);
endproperty
a1: assert property (p1)
else $error("assertion got failed");
6. write a assertion to verify dut clock frequency of 10ns.
module tb;
time pre_time;
property p1;
@(posedge clk) disable iff(rst)
$rose(clk) |-> (($time - pre_time)== 10);
endproperty
assert property(p1)
else $error("clk period is not 10ns");
always @(posedge clk or posedge rst) begin
if (rst)
pre_time <= 0;
else
pre_time <= $time;
end
endmodule
7. When req is high , grant should be asserted within 2 to 20 clk cycles until request should be high. In the next clk cycle, req should be low.
sequence s1;
req |-> ##[2:20] grant throughout req;
endsequence
sequence s2;
s1 |=> !req;
endsequence
property p1;
@(posedge clk) disable iff(rst)
s1 |-> s2;
endproperty
a1: assert property(p1)
else $error("assertion got failed");
8. Write a SV assertion that monitors for an ack. If the ack is not received within 500clks, it issue an error.
property p1;
@(posedge clk) disable iff(rst)
(!ack) |=> ##[0:499]ack;
endproperty
a1: assert property(p1)
else $error("Error:ACK not received within 500 clock cycles!");