In reply to feiphung:
That tool is more academic and “Yosys does not support SVA properties!”
Obviously, it is more practical to use SVA concurrent assertions with assumes to define the requirements and the restrictions. The definition you wrote is very hard to follow.
Commercial formal verification tools do use SVA and PSL.
Ben SystemVerilog.us