Translate English requirements into SVA: one-cycle versus bounded response, liveness expressed as bounded safety, and whether reaching an ERROR state is a bug.
Part of Discrete Mathematics for Formal Verification on formal.org.