How do I write an System Verilog Assertion to prove a signal

[rajatkmitra@gmail.com]

Hello,
I need to write a system verilog assertion that proves that a signal A holds its value for 2 clock cycles..Is this how this is written ??

//this is what the actual code is suppose to do -
//clk_div_2 is clk divided by 2.

always @(posedge clk)
if(clk_div_2)begin
if(enable)
A<= B;
end


Is this the correct way to write the assertion ??
property FOO;
int data;
@(posedge clk)
(enable, data=B) |=> ##2 (A==data);
endproperty

CHECK_FOO:assert_property(FOO);

Thanks for you help,
Raj

 

[Alan Fitch]

On 25/10/14 05:01, rajatkmitra@gmail.com wrote:

Hello,
I need to write a system verilog assertion that proves that a signal A holds its value for 2 clock cycles..Is this how this is written ??

As is usual with assertions, the trick is understanding the spec. From
the sentence you've written, you sound like you want A to have the same
value for two clock cycles. There is no mention of any input data.

//this is what the actual code is suppose to do -
//clk_div_2 is clk divided by 2.

always @(posedge clk)
if(clk_div_2)begin
if(enable)
A<= B;
end

From that code, and your original spec, perhaps you mean:

"if enable is high and clk_div_2 is high in clk 1, then in clk 2 A must
have the same value as it had in clock 1"

i.e.
property p;
@(posedge(clk)
clk_div_2 && enable |=> (A == $past(A));
endproperty

That's the fun thing with assertions - they make you wonder what your
original spec actually means

regards
Alan

P.S. apologies if I've got the detailed syntax wrong, it's from memory.

Is this the correct way to write the assertion ??
property FOO;
int data;
@(posedge clk)
(enable, data=B) |=> ##2 (A==data);
endproperty

CHECK_FOO:assert_property(FOO);

Thanks for you help,
Raj

--
Alan Fitch

 

[rajatkmitra@gmail.com]

On Saturday, October 25, 2014 6:03:44 AM UTC-4, Alan Fitch wrote:

On 25/10/14 05:01, rajatkmitra@gmail.com wrote:
Hello,
I need to write a system verilog assertion that proves that a signal A holds its value for 2 clock cycles..Is this how this is written ??


As is usual with assertions, the trick is understanding the spec. From
the sentence you've written, you sound like you want A to have the same
value for two clock cycles. There is no mention of any input data.

//this is what the actual code is suppose to do -
//clk_div_2 is clk divided by 2.

always @(posedge clk)
if(clk_div_2)begin
if(enable)
A<= B;
end



From that code, and your original spec, perhaps you mean:

"if enable is high and clk_div_2 is high in clk 1, then in clk 2 A must
have the same value as it had in clock 1"

i.e.
property p;
@(posedge(clk)
clk_div_2 && enable |=> (A == $past(A));
endproperty

That's the fun thing with assertions - they make you wonder what your
original spec actually means

regards
Alan

P.S. apologies if I've got the detailed syntax wrong, it's from memory.


Is this the correct way to write the assertion ??
property FOO;
int data;
@(posedge clk)
(enable, data=B) |=> ##2 (A==data);
endproperty

CHECK_FOO:assert_property(FOO);

Thanks for you help,
Raj



--
Alan Fitch

Greetings Alan,
Hope all is well at Doulos... Yes thanks for this ... We are starting to introduce SVA into our tesbench rather extensively .. perhaps we should have you folks come over ans train us ;-)....

-Raj

 

[Alan Fitch]

On 25/10/14 19:37, rajatkmitra@gmail.com wrote:

On Saturday, October 25, 2014 6:03:44 AM UTC-4, Alan Fitch wrote:
snip

Greetings Alan,
Hope all is well at Doulos... Yes thanks for this ... We are starting to introduce SVA into our tesbench rather extensively .. perhaps we should have you folks come over ans train us ;-)....

-Raj

Actually I left Doulos a year ago - but as I worked there for 15
years(!) I would of course recommend their courses

kind regards
Alan

--
Alan Fitch