Assume for formal verification

Question

Hi, I am trying to write an assume as per following assumption:

> for every change in a data bus there should be only one corresponding valid signal ($rose), something like the image added. I tried writing this way but it is not working:

sequence valid_cond;
@(posedge clk)
$changed(Data) ##[0:$] $changed(Data);
endsequence

valid_assume: assume property (
@(posedge clk) disable iff(disable)
1'b1 |-> $rose(valid) and valid_cond
)
Tried above with throughout also.

Tool says constraint conflict.

Is there any alternative to this?

More info:
This valid can come anytime during the complete duration but we should definitely see one and only one valid rise

Answer 1

ViVer

Forum Access

7 posts

May 28, 2023 at 6:14 am

In reply to ViVer:

Quote:

Hi, I am trying to write an assume as per following assumption:
> for every change in a data bus there should be only one corresponding valid signal ($rose), something like the image added. I tried writing this way but it is not working:

sequence valid_cond;
@(posedge clk)
$changed(Data) ##[0:$] $changed(Data);
endsequence

valid_assume: assume property (
@(posedge clk) disable iff(disable)
1'b1 |-> $rose(valid) and valid_cond
)
Tried above with throughout also.

Tool says constraint conflict.

Is there any alternative to this?

More info:
This valid can come anytime during the complete duration but we should definitely see one and only one valid rise

Answer 2

ben@SystemVerilog.us

Full Access

2883 posts

May 29, 2023 at 10:15 pm

In reply to ViVer:
For every change in a data bus there should be only one corresponding valid signal ($rose),

valid_assume: assume property (
     @(posedge clk) disable iff(disable)
     $changed(Data)  |-> $rose(valid)); // May not be what you want
 
// This may be what you need
// If a change in data then ONE valid within this change and the next change 
valid_assume2: assume property (
     @(posedge clk) disable iff(disable)
// $changed(Data)  |-> valid[->1] within $changed(Data)[->2]
$changed(Data)  |-> valid[=1] intersect $changed(Data)[->2]
);

Ben Cohen

Link to the list of papers and books that I wrote, many are now donated.
http://systemverilog.us/vf/Cohen_Links_to_papers_books.pdf
or https://rb.gy/ibks5p

Getting started with verification with SystemVerilog
https://rb.gy/f3zhh

Answer 3

ViVer

Forum Access

7 posts

May 30, 2023 at 3:38 am

In reply to ben@SystemVerilog.us:

Difference between within/and/intersect: the change is w.r.t. the matching start and end point, right?
I mean if we use "and" that means valid is 1 at the same clock when $changed(data) is detected and if we use "within" that means valid can be 1 anywhere between two changes in data and with "intersect" both valid and data change detection points should match which means the duration of valid is equal to duration between two changes.

am I getting it right?

the problem however is a bit complex it doesn't say there is any relation of valid high duration with change in data. The more descriptive problem is there should be one valid per data change and that valid should remain asserted until it sees an ack after which it falls. maybe better to break into two assumes.

Answer 4

ben@SystemVerilog.us

Full Access

2883 posts

May 30, 2023 at 12:32 pm

In reply to ViVer:

Quote:

In reply to ben@SystemVerilog.us:
Difference between within/and/intersect: the change is w.r.t. the matching start and end point, right?
I mean if we use "and" that means valid is 1 at the same clock when $changed(data) is detected and if we use "within" that means valid can be 1 anywhere between two changes in data and with "intersect" both valid and data change detection points should match which means the duration of valid is equal to duration between two changes.
am I getting it right?

[Ben] NO. You are missing the goto operator.

$changed(Data)  |-> valid[->1] within $changed(Data)[->2]
// I am shying away from the "within" because a second valid would be missed. 
// 1800'2017: The construct seq1 within seq2 is an abbreviation for the following: 
(1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 
 
// This property 
$changed(Data)  |-> valid[=1] intersect $changed(Data)[->2]
// is same as 
$changed(Data)  |-> !valid[*0:$] ##1 valid ##1 !valid[*0:$] intersect $changed(Data)[->2]
// Thus, after a change in data there can be ONE valid between that change (at the attempt time) 
// and (including) the next change in data

Quote:

the problem however is a bit complex it doesn't say there is any relation of valid high duration with change in data.

[Ben] Above assertion does require valid to be true for only one cycle.

Quote:

The more descriptive problem is there should be one valid per data change and that valid should remain asserted until it sees an ack after which it falls. maybe better to break into two assumes.

valid_assume2: assume property (
     @(posedge clk) disable iff(disable) 
        $changed(Data)  |-> 
              valid[*1:$] ##1 ack ##1 !valid[*1:$] ##1 $changed(Data);
valid_assume3: assume property ( // valid can come in after a few cycles
     @(posedge clk) disable iff(disable) 
        $changed(Data)  |-> 
             valid[->1] ##0 valid[*1:$] ##1 ack ##1 !valid[*1:$] ##1 $changed(Data);

Let me know if this works out for you.
Ben

Languages & Standards

Methodologies

Techniques & Tools

Universal Verification Methodology (UVM)

Featured Courses

Additional Courses

Formal-Based Techniques

Analog/Mixed Signal

UVM Forum

SystemVerilog Forum

Coverage Forum

Additional Forums

Implementation Patterns

Specification Patterns

Pattern Resources

UVM Cookbook

Coding Guidelines & Deployment

Coverage Cookbook

Featured & On-Demand

On-Demand Library

Recording Archive

Conferences & WRG

Siemens EDA Learning Center

Blog & News

Verification Horizons Publication

About Us

Training

Portfolio

Explore

Siemens

Contact