I would like to write the following in SVA (SystemVerilog Assertion) format.
signal a should never be 2 until it attains the value 1
How can we do that?
Such a condition requires a state machine, and cannot be done with simple assertions alone. You need to build the state machine, and then make an assertion that certain transitions cannot occur within that state machine.
property p; @(posedge clk) (A != 2) until (A == 1); endproperty assert property (p);