I am new to system verilog assertions. and i stuck with the below implementation in my code.
I have 3 signals a,b,c which are asynchronous.
a signal changes 4 times for a operation i.e i need to calculate time for 4 pulses of a.
b has some default value which i can use direct value.
c signal should start after 4 pulses of a + .
Ho w can i write assertion check for the signal C that is dependendent on a and b.
I see write a seperate a sequence for caluculating the signal a change for 4 times.
use that sequence inside a property which checks the c condition.
In reply to muralidar:
Your requirements are ambiguous; the following comments may help you in clarifying your requirements.
I have 3 signals a,b,c which are asynchronous.
[Ben] So they are not derived from any clock? Do you mean that a, b, c are generated from different clocks or are they derived from flops going through combinational signals? Could they be glitchy?
a signal changes 4 times for a operation i.e i need to calculate time for 4 pulses of a
[Ben] you did not state that your assertion needs to calculate “time”. ???
b has some default value which i can use direct value.
[Ben] what does the default value has to do with your assertion? Is it fixed all the time, or does it change. How does “b” play in your requirements?
[quote]c signal should start after 4 pulses of a + .Ho w can i write assertion check for the signal C that is dependent on a and b.I see write a separate a sequence for calculating the signal a change for 4 times, and then use that sequence inside a property to check the c condition.
[Ben]SVA needs clocks or events. If you want to say that after 4 pulses of “a”, then if(b) then c changes, then you can do something like the following, but you need clocks or you need to generate events.
// assuming that a, b, c are generated from separate clocks
module t;
bit clka, clkb, clkc;
bit a, b, c; // single pulses
bit go; // to start the checking process. More on that after you clarify your requirements
ap_abc: assert property(@(posedge clka) go && a ##1 a[->3]
|-> @(posedge clkb) b[->1] ##0 @(posedge clkc) c[->1]);
endmodule
I have a common clk for all 3 signals(a,b,c) of same module.
My requirement is that signal a repeats for 3 times but not for every clk then i need to wait for delay of value b then c signal should start risiong from 0 to 1.
The signal a sample on posedge clk but repetition of signal a is not dependent on clk. the second/ occurance of signal a may happen after more no of clks(ex: 4/5/6). basically we should not be dependent on clk while checking signalfor repetition.
I have written something like this: But it results in below compilation Error.
Can you please correct me if iam doing some thing wrong.
In reply to ben@SystemVerilog.us:
I have a common clk for all 3 signals(a,b,c) of same module.
[Ben] Thus, as you know, with a clock, SVA samples the signals in the Preponed region (i.e., a delta time just before the edge of the clock).
My requirement is that signal a repeats for 3 times but not for every clk then i need to wait for delay of value b then c signal should start rising from 0 to 1.
[Ben] I hope that you studied SVA, because, if you did, you will recall the The goto repetition operator (Boolean[->n]) allows a Boolean expression (and not a sequence) to be repeated in either consecutive or non-consecutive cycles, but the Boolean expression must hold on the last cycle of the expression being repeated. The number of repetitions can be a fixed constant or a fixed range.
The signal a sample on posedge clk but repetition of signal a is not dependent on clk.
[Ben] that part is ambiguous; how can “a” be both generated off of a clock, but yet not be dependent on a clock. Maybe what you mean is that “a” is synchronous to a clock, but can repeat at different cycles, or th repeat is not consecutive (e.g., 1 0 0 1 1 0 0 0 0 1).
the second/ occurrence of signal a may happen after more no of clks(ex: 4/5/6). basically we should not be dependent on clk while checking signal for repetition.
[Ben] Again the contradiction! SVA IS dependent on the clock and the sampling of the signals are in the Preponed Region. I think that what you mean is that the occurrences of “a” at not necessarily consecutive.
I have written something like this: But it results in below compilation Error.
Can you please correct me if iam doing some thing wrong.
property a_b_c_timing;
@(posedge clk)
@(posedge a)
(a[*4]) b |-> $rose(c)
endproperty
assert_a_b_c_timing_chk: assert property(a_b_c_timing)
Assertion says: if(rose(a), disable other starts of “a” with the go.
then wait for 3 occurrences of “a”, then start count variable vt until vt==b.
Then wait for 1 to 4 cycles for rose(c).
if assertion pass or fails, set go to 1 to enable other starts.
The first_match() is needed because of the ##[1:$]
Change what you need to match your requirements.
Simulation results
Thanks for reply. It helped me a lot and i changed my assertion little to have proper checks as per my requirement.
I have a question that how can we pass a variable inside a property.
ex: if i need to wait 4 repetitions of signal a i use a[->4], in the same way if i want to use a variable in place value 4 like a[->x]. so here x is configurable. I want to use variable because it is configurable from 0 to 7.
Same thing i need to apply for the this property which you replied.
In reply to ben@SystemVerilog.us:
Thanks for reply. It helped me a lot and i changed my assertion little to have proper checks as per my requirement.
:)
I have a question that how can we pass a variable inside a property.
ex: if i need to wait 4 repetitions of signal a I use a[->4], in the same way if i want to use a variable in place value 4 like a[->x]. so here x is configurable. I want to use variable because it is configurable from 0 to 7.
I explain another approach in my SVA Handbook 4th Edition, 2016 If the variable used to define the delay has values that are within a constraint range, such as between 0 and 7 (or 15, or at most 32) one can use the generate statement, which appears much simpler than the use of local variables and the sequence_match_item. Example:
generate for (genvar g_i=0; g_i<8; g_i++) begin
ap_delay_gen: assert property (v==g_i && $rose(a) |-> ##g_i b);
end endgenerate
For your assertion, you can do the following, but keep in mind that with the generate statement and more variables, you have many assertions. The generate is used because it creates static values after elaboration. The full model is at http://SystemVerilog.us/vf/repabc2.sv
the pertinent part is shown below:
module top;
bit clk, a, c, go=1;
bit[2:0] b=5, d=2; // delay variables for assertions
generate for (genvar g_i=0; g_i<8; g_i++) begin // one variable
property p_abc_timing2;
@(posedge clk)
(b==g_i && go && $rose(a), setgo(0)) ##1 a[->3] ##g_i 1'b1
|-> ##[1:4] $rose(c);
endproperty
ap_abc_timing2: assert property(p_abc_timing2) setgo(1); else setgo(1);
end endgenerate
generate for (genvar g_i1=0; g_i1<8; g_i1++) begin : t1// two variables
for (genvar g_i2=0; g_i2<8; g_i2++) begin : t2// two variables
property p_abc_timing3;
@(posedge clk)
(b==g_i1 && d==g_i2 && go && $rose(a), setgo(0)) ##1
a[->g_i2] ##g_i1 1'b1
|-> ##[1:4] $rose(c);
endproperty
ap_abc_timing3: assert property(p_abc_timing3) setgo(1); else setgo(1);
end // : t2
end endgenerate // : t1
the suggested code works for own implementation but we do not have control on the variable from property.
Actually the variable is coming from DUT which is configured in test. So i can not iterate through values inside property. Only i can use the value coming from DUT by binding the dut signal. but using the variable is not allowed.
