format_version: "0.1"
properties:
  - id: P1
    kind: invariant
    expression: "!OneShot || !Sig"
    justification: "The falling-edge one-shot fires only when the signal is (now) low."