sig_a and sig_b are environment signals, which can be given at any time, but should never be given together
Every sig_a must eventually be acknowledged by sig_b, unless sig_c appears.
if there is a sig_a, followed by 3 consective sig_b, then in each of the 3 cycles the data written(DO) is equal to the data read(DI).
if the state machine reaches state=ACTIVE1, it will eventually reach state=ACTIVE2.
if there are two occurences of sig_a rising with state=ACTIVE1, and no sig_b occurs between them, then within 3 cycyles of the second rise of sig_a, START must occur.
show a sequence with 3 transactions (in which sig_a is asserted 3 times).
sig_a must not rise if we have seen sig_b and havent seen the next sig_c yet(from the cycle after the sig_b until the cycle before the sig_c)
if sig_a is down , sig_b may only rise for one cycle before the next time that sig_a is asserted.
The Auxiliary signal sig_a indicates that we have seen a sig_b, and havent seen a sig_C since then. it rises one cycle after the sig_b, and falls one cycle after the sig_c.
A. what is Eventually acknowlegment
B. what is Environment signals
Have you attempted any of these?
Which ones are you having trouble with?
It would be far more instructive for you to provide attempts at solutions and learn from your mistakes, we can help there.
I resolved 21 out of 30 Assertions interview Questions, some of the Assertions Queries are not understand as mentioned above and not able get idea, that why i mentioned in this thread.
mainly i struggling on 1,3,5,6 Queries as listed above
Below are my assertions for these. I made use of the gotooperator [->n], a very useful operator. I wrote several responses on this. Do a google search on
verificationacademy cohen “goto” first_match
Would be nice to see how you wrote the ones you wrote.
module top;
timeunit 1ns/100ps;
`include "uvm_macros.svh"
import uvm_pkg::*;
bit clk, a, b;
bit[15:0] DI, DO;
bit[15:0] mem[31:0];
typedef enum {ACTIVE1, START} st_t;
st_t state;
initial forever #10 clk=!clk;
// 1) a and b are environment signals, which can be given at any time, but should never be given together
ap1_not_a_and_b: assert property(@ (posedge clk) not(a && b) );
// 3) if there is a sig a, followed by 3 consective sig b,
// then in each of the 3 cycles the data written(DO) is equal to the data mem(DI).
// $past( expression1 [, number_of_ticks] [, expression2] [, clocking_event])
ap3_a3bmem: assert property(@ (posedge clk) a ##1 b[*3] |->
DO==mem[DI] && $past(DO, 1)== $past(mem[DI],1) && $past(DO, 2)== $past(mem[DI],2));
// 5) If there are two occurences of sig a rising with state=ACTIVE1,
// and no sig b occurs between them, then within 3 cycyles of the second rise of sig a, START must occur.
ap5_aa_nob: assert property(@ (posedge clk)
$rose(a) && state==ACTIVE1 ##1 $rose(a) && state==ACTIVE1[->1] intersect !b[*1:$] |->
##[1:3] state==START );
// 6. show a sequence with 3 transactions (in which sig_a is asserted 3 times).
sequence q_a3;
@ (posedge clk) a[->3];
endsequence
initial begin
repeat(400) begin
@(posedge clk);
if (!randomize(a, b, state, DI, DO) with
{ a dist {1'b1:=1, 1'b0:=1};
b dist {1'b1:=1, 1'b0:=2};
DO dist {16'b0000:=1, 16'H000F:=1};
DI dist {16'H0000:=1, 16'H000F:=1};
}) `uvm_error("MYERR", "This is a randomize error");
end
$finish;
end
endmodule
I tried for few above listed Queries, Please correct it when assertions are went wrong
Every sig_a must eventually be acknowledged by sig_b, unless sig_c appears.
sig_a|=> !sig_c ##1 sig_b
if the state machine reaches state=ACTIVE1, it will eventually reach state=ACTIVE2.
state==ACTIVE1 |-> 1[0:$] ##1 state==ACTIVE2
sig_a must not rise if we have seen sig_b and havent seen the next sig_c yet(from the cycle after the sig_b until the cycle before the sig_c)
!sig_a |=> sig_b[0:$] ##1 sig_a |=> sig_c
if sig_a is down , sig_b may only rise for one cycle before the next time that sig_a is asserted.
!sig_a |-> 1[0:$] ##1 sig_b |=> sig_a
The Auxiliary signal sig_a indicates that we have seen a sig_b, and havent seen a sig_C since then. it rises one cycle after the sig_b, and falls one cycle after the sig_c.
sig_a |=> (sig_b and !sig_c) ##1 sig_c ##1 !sig_b
In reply to Subbi Reddy: A few comments: Your solutions indicate to me that you have not really studied SVA, and know a very limited number of constructs. If I was giving these interview questions, I am sorry to tell you that you failed. If you need to use SVA, you need to really study it. There are many good books (including mine) that cover the subject. Tis forum also provides many solutions to real assertion problems.
/*2. Every sig_a must eventually be acknowledged by sig_b, unless sig_c appears.
sig_a|=> !sig_c ##1 sig_b */
// When a "MUST" is in the spec, you need to use the strong property qualifier in the consequent
// It is unclear if c occurrs it is a pass or a failure. Am assuming a failure
ap_a_eventually: assert property(@ (posedge clk) sync_reject_on(c) // ? sync_accept_on(b)
a |=> s_eventually b );
/* 4. if the state machine reaches state=ACTIVE1, it will eventually reach state=ACTIVE2.
state==ACTIVE1 |-> 1[0:$] ##1 state==ACTIVE2 */
ap_4a: assert property(@ (posedge clk) state==ACTIVE1 |-> strong(##[1:$] ##1 state==ACTIVE2)); // Use strong if a must
ap_4b: assert property(@ (posedge clk) state==ACTIVE1 |-> s_eventually(state==ACTIVE2));
/*7. sig_a must not rise if we have seen sig_b and havent seen the next sig_c yet
(from the cycle after the sig_b until the cycle before the sig_c)
!sig_a |=> sig_b[0:$] ##1 sig_a |=> sig_c */
ap_7a: assert property(@ (posedge clk) b |-> strong(!$rose(a)[->1] within b ##[1:$] c ));
ap_7b: assert property(@ (posedge clk) not(!$rose(a) && c) );
// Note: (seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
/*8. if sig_a is down , sig_b may (MUST ?) only rise for one cycle before the next time that sig_a is asserted.
!sig_a |-> 1[0:$] ##1 sig_b |=> sig_a */
// The "may" is ambiguous.
ap_8: assert property(@ (posedge clk) !a |-> strong(b[->1] ##1 1'b1 intersect a[->1] ));
/*9a. The Auxiliary signal sig_a indicates that we have seen a sig_b,
and havent seen a sig_C since then.*/
// This need some interpretation. It is not a clear requirement.
// This requirement imposes the need of support logic since "b" occurs in the past of "c"
// by an underterminate number of cycles.
bit b_occurred, c_occured;
always_ff @(posedge clk) begin // support logic
if(b) b_occurred <=1'b1;
if(c) c_occured <=1'b1;
if(a) begin b_occurred <= 1'b0;
c_occured <=1'b0; end
end
ap_9a: assert property(@ (posedge clk) a |-> b_occurred && !c_occured);
/* 9b sig_a rises one cycle after the sig_b, and falls one cycle after the sig_c.
sig_a |=> (sig_b and !sig_c) ##1 sig_c ##1 !sig_b */
ap_9: assert property(@ (posedge clk) b |=> $rose(a) ##1 c[->1] ##1 $fell(a));
If you need links to users’ questions on Assertions that I answered , I suggest that you do a Google search on Verificationacademy.com cohen assertion property
Over the years I answered many questions on this forum, and other users also contributed.
You can also do a more generic search: verificationacademy.com assertion property
There are also videos and other papers on the subject.
Ben
// Note: (seq1 within seq2) is equivalent to: ((1[*0:$] ##1 seq1 ##1 1[*0:$]) intersect seq2 )
The expr[*0:m] repetition declares that the element in the SEQUENCE must repeat (i.e., can be skipped altogether 0 times ), or 1 times, or 2 times, or … m times.
The example, b[*0:3] means that b may either be skipped (i.e., no cycle spent on b), or b may be repeated once, twice, or three times.
In the sequence (b[*0:3] ##1 c), if c holds at the start of this sequence, then a check on b is skipped altogether, as if it were not there. However, if c does not hold at the start of the sequence, then b needs to hold a maximum of three cycles . As a result, this construct creates a set of different threads that can occur. The following describes the expected behavior for this assertion.
a |-> (b[*0:3] ##1 c); // one thread at each attempt
// equivalent to
a |-> // (b[*0] ##1 c ) //is equivalent to c
( c ) or
(b[*1] ##1 c ) or
(b[*2] ##1 c ) or
(b[*3] ##1 c );
// b is the expression, which can be 0 or 1
// b can be any expression, including the value of 1
Check out my papers in my signature below.
Also study the repetition operator, many books and sites cover this topic.
Ben Cohen http://www.systemverilog.us/ben@systemverilog.us
** SVA Handbook 4th Edition, 2016 ISBN 978-1518681448
…
Hi Ben, I now understand what the difference between [*0:] and [*1:] is. I looked up repetition operators online but I still don’t understand what the ‘1’ prefix in 1[*0:$] is. Can you please explain this?
In reply to vk7715:
SVA allows an expression or a sequence to be repeated. For example:
b[*2] is equivalent to b ##1 b
(a ##1 b)[*2] is equivalent to (a ##1 b) ##1(a ##1 b).
the expression can be a variable (like “a”, or it can be a constant like 1’b1 or just 1
Thus 1[*2] is same as 1 ##1 1
same as true ##1 true,
(seq1 within seq2) is equivalent to: ((1[*0:] ##1 seq1 ##1 1[*0:]) intersect seq2 )
COuld have written this as
(seq1 within seq2) is equivalent to: ((##[0:] seq1 ##[0:]) intersect seq2 )
Hi, I was just observing your solution. And I think, I got another way to write an assertion for Question:- 05.
// Question - If there are two occurrences of sig a rising with state=ACTIVE1,
// and no sig b occurs between them, then within 3 cycles of the second rise of sig a, START must occur.
property p1;
$rose(a) && state == ACTIVE1 ##1 !b[*1:$] ##1 $rose(a) && state == ACTIVE1 |-> [1:3]state == start;
endproperty
assert property (p1);
In reply to Shubhabrata:
You need a first_match. From my SVA book: 2.5.1 first_match operator
Section 2.3.2 addressed the multiple matching of sequences, and explained the consequences of
such matches. For example, the sequence ($rose(a) ##[2:3] b) has two possible matches, and
(rose(a) ##[2:] b) can have an infinite number of matches as that can be decomposed as a
series of threads ORed together. To avoid the possibility of multiple matches that could cause
unexpected errors, or cause an assertion to never succeed because all threads of an antecedent
must be tested for a property to succeed, one could use the first_match(a_sequence) operator.
Rule: [1] The first_match operator matches only the first of possibly multiple matches for
an evaluation attempt of its operand sequence. This allows all subsequent matches to be
discarded from consideration. This is significant when a sequence is used in the antecedent of an assertion because when a range is used in the antecedent, it can create multiple threads, each triggering the evaluation of the consequent when matched, and all threads must hold for the assertion to hold. This can cause significant performance impacts and possible unexpected errors.
However, applying the first_match operator has significant (positive) effect on the evaluation of
the enclosing sequence. Consider the following example:
ap_never_succeed: assert property(
($rose(a) ##[2:$] b) |=> c);
//The assertion ap_never_succeed is equivalent to
ap_equivalent_to_ap_never_succeed: assert property(
($rose(a) ##2 b)or
($rose(a) ##3 b)or
…
($rose(a) ##n b)|=> c); // where n is infinity
For the ap_equivalent_to_ap_never_succeed assertion to succeed, all threads must succeed, and
there are an infinite number of threads; specifically, these threads include:
($rose(a) ##2 b) |=> c // thread 1
($rose(a) ##3 b) |=> c // thread 2
…
($rose(a) ##n b)|=> c // thread n
If any of these threads fails, then the assertion fails; however success cannot be achieved. With the first_match method, only the first match of the sequence is considered, and all other threads are ignored. Thus, in the assertion ap_FM_can_succeed a first match of the antecedent is considered for the evaluation of the consequent.
ap_FM_can_succeed: assert property(
first_match($rose(a) ##[2:$] b) |=> c);
// Question - If there are two occurrences of sig a rising with state=ACTIVE1,
// and no sig b occurs between them, then within 3 cycles of the second rise of sig a, START must occur.
property p1;
first_match($rose(a) && state == ACTIVE1 ##1 !b[*1:$] ##1
$rose(a) && state == ACTIVE1) |-> [1:3]state == start;
endproperty
assert property (p1);
Hello Sir, Understood what you described. But I want to know if I have written any wrong assertion . Because it looks okay to me.
In reply to ben@SystemVerilog.us:
Hi, I was just observing your solution. And I think, I got another way to write an assertion for Question:- 05.
// Question - If there are two occurrences of sig a rising with state=ACTIVE1,
// and no sig b occurs between them, then within 3 cycles of the second rise of sig a, START must occur.
property p1; rose(a) && state == ACTIVE1 ##1 !b[*1:] ##1 $rose(a) && state == ACTIVE1 |-> [1:3]state == start;
endproperty
assert property (p1);
Could you tell me whether I can do it or not?
I got a couple more queries.
In question - 7, you used two ways to write the code. In the 2nd one, I assume that you
missed writing b |->. Probably after this ( not (!$rose(a) && c) ) fits well.
I got another solution, I guess. Please look into that.
b|-> !$rose(a) until c;
In question - 8, You have solved it considering "… must appear … ". But the
problem says “… may appear…”. And, I think it’s correct. I tried something. Please look into this too.
In reply to ben@SystemVerilog.us:
Hello Sir, Understood what you described. But I want to know if I have written any wrong assertion . Because it looks okay to me.
ABove assertion looks OK, but it needs the first_match.
I got a couple more queries.
In question - 7, you used two ways to write the code. In the 2nd one, I assume that you
missed writing b |->. Probably after this ( not (!$rose(a) && c) ) fits well.
I got another solution, I guess. Please look into that.
In question - 8, You have solved it considering "… must appear … ". But the
problem says “… may appear…”. And, I think it’s correct. I tried something. Please look into this too.
!a[*1:$] |-> b[=0:1] ##1 a;
BAD style! !a[*1:$] |-> … causes unnecessary multiple threads at each attempt;
just use !a
If b “may” appear, you are essentially say that it does not matter if it does or does not appear. Thus, b is not in the equation.
Same thing in people’s behavior: “I go to the airport; it may or may not rain, I am taking the plane to go to Las Vegas”. The rain is not consequential.
Thus, you can write
!a |-> a[->1];
Still, I think the last question requires special attention. That question emphasizes that if sig_b appears, it should not be more than one clock cycle. It’s not appearing, that’s acceptable; and if it intends to show up, it should be for one clock cycle. We need to focus on this one clock cycle factor.
That’s why I came up with that solution. I admit the first repetition was unnecessary. To be honest, thinking about it now, I believe it’s stupidity.
!a |-> b[=0:1] ##1 a;
I think this one is perfect.
If there is any more suitable answer, please put it in this thread. And also, please look into my observation. b[=0:1] takes care of the number of occurrences of sig_b. Now the reason behind using a non-repetition operator instead of using a goto one is we don’t know when a will be asserted after the occurrence of b if it happens.
b[=1] // is equivalent to:
!b[*0:$] ##1 b ##1 !b[*0:$]
b[=0:1] ##1 a; // is equivalent to
b ##1 !b[*0:$] ##1 a or // because of the empty match !b[*0] ##1 b ##1 !b[*0:$]
!b[*1] ##1 b ##1 !b[*0:$] ##1 a
THus, !a |-> b[=0:1] ##1 a; requires that b appears either immediately or later on.