Using inout ports in SVA properties/assertions

SystemVerilog
, ,
1

Hi,

Is it possible to use input and output counterpart of inout port in SVA assertion/property?
Is there some SVA system functions of directives?

For example, if I use the following designs:
Example 1


module bidir (
    input clk, 
    input oe, 
    inout bi_port 
);
    reg data_tx, data_rx;
   
    always @(posedge clk)
    begin
	if (oe)
	    bi_port = data_rx;
        else
	    bi_port = 1'bZ;
    end 

    always @(posedge clk)
    begin
        data_rx = bi_port; 
    end 
endmodule

Or simpler one (without clk and always block)
Example 2


module bidir (
    input oe, 
    inout bi_port 
);
    data_tx, data_rx;

    assign bi_port = oe ? data_tx : 1'bZ;
    assign data_rx = bi_port;
       
endmodule

How can I approach input and output part of bi_dir?
Something like:
Related to Example 1 (output_part() is some contrived system function for the sake of the example.)


bi_dir_assert: assert property (
oe |=> output_part (bi_dir) == 1'b0);

Or some immediate assertions related to Example 2

Thanks!

2

In reply to Ratko:


module bidir (
    input logic clk, 
    input logic oe, 
    inout wire bi_port 
);
    logic data_tx, data_rx;
    bi_dir_assert: assert property (@(posedge clk) 
       oe |=> bi_port == data_rx); 
// IF oe is not from a register, do an deferred immediate assertion 
    always_comb if(oe) assert #0(bi_port == data_rx); 
      else assert #0(bi_port=='Z || top.bi_port);

    bi_dir_z: assert property (@(posedge clk) // if synchronous oe 
       oe==0 |=> bi_port=='Z || top.bi_port); // A Z or whatever is assigned at the higher level

 
    assign bi_port = oe ? data_tx : 'Z; 
      
    always @(posedge clk) data_rx <= bi_port; 
   
endmodule
  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Free books:
  1. Papers:
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1 and part 2
    Reflections on Users’ Experiences with SVA
    Reflections on Users’ Experiences with SVA - Part II
    SUPPORT LOGIC AND THE ALWAYS PROPERTY
    http://systemverilog.us/vf/support_logic_always.pdf
    SVA Alternative for Complex Assertions
    https://verificationacademy.com/news/verification-horizons-march-2018-issue
    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
    SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
    https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.

====================

  1. SVA Package: Dynamic and range delays and repeats SVA: Package for dynamic and range delays and repeats - SystemVerilog - Verification Academy
  2. Papers:
    Understanding the SVA Engine,
    Verification Horizons

Reflections on Users’ Experiences with SVA,

Reflections on Users’ Experiences with SVA, part 2

SUPPORT LOGIC AND THE ALWAYS PROPERTY

SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue

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

SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.

—---------------
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
** 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:
  3. Papers:
    Understanding the SVA Engine,
    Verification Horizons
    Reflections on Users’ Experiences with SVA, part 1 and part 2
    Reflections on Users’ Experiences with SVA

SUPPORT LOGIC AND THE ALWAYS PROPERTY
http://systemverilog.us/vf/support_logic_always.pdf
SVA Alternative for Complex Assertions
https://verificationacademy.com/news/verification-horizons-march-2018-issue
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
SVA for statistical analysis of a weighted work-conserving prioritized round-robin arbiter.
https://verificationacademy.com/forums/coverage/sva-statistical-analysis-weighted-work-conserving-prioritized-round-robin-arbiter.

Udemy courses by Srinivasan Venkataramanan (http://cvcblr.com/home.html)
https://www.udemy.com/course/sva-basic/
https://www.udemy.com/course/sv-pre-uvm/

3

In reply to ben@SystemVerilog.us:

Thanks Ben for your answer!