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:
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
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 Ben@systemverilog.us
Link to the list of papers and books that I wrote, many are now donated.
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.
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
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.
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);
