In reply to ben@SystemVerilog.us:
After more thoughts, I believe that property is incorrect. Consider this instead
property p_data_unique;
int v_serving_ticket;
@(posedge clk) ($rose(a), v_serving_ticket=ticket, inc_ticket()) |=>
((a [->4]) intersect !o[*] )
##[1:5] $rose(a) && $rose(o)
&& now_serving==v_serving_ticket;
// With the ##[1:$] property will never fail. Suggest adding a limit, such as 5, or 10
endproperty
In reply to ben@SystemVerilog.us:
Achieving exclusivity of threads for each attempt is difficult.
For this particular problem, even above solution will not work for all attempts.
One other solution using tags and queues or associative arrays to keep track of the occurrences of A and O is necessary,
In any case, supporting logic is needed.
Ben
In reply to ben@SystemVerilog.us:
That problem is confusing, indeed!
From http://themindunleashed.org/2014/12/25-life-lessons-albert-einstein.html
- If you can’t explain it simply, you don’t understand it well enough.
A lot of truth there …
Thank you so much Ben for your time & ideas. I keenly saw your reply, and all these days was trying to materialize some solution from your comments. Let me mention the context of this work. The idea of logical clocks is used in this context initially proposed by Lamport in 1978 (1). The idea of these signals (or variables as you say in SystemVerilog terms) is simple, that the signal events don’t have any strict relation to a physical clock but focus more on the relation between the events. In short we can call them monotonically increasing time stamps (2). This concept of logical clocks is also used in some other programming languages like Esterel.
My PhD professor, invented a language Clock Constraint Specification Language (CCSL)(3) for the formal representation of relations between clocks/synchronous signals, represented by various operators. Recently for some work I am exploring the possible relation of those operators with the SystemVerilog Assertions.
For the most part, these relations are simple. Like in CCSL, there is a operator ‘Subclock’ that relates as ‘A isSubClockOf B’ means when there is an event on A, B must also be present but not the other way around. And we both know that this is the same as |-> of SystemVerilog Assertions.
But some other operators are not so much compatible like ‘Asfrom’ mentioned on page 13 of this report(4). For this Asfrom relation, the output signal O shouldn’t consider first k events and after that is coincident with the A. Apparently this relation should work for k = 5.
$rose(rst) ##1 ((a[=5]) intersect (!o[*])) |=> ((a ~^ o)[*0:1000]); // interval 0:1000 is used instead of 0:$
where I use the XNOR operator to check the resemblance of signals after the trigger k. But somehow it works fine for the part before the implication but not afterwards. I feel I lack some concepts about the working of SVAs here.
In reply to ben@SystemVerilog.us:
lolzzzzz. nice one :), I will try to explain the problem and the context in detail.
In reply to Jadoon:
Here is the picture to show the violations that were expected but never occurred.
Another quite similar relation is ‘Await’ where O = A await n is an output that ticks only once when the nth tick of A arrives, and then dies forever. Here is my interpretation for this (with n = 5):
$rose(rst) |=> ( (a[=5]) intersect (!o[*]) ) ##1 ( $rose(a) && $rose(o) ) ##1 ( (a[=1:$]) intersect !o[*] ) ;
Here as per your book, a[=2] is equivalent to
!a[*0:$] ##1 a ##1 !a[*0:$] ##1 a ##1 !a[*0:$]
then it seems quite OK but in practice it doesn’t work. May be you can help!
In reply to Jadoon:
I have to give some thought about what you wrote, but just looking at code
$rose(rst) |=> ( (a[=>5]) intersect (!o[*]) ) ##1 ( $rose(a) && $rose(o) ) ##1 ( (a[=1:$]) intersect !o[*] ) ;
// that should be
$rose(rst) |=> ( (a[->5]) intersect (!o[*]) ) ##[1:1000]( $rose(a) && $rose(o) ) ##1 (
//(a[=1:$]) intersect !o[*] ) ;
Above looks illegal (a[=1:$]
And if it is, it does not make sense.
I suggest that you explain that property in English.
Ben
In reply to ben@SystemVerilog.us:
In reply to Jadoon:
Textual description of AsFrom relation:
In reply to Jadoon:
Several comments:
Syntax
// $rose(rst) ##1 ((a[=5]) intersect (!o[*])) |=> ((a ~^ o)[*0:1000]);
// TOO MANY parentheses, modified it to:
($rose(rst) ##1 a[=5]) intersect !o[*] |=> (a ~^ o)[*0:1000]
*-------------------------------------
// You seem to INSIST on using in this case the a[=5] instead of the a[->5].
// b[=2] is equivalent to: // From my book, page 37
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]
b[->2] is equivalent to: // From my book, page 35
!b[*0:$] ##1 b ##1 !b[*0:$] ##1 b
//Thus, looking at the antecedent, using 2 for simplicity
($rose(rst) ##1 a[=2]) intersect !o[*]) // is same as
($rose(rst) ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b ##1 !b[*0:$]) intersect !o[*])
// The last !b[*0:$] creates a problem because all matches of antecedent must be
// executed for an assertion to succeed. See 2.5.1 first_match operator for an explanation.
// THUS, the assertion can never succeed; it can fail or be vacuous.
If you insist on using the [=5], then use the first_match operator
first_match($rose(rst) ##1 a[=5]) intersect !o[*] |=> (a ~^ o)[*0:1000]
// But, by using the goto -> operator, you don't need a first_match.
($rose(rst) ##1 a[->2]) intersect !o[*]) // is same as
($rose(rst) ##1 !b[*0:$] ##1 b ##1 !b[*0:$] ##1 b) intersect !o[*])
Requirements
module ccsl;
bit a, o, clk, rst;
// Initially, o must be 0
ap_o0: assert property(@(posedge clk)
$rose(rst) |-> o==0);
ap_p0: assert property(@(posedge clk)
($rose(rst) ##1 a[->5]) intersect !o[*] |=> a ~^ o[*0:1000]);
initial forever #5 clk=!clk;
initial begin
@(posedge clk) rst <= 1'b1;
@(posedge clk) rst <= 1'b0;
end
always @(posedge clk)
begin
if (!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=99};
a dist {1'b1:=40, 1'b0:=60};
o dist {1'b1:=10, 1'b0:=70}; }) $display("error");
end
endmodule
A few lessons that you may have learned from this exercise:
Ben Cohen
http://www.systemverilog.us/ ben@systemverilog.us
In reply to ben@SystemVerilog.us:
I believe that there are issues with the requirements.
// Contradiction: O will be 1 once in its life time and after that will die away.
// O can’t be 1 while A is 0, any occurrence of O other than the one specified above is a violation
Is o ==1 once and only once?
// Initially, o must be 0
ap_o0: assert property(@(posedge clk)
$rose(rst) |-> o==0);
ap_p0: assert property(@(posedge clk)
($rose(rst) ##1 a[->5]) intersect !o[*] |=> o==1'b1 ##0 a ~^ o[*1000]);
// Contradiction: O will be 1 once in its life time and after that will die away.
// O can't be 1 while A is 0, any occurrence of O other than the one specified above is a violation
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
Well this one you wrote here just above, seems to be the code for the AsFrom. I am still trying to get the desired result on my testbench for the AsFrom. I don’t know why the second part of the assertion (XNOR) doesn’t work with me. Haven’t yet checked the code for the Await.
Grand Summary of the two properties:
AsFrom: Initially O is 0, A comes at any time. On Kth arrival of A sampled on clk, O should be there, and afterwards O is exactly same as A.
Await: Initially O is 0, A comes at any time. On Nth arrival of A sampled on clk, O should be there, and afterwards O is zero again forever.
So yes O is ON once for a single clock cycle in its lifetime for the AWAIT property. Its not a contradiction, O will be 1 on the Nth detection of A, telling that the signal we were waiting for has arrived. Afterwards its zero forever. At that time when O=1, A must be 1 for the Nth time.
But for the other property AsFrom, O starts after the Kth event on A. and is exact copy of A. My apologies that the wording I chose made it confusing.
In reply to Jadoon:
OK, I worked out the AsFrom assertion and the tb for it.
The png result is at http://systemverilog.us/ccsl.png
The code is at http://systemverilog.us/ccsl.sv
I used constrained-randomization with count as the vehicle to define the types of constraints.
Using constrained-randomization is a fast way of achieving a variety of test vectors.
BTW, I added an error on count 16 to demonstrate the failure.
module ccsl;
bit a, o, clk, clk1, rst;
int count;
// Initially, o must be 0
ap_o0: assert property(@(posedge clk)
$rose(rst) |-> o==0);
// AsFrom: Initially O is 0, A comes at any time. On Kth arrival of A sampled on clk,
// O should be there, and afterwards O is exactly same as A.
// Let k==5
ap_AsFrom: assert property(@(posedge clk)
(($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] |->
o==1'b1 ##1 a ~^ o[*1000]);
initial forever #5 clk=!clk;
initial begin
@(negedge clk) rst <= 1'b1;
@(negedge clk) rst <= 1'b0;
end
always @(posedge clk)
begin
if (count <4) begin
if(a ) count<=count+1'b1; // increment before update of "a"
if(!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=999}; // can comment this line
a dist {1'b1:=25, 1'b0:=75};
o dist {1'b1:=10, 1'b0:=70};
0==1'b0;}) $display("error");
end
else if (count == 4) begin
if(!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=999};
a dist {1'b1:=30, 1'b0:=70};
o dist {1'b1:=10, 1'b0:=10};
o==a; }) $display("error");
if(a) count<=count+1'b1;
end
else if (count >= 5 && count <16 ) begin
count<=count+1'b1;
if(!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=999};
//a dist {1'b1:=30, 1'b0:=30};
//o dist {1'b1:=10, 1'b0:=10};
o==a; }) $display("error");
end
else if (count==16) begin
count<=count+1'b1;
if(!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=99};
a dist {1'b1:=30, 1'b0:=30};
o dist {1'b1:=10, 1'b0:=10};
a!=o; }) $display("error");
end
else begin
count<=count+1'b1;
if(!randomize(rst, a, o) with
{ rst dist {1'b1:=1, 1'b0:=999};
a dist {1'b1:=30, 1'b0:=30};
o dist {1'b1:=10, 1'b0:=10};
o==a; }) $display("error");
end
end
endmodule
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
I tried the property:
(($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] |-> o==1’b1 ##1 a ~^ o[*1000]);
but it fails for the case when 2 events of A have occurred and then O comes (but with no A). It doesn’t detect this violation as needed by !o[*] part. Let me simulate further and then will post the image.
In reply to Jadoon:
(($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1]
Is the antecedent; if it fails, assertion is vacuous.
Two options:
1) write another assertion with just the antecedent, I.e.,
(($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1]
If that sequence fails, that assertion will fail.
2) replace the implication operator with ##0. Thus,
(($rose(rst) ##1 a[->4]) intersect !o[*]) ##1 a[->1] ##0 o==1'b1 ##1 a ~^ o[*1000]);
Ben SystemVerilog.us
In reply to ben@SystemVerilog.us:
replacing the implication operator will make the program to expect a valid start on each clock cycle. thats what i think, and also i get 5/6 errors now, right from the beginning of the simulation.
In reply to Jadoon:
Use the implication operator after the rst
$rose(rst) |=> (a[->4]) intersect !o[*]) ##1 a[->1]
In reply to ben@SystemVerilog.us:
Seems I got the answer, using two assertions:
$rose(rst) |=> (a[->4] intersect !o[*]) ##1 a[->1] ##0 o==1'b1;
$rose(rst) |=> o[->1] ##0 a==1'b1 ##1 a ~^ o[*1000];
First assertion forbids O for 4 events of A, followed by 5th A with O.
Second assertion checks for O and expects A that time. It is to catch the violation:
rst…a…a…a…a…o…a
It is followed by the XNOR pattern. Just one question, I tried this assertion with the range a ~^ o[*1:$] and it didn’t worked. Can you refer to some detailed reading material for the reason behind it?
thanks a ton.