斷言ASSERTIONS
Simulation Assertions
簡單來說就是利用簡單的語義描述來驗證signals protocol 而這個驗證語法是基於一個或多個clock來確認signals之間的關係
断言被分为两大类：一类是由设计者定义，另一类由验证工程师定义。
● 由设计者定义的设计断言（Implementation Assertion）
通常寫成embedded Mode，而嵌入到RTL中，因為Assertion 不會被合成
● 由验证工程师定义的规范断言（Specification Assertion）
通常會使用blockbox方式來驗證design，常放在design的外部
由於assertion只能指出錯誤，但不能指出少驗了那些項目
因此必須搭配code coverage相關的方法來使用
Formal Assertion Proving
Formal tools called model checker or assertion provers can mathe-matically prove that, given an RTL design and some assumptions
about the relationships of the input signals, an assertion will always
hold true. If a counter example is found, the formal tool will pro-
vide details on the sequence of events that leads to the assertion
violation. It is then up to you to decide if this sequence of events is
possible, given additional knowledge about the environment of the
design.
形式验证领域将这些输入断言称为约束（constraint），这里作者使用术语“假设”（assumption）将其与随机发生
的约束区分开来，后者是一种随机的概念。
這個驗證觀念在2008之後似乎不再有人再提了，
現在的觀念應該是
Formal verification就用formal tools(LEC, formality)之類來作靜態驗證
Assertion就用SVA, PSL, OVL之類來作動態驗證
另一種原因可能是OVM/UVM的出現，而random input及constraints在其中的使用
