Writing Assertions for FSM

SystemVerilog
,
1

Hi,
I am trying to write assertions for the APB slave module using bind construct. And I have declared all my internal signals and other i/p and o/ps of the DUT as input to my assertion module. After executing I get and error stating
xmvlog: *E,SEQVER (testbench.sv,67|29): Sequences and properties are illegal as verilog operands.

I suppose the error is due to FSM states. How do I use my states in assertion block.
Thank You

Link for APB_SLAVE

2

In reply to sai_pra99:
Your main issue here is that in the antecedent you are ANDing a logical variable (the “&”) with a sequence, and that is ILLEGAL. Specifically, you have


(p_wren && setup_state) // setup_state is declared as a sequence 
// Thus, the compiler sees 
sequenceA && sequenceB // p_wren is a sequence of 1 term. 
// If you really want the AND, then you need the sequence AND operator, which is "and".
// I would use the Sequence fusion (##0) operator, Thus, 
 
   sequence setup_state;
    (state==SETUP_PHASE);
  endsequence
  
  property stable_wr_data;
    disable iff(!p_rstn)
    @(posedge p_clk)
   // (p_wren && setup_state) |-> ##1 !($isunknown(tmp_data) && $isunknown(tmp_addr));
    (p_wren ##0 setup_state) |-> ##1 !($isunknown(tmp_data) && $isunknown(tmp_addr));
  endproperty

There are other things about your code that needs to corrected, from a style point of view.

  1. Don’t use a program, use a checker or a module
  2. You have way too many sequence declarations of 1 term, why not put them inline with your assertion or with your property.
  3. If a property is used once and does not have local variables, then put the property contents within the assertion.
 ap_stable_wr_data: assert property( // better style
disable iff(!p_rstn)
@(posedge p_clk)
// (p_wren && setup_state) |-> ##1 !($isunknown(tmp_data) && $isunknown(tmp_addr));
p_wren && state==SETUP_PHASE |-> ##1 !($isunknown(tmp_data) && $isunknown(tmp_addr)) );
  1. Use the SystemVerilog style for port list, instead of Verilog style.

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
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats | Verification Academy
  2. Free books: Component Design by Example FREE BOOK: Component Design by Example … A Step-by-Step Process Using VHDL with UART as Vehicle | Verification Academy
    Real Chip Design and Verification Using Verilog and VHDL($3) Amazon.com
  3. Papers:
3

In reply to ben@SystemVerilog.us:

Hi sir,
Thanks for the reply and feedback. I have made all the possible changes and modifications as you have mentioned and now the code is error-free.

But then, there is no output shown in my console. The assertions are not firing like it has to. Can you please point out where I went wrong?

Modified EDA link APB_MOD

ThankYou

4

In reply to sai_pra99:

I have made all the possible changes and modifications as you have mentioned

Sorry, but you did not do the changes I asked.
I can’t debug your code, but I’ll give you pointers about your style that is Verilog instead of SystemVerilog.

  • Below is a SystemVerilog style port list

typedef enum{IDLE, SETUP_PHASE,ACCESS_PHASE} state_fsm;
//*******************Program**************************
module APB_assertions
#(D_WIDTH=16,A_WIDTH=8,DEPTH=16)
(input logic p_clk, p_rstn,
input logic[A_WIDTH-1:0] p_addr, wr_data, rd_data,
input logic p_wren, trans,
input state_fsm state,
input logic out, p_ready, p_sel, p_enable,
input logic[A_WIDTH-1:0] tmp_addr, tmp_data);
  • DO NOT use “reg”, use "logic’ // reg is not recommended for SystemVerilog.
  • You still use sequences of one term. If you like this style because the name of the sequence is meaningful to you, then use the let instead. thus,

// instead of
sequence setup_state;
(state==SETUP_PHASE);
endsequence
// USE
let setup_state = (state==SETUP_PHASE);
  • I did not see a clock generator in your testbench
  • I see in your testbench a lot of directed tests. That is OK, but you are using blocking assignments (the var = a_value;) instead of nonblocking assignment; this is needed for the assertions to work. Specifically, for directed tests:

// BAD STYLE
initial
begin
p_rstn=0; p_ready=0; trans=0;
#20 p_rstn=1; trans=1; p_wren=1; wr_data=16'h3456; p_addr=8'h44;
#60 p_ready=1;
// USE
initial
begin
p_rstn<=0; p_ready<=0; trans<=0;
@(posedge clk) // assuming clk is your clock
p_rstn<=1; trans<=1; p_wren<=1; wr_data<=16'h3456; p_addr<=8'h44;
repeat(3) @(posedge clk)  p_ready< =1;
//
/ Your clock gen
initial forever #10 clk=!clk;   // fix the delay
  • consider randomizing your variables. For example:

initial begin
repeat(200) begin
@(posedge clk);
if (!randomize(a, b)  with
{ a dist {1'b1:=1, 1'b0:=1};
b dist {1'b1:=1, 1'b0:=2};
}) `uvm_error("MYERR", "This is a randomize error");
end
$finish;
end

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
…

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books: Component Design by Example https://rb.gy/9tcbhl
    Real Chip Design and Verification Using Verilog and VHDL($3) https://rb.gy/cwy7nb
  3. Papers: