Assumption in Formal verification

SystemVerilog
1

Hi,
how can we write a assumptions for the following scenario in SVA
signal A,B
if signal A is high then it should be remain high until B becomes 1

Thanks in advance…

Regards,
Siva.

2

In reply to sivareddy437:

assume property (@(posedge clk) $rose(A) |-> A until B);
3

In reply to dave_59:

Thanks Dave,
i used in following way,
assume property (@(posedge clk) $rose(A) |-> A throughout B[->1]);

4

In reply to sivareddy437:

In reply to dave_59:
Thanks Dave,
i used in following way,
assume property (@(posedge clk) $rose(A) |-> A throughout B[->1]);

It’s the same as
assume property (@(posedge clk) $rose(A) |-> A until_with B);