Signal checking

Hi All,
I have two signals A and B. when the reset is high, A can not be unknown. When the reset is high and A is 1, B can not be unknown.
So, I write two property.

property @(posedge clk) disable iff (~reset) !$isunknown(A) endproperty
property @(posedge clk) disable iff(~reset) A |-> !isunknown(B) endproerty

is it possible to write one property only?
Thank you!

One of these should work for you

property p1; 
  @(posedge clk) disable iff (~reset)
   !$isunknown(A) and ((A |-> !$isunknown(B))) ; 
endproperty   
property p2; 
  @(posedge clk) disable iff (~reset) 
   A==0 || A ==1 && !$isunknown(B);
endproperty

1 Like

thanks for reply.
theses two statement are same?
A==0 || A ==1 && !$isunknown(B);
A==0 OR A ==1 && !$isunknown(B);

There is no difference in the two expressions you show. The || and or operators have the least precedence amongst the other operators and both its operands are boolean expressions.

Note that or may be used as an operator between sequences and properties.