Digital Circuit Functional Verification(十五)

斷言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在其中的使用