Wan yo write a assertion for following senario:
Signal is ‘A’ is deassrting when signal ‘B’ deasserted .
aftersignal B again asserted and after 2/3 clks I wan to check signal A value and ensure that It’s same as before dessartion of siganl B .
Is there a easy way for writing same using system verilog inbuilt functions ?
module test_ab;
/* Want to write a assertion for following scenario:
Signal is 'A' is deasserting when signal 'B' deasserted .
after that signal B is again asserted and after 2 to 3 clks
I want to check signal A value and ensure that It's same as before dessertion of siganl B .
Is there a easy way for writing same using system verilog inbuilt functions ? */
bit[3:0] a, b;
bit clk, a0, b0;
// Definition of a being asserted for a vector is not clear by your requirements.
// I'll assume that "not asserted" means that a==4'b0000
ap_notA_NotB: assert property(@ (posedge clk) a==4'b0000 |-> b==4'b0000);
property a_stable;
bit[3:0] v;
(b!=4'b0000, v=a) |-> ##[2:3] a==v;
endproperty
ap_B_then_A: assert property (@ (posedge clk) a_stable);
endmodule
Ben Cohen http://www.systemverilog.us/
In reply to ben@SystemVerilog.us:
thanks Ben
Just curious how it works …
(b!=4’b0000, v=a)
can you pls explain same ?
One more doubt w.r.t. this implementation is initial value of signal ‘B’ is 0.
Whenever 1st time signal ‘B’ will be asserted will above implementation will be hold good.?
In reply to dave_59:
(b!=4’b0000, v=a)
can you pls explain same ?
One more doubt w.r.t. this implementation is initial value of signal ‘B’ is 0.
Whenever 1st time signal ‘B’ will be asserted will above implementation will be hold good.?
If you’re looking for transitions, use the $fell; thus,
($fell(b!=4’b0000), v=a)
Ben systemverilog.us
In reply to ben@SystemVerilog.us:
property a_stable;
bit[3:0] v;
(b!=4’b0000, v=a) |->##[2:3] a==v;
endproperty
THe RHS is not fullfilling the requirement .
The requirement was after asserting signal ‘B’ , then 2/3 clk cycle delay value of ‘A’ need to be checked with previous value of ‘A’ i.e. before $fell of signal ‘B’ ie before last dessert of ‘B’.
I think somthing like below will be the requirements for same:
property a_stable;
bit[3:0] v;
(b!=4’b0000, v=a) ##1 !b[*0:$] ##1 $rose(b) |->##2:4;
endproperty
can you pls rethink regarding requirement?
In reply to skumarsamal:
wire B; // easier to deal with single bit rather than a vector.
assign B= b==4'b0000; // You need to define this, per your requirements
// Am concentrating on the syntax, rather than your requirements
property a_stable;
bit[3:0] v;
($rose(B), v=$past(a)) // when B rises, v=a from cycle before
|-> ##[2:3] a==v;
endproperty
THe RHS is not fullfilling the requirement .
The requirement was after asserting signal ‘B’ , then 2/3 clk cycle delay value of ‘A’ need to be checked with previous value of ‘A’ i.e. before fell of signal 'B' ie before last dessert of 'B'. I think somthing like below will be the requirements for same: property a_stable; bit[3:0] v; (b!=4'b0000, v=a) ##1 !b[*0:] ##1 $rose(b) |->##2:4;
endproperty
If this is what you want, then you’ll need a first_match()
property a_stable;
bit[3:0] v;
first_match((b!=4'b0000, v=a) ##1 !b[*0:$] ##1 $rose(b))
|->##[2:4](a==v);
endproperty
Ben Cohen SystemVerilog.us