形式验证(Formal verification)

• 通常(General)
• 形式后端(Formal backend)
• 安装需求(Installing requirements)
• 举例(Example)
  • 一、外部断言(External assertions)
  • 二、内部断言(Internal assertions)
  • 三、外部激励(External stimulus)
  • 四、更多的断言/传递(More assertions/past)
  • 五、假设存储内容(Assuming memory content)
• 实用程序和原语(Utilities and primitives)
  • 一、断言/时钟/复位(Assertions/clock/reset)
  • 二、给定信号初始值(Specifying the initial value of a signal)
  • 三、给定初始化声明(Specifying a initial assumption)
  • 四、存储内容(Memory content)
  • 五、在复位区域内给定断言(Specifying assertion in the reset scope)
  • 六、形式化原语(Formal primitives)
• 限制(Limitations)
  • 四、例子(Example)
  • 五、开发区域(Developers Area)