Trying Concurrent Assertions within Procedural Context

SystemVerilog
,
2

In reply to Have_A_Doubt:

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:

  1. 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
  1. 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.

or Links_to_papers_books - Google Docs

Getting started with verification with SystemVerilog