SV concurrent assertion does not work

[dario.dellaquia]

Hi,
I wrote the following piece of code.

---

module assert_one_hot_three_states_fsm
  (
  input bit clk,
  input bit reset,
  input bit a,
  input bit b,
  input bit c
  );

typedef enum bit [2:0] {st0 = 3'b001, st1 = 3'b010, st2 = 3'b100} assert_state_t;
assert_state_t assert_state;
  
always @(posedge clk) begin
  if (reset == 1'b1) begin
    assert_state <= st0;
  end
  else begin
    case (assert_state)
      st0     : begin
                case ({c,b,a})
                  3'b000  : begin
                              assert_state <= st0;
                            end
                  3'b001  : begin
                              assert_state <= st0;
                            end
                  3'b010 :  begin
                              assert_state <= st1;
                            end
                  default : begin
                              assert_state <= st0;
                              `uvm_error("assert_one_hot_three_states_fsm", "Description => Combination of input signals is not correct \n");
                            end
                endcase
                end
      st1     : begin
                case ({c,b,a})
                  3'b001  : begin
                              assert_state <= st0;
                            end
                  3'b010  : begin
                              assert_state <= st1;
                            end
                  3'b100  : begin
                              assert_state <= st2;
                            end
                  default : begin
                              assert_state <= st0;
                              `uvm_error("assert_one_hot_three_states_fsm", "Description => Combination of input signals is not correct \n");
                            end
                endcase
                end
      st2     : begin
                case ({c,b,a})
                  3'b001  : begin
                              assert_state <= st0;
                              `uvm_error("assert_one_hot_three_states_fsm", "Description => Loss of alignment \n");
                            end
                  3'b010  : begin
                              assert_state <= st0;
                              `uvm_error("assert_one_hot_three_states_fsm", "Description => Invalid FMS transition \n");
                            end
                  3'b100  : begin
                              assert_state <= st2;
                            end
                  default : begin
                              assert_state <= st0;
                              `uvm_error("assert_one_hot_three_states_fsm", "Description => Combination of input signals is not correct \n");
                            end
                endcase
                end
      default : begin
                  assert_state <= st0;
                end
    endcase
  end
end

ERROR_B_STABLE_WHEN_A_FALLS:
assert property (@(posedge clk) disable iff ((reset) | (!assert_state[0])) ($fell(a) |-> $rose(b)))
else begin //fail block
  `uvm_error("assert_one_hot_three_states_fsm", "Description =>  a 1-> 0, then b is stable\n");
end;

ERROR_C_STABLE_WHEN_B_FALLS:
assert property (@(posedge clk) disable iff ((reset) | (!assert_state[1])) ($fell(b) |-> $rose(c)))
else begin //fail block
  `uvm_error("assert_one_hot_three_states_fsm", "Description =>  b 1-> 0, then c is stable\n");
end;

ERROR_C_LOW:
assert property (@(posedge clk) disable iff ((reset) | (!assert_state[2])) (c))
else begin //fail block
  `uvm_error("assert_one_hot_three_states_fsm", "Description =>  c = 0 \n");
end;

endmodule : assert_one_hot_three_states_fsm

The last assertion works properly but the other two do not activate at all.
Is there anything wrong with them?

Question: is it legal to declare a concurrent assertion within a procedural code like always@?

Thanks and regards

/Dario

[ben2]

In reply to dario.dellaquia:
Your assertions appear to correctly written in terms of syntax.
I believe the reason that they are not triggering is because of the way to are using the variableassert_state. Specifically,

// declaration 
typedef enum bit [2:0] {st0 = 3'b001, st1 = 3'b010, st2 = 3'b100} assert_state_t;
assert_state_t assert_state;

// USAGE 
assert property (@(posedge clk) disable iff ((reset) | (!assert_state[1]))
   ($fell(b) |-> $rose(c)))

// Enum types are complex in SystemVerilog  (FWIW, they are better in vhdl) 
// I would have written your assertion (though not a good style) as 
assert property (@(posedge clk) disable iff ((reset) | (!assert_state==st1)) 
 ($fell(b) |-> $rose(c))) ...
// HOWEVER <<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<<-------
// I question your use of the assert_state variable in the disable.  
// Disable is typically used for resets.  Thus, this is a better assertion 

assert property (@(posedge clk) disable iff ((reset) 
  assert_state!=st1  && $fell(b) |-> $rose(c)) ...
// Thus, the assertion is vacuous if  assert_state==st1 instead of being disabled if 
// assert_state==st1
 

Question: is it legal to declare a concurrent assertion within a procedural code like always@?

Yes, it is called a procedural concurrent assertion
I explain all of this with examples in my SVA book. A quick summary and example:
4.3.4 Procedural Concurrent Assertion
 Rule: [1] A procedural concurrent assertion is a concurrent assertion statement that appears in a procedural code, such as an always, always_ff, or an initial block. Concurrent assertions are illegal inside final procedures because the only statements allowed inside a final procedure are those permitted inside a function declaration. Thus, only immediate assertions are allowed inside a final procedure. Concurrent assertions are also illegal in tasks and class methods.

  property p_ab; a |=> b; endproperty
always @(posedge clk) begin : a1
  a <= c;
  if(d) begin : if1
     ap_ab: assert property (p_ab); // Assertion pushed into queue. 
    // Its leading clocking event is (posedge clk), the current edge
     ap_ab_clk1: assert property (
         @(posedge clk1) (p_ab)); // Assertion pushed into queue. 
             // Its leading clocking event is (posedge clk1)
  end : if1
  // ap_ab_clk1 is put into the queue at @ (posedge clk), started at @ (posedge clk1)
end : a1 

There are rules to follow.
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
For training, consulting, services: contact Home - My cvcblr

• SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
• A Pragmatic Approach to VMM Adoption 2006 ISBN 0-9705394-9-5
• Using PSL/SUGAR for Formal and Dynamic Verification 2nd Edition, 2004, ISBN 0-9705394-6-0
• Real Chip Design and Verification Using Verilog and VHDL, 2002 isbn 978-1539769712
• Component Design by Example ", 2001 ISBN 0-9705394-0-1
• VHDL Coding Styles and Methodologies, 2nd Edition, 1999 ISBN 0-7923-8474-1
• VHDL Answers to Frequently Asked Questions, 2nd Edition ISBN 0-7923-8115

---

1. VF Horizons:PAPER: SVA Alternative for Complex Assertions - SystemVerilog - Verification Academy
2. http://systemverilog.us/vf/SolvingComplexUsersAssertions.pdf
3. “Using SVA for scoreboarding and TB designs”
   http://systemverilog.us/papers/sva4scoreboarding.pdf
4. “Assertions Instead of FSMs/logic for Scoreboarding and Verification”
   https://verificationacademy.com/verification-horizons/october-2013-volume-9-issue-3
5. SVA in a UVM Class-based Environment
   https://verificationacademy.com/verification-horizons/february-2013-volume-9-issue-1/SVA-in-a-UVM-Class-based-Environment