Assertions:
1.After req, grant comes within 3 to 5 clock cycles…
Solve above using $past
module abc;
bit req,gnt,clk=1'b0;
initial begin
forever #5 clk=~clk;
end
property p1;
//same cycle
@(posedge clk) req |-> ##1 (gnt[*3:5]) ##1 gnt==$past(gnt,1);
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
//repeat(100)
for(int i=0;i<100;i++)
begin
req=$random;
//gnt=$random;
gnt=i;
assert property (p1)
$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);
#5;
end
#100 $finish;
end
endmodule
2.If signal "a" is high on a given positive clock edge, then signal "b" should
also be high on the same clock edge.
module abc;
bit a,b,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) a |-> b;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
assert property(p1)
$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);
#5;
end
#100 $finish;
end
endmodule
3.If signal "a" is high on a given positive clock edge, then signal "b" should be
high on the next clock edge.
// Code your testbench here
// or browse Examples
module abc;
bit a,b,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) a |=> b;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
assert property(p1)
$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);
#5;
end
#100 $finish;
end
endmodule
4.If signal "a" is high in a given positive clock edge, then signal "b" should be
high after 2 clock cycles.
module abc;
bit a,b,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) a |=>##1 b;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
assert property(p1)
$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);
#5;
end
#100 $finish;
end
endmodule
5.If the boolean expression "a && b" is true on any given positive edge of the
clock. If it is true, then within 1 to 3 clock cycles, the signal "c" should be
high.
module abc;
bit a,b,c,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) a && b |-> ##1 (c[*1:3]);
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
c=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
6.On a given positive edge of clock, signal "a" is high. If so, then signal "b"
will be high eventually starting from the next clock cycle and after that, signal
"c" will be high eventually starting at the same clock cycle in which signal
"b" was high.
module abc;
bit a,b,c,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) a |=> b |-> c;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
c=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
7.If signal "c" is high then the value of signal "d" is equal to the value of
signal "a." If signal "c" is not detected high, then the value of signal "d" is
equal to the value of signal "b." This is a combinational check and is
performed on every positive edge of clock.
module abc;
bit a,b,c,d,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) if(c)
(d==a)
else
(d==b);
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
c=$random;
d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
8.Two clock cycles after a valid start, signal "a" stays high for 3 continuous
clock cycles and two clock cycles after that, signal "stop" is high. One clock
cycle later signal "stop" is low.
module abc;
bit a,start,stop,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) start |=>##1 ##1 a[*3] |=> ##1 stop |=>(!stop);
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
start=$random;
stop=$random;
// d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
9.Two clock cycles after a valid start, sequence (a ##2 b) repeats 3 times and
two clock cycles after that, signal "stop" is high.
module abc;
bit a,b,start,stop,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
sequence s;
a ##2 b;
endsequence
property p1;
@(posedge clk) start |=> ##1 ##1 s[*3] ##1 ##1 stop;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
start=$random;
stop=$random;
// d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
10.Two clock cycles after a valid start, sequence (a ## [1:4] b) repeats 3 times
and two clock cycles after that, signal "stop" is high.
module abc;
bit a,b,start,stop,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
sequence s;
a ## [1:4] b;
endsequence
property p1;
@(posedge clk) start |=> ##1 ##1 s[*3] ##1 ##1 stop;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
b=$random;
start=$random;
stop=$random;
// d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
11.Two cycles after a valid start signal, the signal "a" will stay high repeatedly
until a valid stop arrives.
module abc;
bit a,start,stop,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) disable iff(stop)
start ##1 ##1 ##1 ##1 a[*0:$];
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
start=$random;
stop=$random;
// d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
12.If there is a valid start signal on any given positive edge of the clock, 2
clock cycles later, signal "a" will repeat three times continuously or
intermittently before there is a valid stop signal.
module abc;
bit a,start,stop,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) start ##1 ##1 ##1 a[->3] ##1 stop;//go-to
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
start=$random;
stop=$random;
// d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
13.If there is a valid start signal on any given positive edge of the clock, 2
clock cycles later, signal "a" will repeat three times continuously or
intermittently before there is a valid stop signal. One clock cycle later, the
signal "stop" should be detected
module abc;
bit a,start,stop,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) start ##1 ##1 ##1 a[->3] ##1 stop ##1 stop;
//go-to
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
start=$random;
stop=$random;
// d=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
14.Write an assertion for: As long as sig_a is still up,sig_b should not be
asserted.
module abc;
bit sig_a,sig_b,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) if(sig_a)
sig_a == !sig_b;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
sig_a=$random;
sig_b=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
15.Write an assertion for,The signal sig_a is a pulse: It can only be asserted
for one cycle, and must be deasserted in the next cycle.
module abc;
bit sig_a,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) $fell(sig_a);
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
sig_a=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
16.Write an assertion for, sig_a must not be asserted before the first
sig_b(may be asserted on the same cycle as sig_b).
module abc;
bit sig_a,sig_b,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
sequence s1;
##[0:1] sig_a;
endsequence:s1
sequence s2;
##[0:1] !sig_a;
endsequence:s2
property p1;
@(posedge clk) if(sig_b)
(s1 or s2)
else if(!sig_b)
sig_a == 0;
endproperty:p1
initial begin
$dumpfile("dumb.vcd");
$dumpvars(1);
end
initial
begin
repeat(100)
begin
sig_a=$random;
sig_b=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
17.Write an assertion for, after one of the signals req is asserted, ack must be
deasserted, and must stay down untill the next req.
module abc;
bit req,ack,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) req ##0 !ack throughout req;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
req=$random;
ack=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
18.Write an assertion for, req must not be asserted togeather with ack or with
resp.
module abc;
bit req,ack,resp,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) if(ack || resp)
req == 0;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
req=$random;
ack=$random;
resp=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
19.Write an assertion for, if sig_a is down, sig_b may only frise for one cycle
before the next time that sig_A is asserted.
module abc;
bit sig_a,sig_b,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) !sig_a ##0 $rose(sig_b) ##1 sig_a;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
sig_a=$random;
sig_b=$random;
//sig_A=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
20.Write an assertion for, if there are two occurences of sig_a rising with
STATE=active1, and no sig_b occure between them, then within 3 cycles of
the second rise of sig_a.
module abc;
bit sig_a,sig_b,active1,STATE,resp,clk=1'b1;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) disable iff(sig_b)
sig_a |-> (STATE==active1) ##3 sig_a;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
sig_a=$random;
sig_b=$random;
active1=$random;
STATE=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
21.property hr;
@(posedge clk) $fell(start) |->##2 (a[->3]) ##1 stop;
endproperty clk
ass: assert property(hr);
for above example, at which rising edge of the clock will be stop
signal low?
module abc;
bit clk=1'b1;
bit start,a,stop;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) $fell(start) |->##2 (a[->3]) ##1 stop;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
start=$random;
stop=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
22.sequence up;
@(posedge clk) c##7 b;
endsequence;
sequence down;
@(posedge clk) c##[*1:5] b;
endsequence;
property finish;
@(posedge clk) up intesect down;
endproperty
a: assert property(finish);
for above example, try to show the waveform representation.
module abc;
bit clk=1'b1;
bit b,c;
initial begin
forever #5 clk=~clk;
end
sequence up;
@(posedge clk) c ##7 b;
endsequence;
sequence down;
@(posedge clk) c ##1 (b[*1:5]);
endsequence;
property finish;
@(posedge clk) up intersect down;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
b=$random;
c=$random;
assert property(finish);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
23.Write an assertion which checks that once a valid request is asserted by the
master, the arbiter provides a grant within 2 to 5 clock cycles.
module abc;
bit clk=1'b1,request,grant;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) request ##[2:5] grant;
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
request=$random;
grant=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule
24.Write an assertion to make sure that the state variable in a state machine is
always one hot value.
module abc;
bit clk=1'b1;
bit [3:0] a;
initial begin
forever #5 clk=~clk;
end
property p1;
@(posedge clk) $onehot(a);
endproperty
initial begin
$dumpfile("dumb.vcd");
$dumpvars(abc);
end
initial
begin
repeat(100)
begin
a=$random;
assert property(p1);
/*$display("p1 passed time at t=%t \n",$time);
else
$display("p1 failed time at t=%t \n",$time);*/
#5;
end
#100 $finish;
end
endmodule