Recall that safety properties (henceforth and unless) are checked with
reference to the <#284#>prop<#284#> declarations in <#285#>sample.sf<#285#>. For
example, to check property S5 below, the following atomic <#286#>prop<#286#>
decalarations are made in <#287#>sample.sf<#287#>:
verbatim112#
verbatim113#
All the above properties are valid except for S4 and S8. VERIFY
produces a failing state for S4 and S8 (pressing ``;'' returns all the
other failing states). These failing states can help the designer
debug the TTM design.