Embedded assertions

An assertion of the form

  assert label: cond;

will evaluate cond whenever it executes (in zero time). If cond is ever false, the property named label is reported to be false. These assertions can be verified formally by SMV.