property expression evaluation in observed region

Hi,

Could someone please clarify my confusion about the following line
from the SystemVerilog standard:

14.3 The stratified event scheduler
....
The Observed region is for the evaluation of the property
expressions when they are triggered.

Doesn't this mean that for the code below an 'rdy' should be
'ack'ed as if it were combinatorial? because that is not what happens
and indeed
examples from the standard don't support my interpretation.

module assert_property_test();

reg clk, ack;
reg [7:0] req;
wire rdy;

initial begin
clk = 0;
req = 1;
end

always #5 clk = ~clk;

always @(posedge clk)
if (req[7]) begin
if (ack) req = 1;
end
else
req = req << 1;

assign rdy = req[7];

property rdy_ack;
@(posedge clk) rdy;
endproperty

assert_rdy_ack: assert property( rdy_ack )
begin ack = 1'b1; end
else
begin ack = 1'b0; end

endmodule

 

[Jonathan Bromley]

On Fri, 31 Aug 2007 03:05:28 -0700, eascheiber@yahoo.com wrote:

Hi,

Could someone please clarify my confusion about the following line
from the SystemVerilog standard:

14.3 The stratified event scheduler
....
The Observed region is for the evaluation of the property
expressions when they are triggered.

Doesn't this mean that for the code below an 'rdy' should be
'ack'ed as if it were combinatorial?

No. Although properties are evaluated in Observed, those
evaluations use signal values that were sampled in the
Preponed region - on entry to the timeslot, before
anything has happened. So although you change your "rdy"
signal in the Active region, the value of "rdy" that is
seen by the property is the value as it was just before
the clock edge.

I assume you are aware that your code is, to say the
least, eccentric? I'm guessing that it is a test
case, to calibrate your own understanding? Of course,
you would never write a clocked "always" block that
wrote to its output signals using blocking assignment.

Also, of course, it is quite inappropriate to use
assertions' action blocks to implement logic functionality.

module assert_property_test();

reg clk, ack;
reg [7:0] req;
wire rdy;

initial begin
clk = 0;
req = 1;
end

always #5 clk = ~clk;

always @(posedge clk)
if (req[7]) begin
if (ack) req = 1;
end
else
req = req << 1;

assign rdy = req[7];

property rdy_ack;
@(posedge clk) rdy;
endproperty

assert_rdy_ack: assert property( rdy_ack )
begin ack = 1'b1; end
else
begin ack = 1'b0; end

endmodule

--
Jonathan Bromley, Consultant

DOULOS - Developing Design Know-how
VHDL * Verilog * SystemC * e * Perl * Tcl/Tk * Project Services

Doulos Ltd., 22 Market Place, Ringwood, BH24 1AW, UK
jonathan.bromley@MYCOMPANY.com
http://www.MYCOMPANY.com

The contents of this message may contain personal views which
are not the views of Doulos Ltd., unless specifically stated.