For the 1st link as the property already has a Sampling Edge , forever @( posedge clk ) enables triggering of the assertion on each posedge of clk .
Is the Code considered Legal ? Some tools throw a Compilation Error
For the 2nd link the property is triggered only once at T:10 due to initial block being executed only once .
Here are a few points that I noted :
If the property doesn’t have Sampling Clock then : ONLY via always @( posedge clk ) will the Clock be inherited !!
Using forever @( posedge clk ) the Clock won’t be inherited for a property
If we want property to be fired only once , initial block is useful
( Assuming the property has it’s own Sampling edge )
For the 1st link as the property already has a Sampling Edge , forever @( posedge clk ) enables triggering of the assertion on each posedge of clk .
Is the Code considered Legal ? Some tools throw a Compilation Error
[Ben] All 1800 examples show the classical synthesizable form, without “begin” before the clocking expression. And I never saw that form being used unless the always contained multiple clocking events. I also did not see in 1800 a forever with a concurrent assertion.
It looks to me that the following should be legal if it does not have a blocking statement.
However, I do not know why some tools may consider the possibility of a blocking statement and would rather that you stick
My recommendations are:
Use the synthesizable syntax for an always @(posedge clk) as shown in 1800. Thus,
always @(posedge clk)
begin
ap_pab: assert property( a |-> ##1 b); // clock flows into the assertion
c <= d;
begin
Use the always begin … end syntax for combinational logic
always begin
ap_pab: assert ( a&& !b); // immediate assertion
w = d;
begin
For the 2nd link the property is triggered only once at T:10 due to initial block being executed only once .
Here are a few points that I noted :
[list=1]
[*] If the property doesn’t have Sampling Clock then : ONLY via always @( posedge clk ) will the Clock be inherited !!
YES
Using forever @( posedge clk ) the Clock won’t be inherited for a property
[Ben] It’s a bad style.
If we want property to be fired only once , initial block is useful
( Assuming the property has it’s own Sampling edge )
[Ben] Yes. Note that the 1st attempt can create a property that is attempted at every cycles with the always for example:
initial begin
if(go==0) wait(go);
else ap_ab: assert property @(posedge clk) always (a |-> ##1 b);
end
module tb1 ;
bit clk , cstart , req , gnt , CheckWrite ;
always #10 clk = !clk ;
property pr1( req ,gnt );
cstart |=> req ##2 gnt ;
endproperty
always @(posedge clk) begin // OK srtle
if ( CheckWrite )
assert property( pr1( req , gnt ) )
$display("TIME:%2t Assertion pr1 PASSes ", $time );
else $display("TIME:%2t Assertion pr1 Fails ", $time );
end
// BAD STYLE
always begin
@(posedge clk)
if ( CheckWrite ) // clock does not flow in
assert property( @(posedge clk) pr1( req , gnt ) ) // line 18
$display("TIME:%2t Assertion pr1 PASSes ", $time );
else $display("TIME:%2t Assertion pr1 Fails ", $time );
end
/* testbench.sv, 18
Procedural assertion (assert, assume or cover property) is not allowed after
# delay or event control statement. */
// BAD STYLE
initial forever begin
@(posedge clk)
if ( CheckWrite ) // clock does not flow in
assert property( @(posedge clk) pr1( req , gnt ) ) // line 27
$display("TIME:%2t Assertion pr1 PASSes ", $time );
else $display("TIME:%2t Assertion pr1 Fails ", $time );
end
/* Procedural assertion ( i.e., assert, assume or cover property) is not
allowed in looping statement.Only immediate assertions are allowed in this
context.*/
initial begin
CheckWrite = 1 ;
#09 ; cstart = 1 ;
#20 ; cstart = 1 ; req = 1 ;
#20 ; cstart = 0 ; req = 1 ;
#20 ; cstart = 0 ; req = 0 ; gnt = 1 ;
#20 ; cstart = 0 ; gnt = 1 ;
#05 ; $finish() ;
end
endmodule
Ben Cohen Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
In reply to Have_A_Doubt:
On the initial and the always(property), this is what 1800 says:
1800: 16.12.11 Always property
A property is an always if it has one of the following forms that use the always operators: — Weak always always property_expr A property always property_expr evaluates to true if, and only if, property_expr holds at every current or future clock tick.
…
In the following two examples, there is a one-to-one correspondence between the evaluation attempts of p specified by the implicit always from the verification statement implicit_always and the evaluation attempts of p specified by the explicit always operator in explicit_always:
Implicit form:
implicit_always: assert property(p);
Explicit form:
initial explicit_always: assert property(always p);
From this simple test, it seems to me that there is a tool issue here;
We don’t discuss tools in this forum.
Thus, I leave it here with 1800 telling like it should work.