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));