Hello All,
I tried to search the forum and ben cohen’s book but couldn’t find the solution SystemVerilog assertion for my problem.
I have two clocks A and O, and a constant K=5. I want to count first five events/ticks of A (which are randomly arriving) and forbid O from occurring (else violation). After those 5 ticks, O is the exact copy of A. I tried to count 5 ticks of A but every arrival of A triggers a new thread. I tried to use first_match but couldn’t manage to get the results.
In ben’s book, they have this problem “If CONDl then n occurrences of COND2 before COND3; n is value of a variable”. But there they have a start condition “$rose(cmd==WRITE)”. In my case I have no start condition but only CLOCK A. Here is what I tried:
first_match( rose(A) ##1 A[=4] ) |=> (A && O)[=1:];
Glad that you’re using my book :)
Your requirements are not clear.
have two clocks A and O, and a constant K=5. I want to count first five events/ticks of A (which are randomly arriving) and forbid O from occurring (else violation). After those 5 ticks, O is the exact copy of A. I tried to count 5 ticks of A but every arrival of A triggers a new thread. I tried to use first_match but couldn’t manage to get the results.
Variables used in assertions are checked at clocking events. Are you saying that A and O are clocks, and you’re trying to count 5 clocking events of A (like rising edges)with no clocking event of O during that time? And then you have one clocking event of O?
OR, are you saying that A and O are variables clocked by separate clocks or the same clock?
You need to clarify your requirements. In any case, I have 2 comments:
first_match( rose(A) ##1 A[=4] ) |=> (A && O)[=1:];
bit A, O, clk;
// that should be written as:
ap_AO: assert property(@(posedge clk)
$rose(A) ##1 A[->4] |-> ##[1:$](A && O));
but every arrival of A triggers a new thread. I tried to use first_match but couldn’t manage to get the results.
first_match is used in antecedents because otherwise the assertion can never succeed. This is because all threads of the antecedent must be exercised.
You’re seeking uniqueness in that you don’t want an event from one thread to affect other threads. I wrote the following for a future update of my book (TBD release date) http://SystemVerilog.us/uniqueness.pdf
That should help in providing a solution for uniqueness.
Thanks Ben for the reply, Its great feeling to talk to the author whose book I am following these days. Sorry that my question wasn’t that clear. I am actually using SVAs in a research context, so the requirements are quite strange. Also I am not much experienced with SVAs. But I am quite hopeful that it will be a case-study to help other researchers having same issues.
My design consists of two clocks A and O and a variable K (which is 5 for now). The clocks A,O are logical meaning the clock events can come at random intervals, but synchronously on the system clock (from 1 cycle to many cycles). By clock event we don’t necessarily mean the rising edge event (on A), it can be that the value of A is sampled 1 on the rising edge of clk. The expression O = A asfrom K
, where k is a natural number, de fines a clock that is a tight sub-clock of A starting after index K. For example, the event O occurring on the 3rd or 9th clock of A will generate a violation. or event O occurring while the event A is not there will also cause violation. Here is the picture showing one possible execution of events: http://postimg.org/image/gqkom70y7/
I have got one solution to this problem but it is based on the use of external variable cnt (count):
module AsFrom();
reg clk,a,o;
initial
begin
clk=0;a=0;o=0;
#200
a=1; #100 a=0; // a
#100
a=1; #100 a=0; // a
//#100
//o=1; #100 o=0; // o, will cause violation
#200
a=1; #100 a=0; // a
#200
a=1; #100 a=0; // a
#100
a=1; #100 a=0; // a
//#100
//a=1; #100 a=0; // a, will cause violation
#200
a=1;o=1; #100 a=0;o=0; // a,o
#200
a=1;o=1; #100 a=0;o=0; // a,o
#300
a=1;o=1; #100 a=0;o=0; // a,o
#100
a=1;o=1; #100 a=0;o=0; // a,o
#200
a=1; #100 a=0; // a, will cause violation
#200
o=1; #100 o=0; // o, will cause violation
end
always #50 clk = ~clk;
int cnt=0;
const int k=5;
always @(posedge clk) begin
if (a && (cnt < k)) cnt++;
end
// As From
property AsFrom;
@(posedge clk)
o |-> (a && cnt==k);
endproperty
assert property (AsFrom);
endmodule
I want to get the solution based on assertions only. I feel the non-consecutive repetition operator [=5] would be used something like, rose(rst) ##1 A[=5] |=> (A && O)[=1:];
But it doesn’t forbid the clock O. There is a solution in your book using local variables that looks interesting, i quote:
But i couldn’t relate it to my problem. Moreover, one further question can we have a solution for if we have no reset signal rst? can we still count the clock events on A? Will each event not start a new thread for the antecedent (for which first_match may help)?
One auxiliary question, my copy of questasim 10.0c doesn’t support ‘until/until_with’ so i couldn’t try this command. Is it possible to do ‘A until B’ on logical clocks any other way?
Thanks again for your reply and time, it may help many in the future.
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
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
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.
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):
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
// $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
I have two variables A and O that are related to each other.
Each clock cycle of clk, the values of A,O are sampled.
Initially, the O must be 0 else it would be a violation.
[Ben] That should be a separate assertion
*-----------------------------------------------
There is no restriction on A, that when it can come.
When we see the high value on A for the nth time (say 5th time), then that’s the moment when O should also be 1.
The sampled value of A can possibly be 1 for five consecutive cycles of clk or it can come literally after a gap of 1000s of cycles of clk.
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] I believe that what you lastly wrote seems to be what you need. Below is code that I tested.
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:
Making requirements clear is necessary.
Assertions help in clarifying the requirement becuase it forces you to explain.
Write many small assertions
If confusing, write the requirements, step-by-step in English
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
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.
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
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.
(($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]);
