How assumptions work in formal tool

SystemVerilog
,
1

Hi,
I want to know more about how assumptions work in Formal tool
Is it advisable to use same signal in antecedent and consequent .
eg -
assume property(@(posedge clk) (a==0)|-> ##1 (a==1)[=1] );

Here my intention was to get signal a asserted for 1 cycle only in whole simulation.
But I am seeing it asserted for 2 back to back cycles .

Kindly help me in what I am doing wrong here.

2

In reply to ashish_banga:


 if signal is one clock cycle wide .  it should toggle only once. 
 it requires some support logic. 
 bit set_a_flag ;
function void set_flag(bit a_flag);
       set_a_flag = a_flag ;
endfunction  

property a_toggle_once ;
@(posedge clk)
 (a==0 ,set_a_flag==0,set_flag(1))|-> ##1 (a==1)[->1] #1 a ==0 ;
endproperty
3

In reply to kddholak:

bit set_a_flag ;
function void set_flag(bit a_flag);
set_a_flag = a_flag ;
endfunction
property a_toggle_once ;
@(posedge clk)
(a==0 ,set_a_flag==0,set_flag(1))|-> ##1 (a==1)[->1] #1 a ==0 ;
endproperty

Your above code won’t compile.It’s illegal to have multiple sequence_expr for a sequence_match_item

4

In reply to kddholak:

I am not asking for alternate solutions. I have figured it out how to do in other ways.
I am asking what my mentioned assume is not working

5

In reply to MICRO_91:

In reply to kddholak:
Your code won’t compile.It’s illegal to have multiple sequence_expr for a sequence_match_item

Is it illegal to have multiple sequence_expr for a sequence_match_item ? What does it mean ?I don’t see any illegal in construct or usage in property.

6

In reply to kddholak:

I don’t see any illegal in construct or usage in property.

I assume you haven’t tried your code . Try it out once

Is it illegal to have multiple sequence_expr for a sequence_match_item ? What does it mean ?

Refer Section 16.10 Local variables , Syntax16-14 of the LRM