Guest
Hi All,
I am currently learning assertion based verification using Accellera
supplied OVL libraries. I am having some problems in verifying the
usage/functionality of the 'assert_width' assertion. Here is a small
sample program which I have written to evaluate how this particular
assertion would/should work. It is a simple 4 bit counter written using
behavioural statements in Verilog and it is purposely made to reset
just when the count reaches 10.
===========================
/*
Example showing the use of assert_width assertion.
Dependencies: The OVL assertion library file assert_width.vlib must be
in the same directory as the source code, since it's absolute path is
hardcoded.
Assertion Description:
This assertion is supposed to ensure that when the value of a specified
expression is TRUE, it remains TRUE for a specified MIN no. of clks and
transitions from TRUE not later than a specified MAX no of clks. The
expression in this case is the counter output bit q[2] going to 1.
Program Description:
The example program is a 4 bit counter written using behavioural
statements.
The assertion checks that the specified expression (q[2] = 1), once
high, remains high for min 1 clk and max 6 clks.
If these MIN and MAX timing limits are not met, then an error is to be
displayed.
*/
/*---- Defines and Includes ----*/
`define OVL_ASSERT_ON
`define OVL_INIT_MSG
`include "assert_width.vlib"
/*--- Module Definition ----------*/
module ctr_4_bit (q, clk, clear);
output [3:0] q;
input clk, clear;
reg [3:0] q;
always @ (negedge clear or posedge clk) //uses negative reset logic
(ckt reset when reset = 0).
begin
if (clear == 0) q <= 4'd0;
else q <= q + 1;
end
endmodule
/*--- Stimulus Block -----*/
module top;
reg clk, reset;
wire [3:0] q;
ctr_4_bit st (q, clk, reset);
initial
clk = 1'b1;
always
#1 clk = ~clk; //toggle clk every 1 time unit
initial
begin
reset = 1'b0; //reset high initially - see waveforms
#2 reset = 1'b1; //reset goes low after 2 time units
#20 reset = 1'b0; //reset goes high again 20 time units
#2 $finish; //end simulation after these many nsecs. To go
indefinitely, comment this line
end
/*---- SHM Dump Block ------*/
initial
begin
$shm_open ("assert_width_example.shm");
$shm_probe ("as");
end
/*----- Assertion Block -----*/
assert_width #(
`OVL_ERROR,
1, //min clks for which test expr must remain true, once it is sampled
true
8, //once it is sampled true, test expr shud NOT remain true more than
this (MAX clks)
`OVL_ASSERT, //MAX value = 8 as specfd here should make the assertion
fail. But it's not failing.
"Error",
`OVL_COVER_ALL)
check (
clk == 1, //clk should always be true for checking
q[2] == 1'b1); //once q[2] becomes 1 (which may happen ANYTIME), it
shud satisfy the MIN and MAX clk durations while it is still true
endmodule
/*---- End ------*/
The description of 'assert_width' says that *whenever* the expression
evaluates to TRUE, it should remain TRUE for a duration >= MIN clks and
<= MAX clks. I have specified MIN clks = 1 and MAX clks = 8 as in the
code above. The MAX value should make the assertion fail (which is
evident from the output timing diagram), but all I get on the output
screen is this:
OVL_NOTE: V1.6: ASSERT_WIDTH initialized @ top.check.ovl_init_msg_t
Severity: 1, Message: Error
Simulation complete via $finish(1) at time 24 NS + 0
../assert_width_example.v:46 #2 $finish; //end
simulation after these many nsecs. To go indefinitely, comment this
line
ncsim> exit
I have tried all options to fire the assertion, but it's not happening.
I want to know what is keeping the assertion from getting fired. Any
help towards this will be greatly appreciated.
Best regards,
Amit.
I am currently learning assertion based verification using Accellera
supplied OVL libraries. I am having some problems in verifying the
usage/functionality of the 'assert_width' assertion. Here is a small
sample program which I have written to evaluate how this particular
assertion would/should work. It is a simple 4 bit counter written using
behavioural statements in Verilog and it is purposely made to reset
just when the count reaches 10.
===========================
/*
Example showing the use of assert_width assertion.
Dependencies: The OVL assertion library file assert_width.vlib must be
in the same directory as the source code, since it's absolute path is
hardcoded.
Assertion Description:
This assertion is supposed to ensure that when the value of a specified
expression is TRUE, it remains TRUE for a specified MIN no. of clks and
transitions from TRUE not later than a specified MAX no of clks. The
expression in this case is the counter output bit q[2] going to 1.
Program Description:
The example program is a 4 bit counter written using behavioural
statements.
The assertion checks that the specified expression (q[2] = 1), once
high, remains high for min 1 clk and max 6 clks.
If these MIN and MAX timing limits are not met, then an error is to be
displayed.
*/
/*---- Defines and Includes ----*/
`define OVL_ASSERT_ON
`define OVL_INIT_MSG
`include "assert_width.vlib"
/*--- Module Definition ----------*/
module ctr_4_bit (q, clk, clear);
output [3:0] q;
input clk, clear;
reg [3:0] q;
always @ (negedge clear or posedge clk) //uses negative reset logic
(ckt reset when reset = 0).
begin
if (clear == 0) q <= 4'd0;
else q <= q + 1;
end
endmodule
/*--- Stimulus Block -----*/
module top;
reg clk, reset;
wire [3:0] q;
ctr_4_bit st (q, clk, reset);
initial
clk = 1'b1;
always
#1 clk = ~clk; //toggle clk every 1 time unit
initial
begin
reset = 1'b0; //reset high initially - see waveforms
#2 reset = 1'b1; //reset goes low after 2 time units
#20 reset = 1'b0; //reset goes high again 20 time units
#2 $finish; //end simulation after these many nsecs. To go
indefinitely, comment this line
end
/*---- SHM Dump Block ------*/
initial
begin
$shm_open ("assert_width_example.shm");
$shm_probe ("as");
end
/*----- Assertion Block -----*/
assert_width #(
`OVL_ERROR,
1, //min clks for which test expr must remain true, once it is sampled
true
8, //once it is sampled true, test expr shud NOT remain true more than
this (MAX clks)
`OVL_ASSERT, //MAX value = 8 as specfd here should make the assertion
fail. But it's not failing.
"Error",
`OVL_COVER_ALL)
check (
clk == 1, //clk should always be true for checking
q[2] == 1'b1); //once q[2] becomes 1 (which may happen ANYTIME), it
shud satisfy the MIN and MAX clk durations while it is still true
endmodule
/*---- End ------*/
The description of 'assert_width' says that *whenever* the expression
evaluates to TRUE, it should remain TRUE for a duration >= MIN clks and
<= MAX clks. I have specified MIN clks = 1 and MAX clks = 8 as in the
code above. The MAX value should make the assertion fail (which is
evident from the output timing diagram), but all I get on the output
screen is this:
OVL_NOTE: V1.6: ASSERT_WIDTH initialized @ top.check.ovl_init_msg_t
Severity: 1, Message: Error
Simulation complete via $finish(1) at time 24 NS + 0
../assert_width_example.v:46 #2 $finish; //end
simulation after these many nsecs. To go indefinitely, comment this
line
ncsim> exit
I have tried all options to fire the assertion, but it's not happening.
I want to know what is keeping the assertion from getting fired. Any
help towards this will be greatly appreciated.
Best regards,
Amit.