Hello,
Can I please get some help in writing an assertion with this question :-
a signal can be high for m number of clocks within a window of n clocks ?
where n > m
In reply to Ashmika:
1. a signal is high.
2. N widow of clocks
3. M signal stays. Assumption: signal stays continuously for M clock cycles.
property
@(posedge clk)
$rose(signal) |-> 1[*N] intersects signal[*M]
endproperty
In reply to kddholak:
Can You elaborate it a little more ?
I know that for intersect to pass both the antecedent and consequent should start and end at the same time .
In reply to Ashmika:
The above assertion N > M.
N is the number of clock cycles. it can be done by 1[*N] number of clock cylces.
M is the number of clock cycles to stay high signal. signal[*M]
clk |…|…|…|…|…|…|…|…|
signal 0 1 1 1 1 1
1 1 1 1 1 1 …
it will match up your start,and endpoint checks
a is a single bit
for every n clock cycle a can occur at most m times
int count_a, count_clk;
@(posedge clk)
(1,count_a=0,count_clk=0) |=> (1,count_clk++, count_a +a )[*n] ##1 (count_a<=m);
2 Likes
I like your simple solution. However, I am not clear on a few things
(1) Why do you have a non-overlapping implication ?
(2) Since you don’t use local variable count_clk at the end, do you even need it ?
(3) Shouldn’t (1,count_clk++, count_a +a )[*n] be
(1,count_clk++,count_a = count_a + a )[*n] / (1,count_clk++, count_a += a )[*n] ?
(4) Any particular reason you wait for 1 more clock ( via ##1 ) to check (count_a<=m) instead of simply using ##0 ?
Thank you for correcting me. count_clk is not needed.
property a_assert;
int count_a;
@(posedge clk)
(1,count_a=0) |-> (1, count_a= count_a +a )[*n] ##0 (count_a<=m);
endproperty
Note:
To make it work with multi-bit you can have additional nets/regs , something like
assign single_bit_net =(multi_bit_vector== value) ;
I didn’t get this
This would not compile.
Like I mentioned earlier it needs to be count_a+=a or count_a = count_a + a
Lets say you need to check if a (a 3 bit vector) needs to be 2 or 3 or 7 for m cycles in total within n clocks. I have made use of additonal signals and checked if
wire valid_a;
assign valid_a = (a==2 || a==3 || a==7) ? 1 : 0 ;
property a_check;
int count;
@(posedge clock) (1,count=0) |→ (1,count=count+valid_a)[*n] ##0 (count==m);
endproperty
endproperty
@ankith_rao Additional signals could be avoided by replicating the logic within the property
property a_assert;
int count_a;
@(posedge clk)
(1,count_a=0) |-> (1, count_a+= (a inside {2,3,7} ? 1 : 0 ) )[*n] ##0 (count_a<=m);
endproperty