Until with

Syntax at a glance

a until_with b

How it works

Until with is a future temporal concept and is not accepted by the current parser. It introduces an inclusive waiting requirement: a condition remains required through the sample where a terminating condition occurs. This is the distinction to study before using it in a full SVA environment.

Suppose a request must remain high while a transaction waits for done. An inclusive requirement also needs that request high on the done sample. A trace where the request drops exactly as done rises illustrates why inclusion of the final sample matters.

The related until concept differs in whether the waiting condition is required at that terminating sample. Separately, the choice of a weak or strong form affects whether the terminating event must eventually occur. Do not equate the word until with an unconditional guarantee of eventual completion.

Full handling requires temporal property semantics beyond this lab's Boolean antecedents and bounded sequences. These records reserve a place in the reference for future lessons; they do not unlock new executable grammar. Current exercises should use supported Boolean conditions, sampled-value functions, and bounded delays with clearly specified endpoints.