Assertions - Examples

Assertions - Examples

Example for Assertions.
(a) Ethernet

(i) Example Immediate Assertion

module assert_immediate;
logic Rx_data_valid;
logic clk,reset;
always_ff @(posedge clk or posedge reset)
begin
if (Rx_data_valid)
begin
CHECK_RESET_WHEN_RX_DATA_VALID: assert (reset && Rx_data_valid) //checking assert condition
begin
$display(" Collect the bits from frame");
end
else
begin
$error("assert failed at time %0t",$time);
$display("the frame is truncated");
end
end
end

initial
begin
$monitor("Rx_data_valid = %0d clk = %d reset = %d",Rx_data_valid,clk,reset);
reset = 0;
Rx_data_valid = 0;
#6 Rx_data_valid = 1;
#8 Rx_data_valid = 0;
#7 reset = 1;
end
initial
begin
$display("Rx_data_valid = %0d clk = %d reset = %d",Rx_data_valid,clk,reset);
#50 $finish;
end
initial
begin
clk = 0;
forever
begin
#10;
clk = ~clk;
end
end
endmodule

Output in VCS

Rx_data_valid = 0 clk = x reset = 0
Rx_data_valid = 0 clk = 0 reset = 0
Rx_data_valid = 1 clk = 0 reset = 0
"assert_imm.sv", 9: assert_immeadiate.CHECK_RESET_WHEN_RX_DATA_VALID: started at 10s failed at 10s
Offending '(reset && Rx_data_valid)'
Error: "assert_imm.sv", 9: assert_immeadiate.CHECK_RESET_WHEN_RX_DATA_VALID: at time 10
assert failed at time 10
the frame is truncated
Rx_data_valid = 1 clk = 1 reset = 0
Rx_data_valid = 0 clk = 1 reset = 0
Rx_data_valid = 0 clk = 0 reset = 0
Rx_data_valid = 0 clk = 0 reset = 1
Rx_data_valid = 0 clk = 1 reset = 1
Rx_data_valid = 0 clk = 0 reset = 1
(ii) Example Sequential Assertion

module asser_seq;
int da,sa,en; // destination address , source address
int frame;
int reset;
logic clk;
always @(posedge clk or negedge reset)
begin
if(en)
begin
if(frame>64) || (frame<511))
begin
$display("Normal frame is transmitted without extension",frame);
end
else
$display("Normal frame transmitted with extention",frame);
end
end

property frame_transmit; //Transmit the frame using property
@(posedge clk)
en |-> frame;
endproperty

frame_transmit_assert: assert property (frame_transmit) //assert condition
else
$display("@ %0d assertion filed",$time);
initial
begin
en = 0;
reset = 0;
#15 en = 1;
#10 reset = 1;
#5 reset = 1;
#3 en = 1;
end
initial
begin
clk = 0;
forever
begin
#5 clk++;
end
end
initial
begin
$display(" %d %d %d %d ", en,reset,frame,clk,$time);
#100 $finish;
end
endmodule

Output in VCS

0 0 0 0 0
Normal frame is transmitted without extension 0
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 25s failed at 25s
Offending 'frame'
@ 25 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 35s failed at 35s
Offending 'frame'
@ 35 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 45s failed at 45s
Offending 'frame'
@ 45 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 55s failed at 55s
Offending 'frame'
@ 55 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 65s failed at 65s
Offending 'frame'
@ 65 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 75s failed at 75s
Offending 'frame'
@ 75 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 85s failed at 85s
Offending 'frame'
@ 85 assertion filed
Normal frame is transmitted without extension 0
"assert_seq.sv", 24: asser_seq.frame_transmit_assert: started at 95s failed at 95s
Offending 'frame'
@ 95 assertion filed
$finish at simulation time 100



(b) Sonet

(i) Example immediate assertion

module assert_on_FP();
bit clk;
bit frame_pulse;
reg [7:0]section_A1;
reg [7:0]section_A2;
bit [7:0]sonet_data_in;
bit A1A2_indicator;
initial
begin
clk = 0;
frame_pulse = 0;
sonet_data_in = 8'b0;
sonet_data_in = 8'b0;
#5 sonet_data_in = 'hf6;
#1 sonet_data_in = 'h28;
#1 A1A2_indicator= 1'b1;
#1 frame_pulse = 1'b1;
#1 sonet_data_in = 'h56;
#4 A1A2_indicator= 1'b0;
#4 frame_pulse = 1'b0;
#1 sonet_data_in = 'h99;
#1 sonet_data_in = 'h88;
#5sonet_data_in = 'hf6;
#1 sonet_data_in = 'h28;
#1 A1A2_indicator= 1'b1;
#1 frame_pulse = 1'b1;
#1 sonet_data_in = 'h56;
#4 A1A2_indicator= 1'b0;
#4 frame_pulse = 1'b0;
#1 sonet_data_in = 'h100;
#1 sonet_data_in = 'h28;
#5 sonet_data_in = 'hf6;
#1 sonet_data_in = 'h28;
#1 A1A2_indicator= 1'b1;
#1 frame_pulse = 1'b1;
#1 sonet_data_in = 'h56;
#4 A1A2_indicator= 1'b0;
#4frame_pulse = 1'b0;
#1 sonet_data_in = 'h44;
#1 sonet_data_in = 'h33;
#100 $finish;
end
always #1 clk = ~clk;

// Assertion used in always block
always @ (posedge clk)
begin
if(A1A2_indicator==1'b1)
CHECK_IF_FRAME_PULSE_IS_HIGH : assert (frame_pulse== 1'b1)
begin
$display ( "Assert Passed at time %0t",$time);
end
else
begin
$error( "assert failed at time %0t", $time);
end
end
endmodule

Output in VCS

"immd_assert.sv", 50: assert_on_FP.CHECK_IF_FRAME_PULSE_IS_HIGH: started at 7s failed at 7s
Offending '(frame_pulse == 1'b1)'
Error: "immd_assert.sv", 50: assert_on_FP.CHECK_IF_FRAME_PULSE_IS_HIGH: at time 7
assert failed at time 7
Assert Passed at time 9
Assert Passed at time 11
Assert Passed at time 27
Assert Passed at time 29
Assert Passed at time 31
"immd_assert.sv", 50: assert_on_FP.CHECK_IF_FRAME_PULSE_IS_HIGH: started at 45s failed at 45s
Offending '(frame_pulse == 1'b1)'
Error: "immd_assert.sv", 50: assert_on_FP.CHECK_IF_FRAME_PULSE_IS_HIGH: at time 45
assert failed at time 45
Assert Passed at time 47
Assert Passed at time 49

(ii) Example Concurrent Assertion

module assert_on_FP();
bit clk;
bit frame_pulse;
reg [7:0]section_A1;
reg [7:0]section_A2;
bit [7:0]sonet_data_in;
bit A1A2_indicator;
initial
begin
clk = 0;
frame_pulse = 0;
sonet_data_in = 8'b0;
sonet_data_in = 8'b0;
#1 A1A2_indicator= 1'b1;
#1 frame_pulse = 1'b1;
#1 sonet_data_in = 'h56;
#1 sonet_data_in = 'h28;
#1 sonet_data_in = 'h38;
#3 A1A2_indicator= 1'b0;
#4 frame_pulse = 1'b0;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#3 A1A2_indicator= 1'b1;
#1 frame_pulse = 1'b1;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#4 A1A2_indicator= 1'b0;
#4 frame_pulse = 1'b0;
#1 sonet_data_in = 'h100;
#1 sonet_data_in = 'h28;
#5 sonet_data_in = 'hf6;
#1 sonet_data_in = 'h28;
#1 A1A2_indicator= 1'b1;
#1 frame_pulse = 1'b1;
#1 sonet_data_in = 'h56;
#1 sonet_data_in = 'h86;
#1 sonet_data_in = 'h96;
#4 A1A2_indicator= 1'b0;
#4 frame_pulse = 1'b0;
#1 sonet_data_in = 'h00;
#1 sonet_data_in = 'h00;
#100 $finish;
end
always #1 clk = ~clk;
// Sequences with different operators
sequence A1A2indic_framepulse;
A1A2_indicator ##1 frame_pulse;
endsequence

sequence framepulse_sonet_data_in;
frame_pulse ##[2:5] sonet_data_in;
endsequence
//Property Layer
property seq_of_seq;
@(posedge clk)
A1A2indic_framepulse |-> framepulse_sonet_data_in;
endproperty
//Assertion Directive Layer
check_property: assert property(seq_of_seq);
endmodule

Output in VCS

"conc_assert.sv", 70: assert_on_FP.check_property: started at 21s failed at 33s
Offending 'sonet_data_in'
"conc_assert.sv", 70: assert_on_FP.check_property: started at 23s failed at 35s
Offending 'sonet_data_in'
"conc_assert.sv", 70: assert_on_FP.check_property: started at 51s failed at 63s
Offending 'sonet_data_in'