Checkers / models

In reply to ben@SystemVerilog.us:

After reviewing your reply, Let me know if the following statements are accurate…

An assertion can be made at several levels, and described with little to no wiggle-room for misunderstanding, using SVA (as one method).

There can be assertions based on requirements; these assertions are independent of architecture or implementation.

There can ALSO be assertions placed on low-level design constructs as the designer sees fit (writing a full-FIFO is not allowed). It has zip to do with the DUT requirements, but it enforces healthy RTL behavior according to the implementer. These assertions are tightly coupled / dependent on architecture or implementation. Do these have a special name?