大家好，欢迎来到IT知识分享网。
Formality基本原理
简单说明一下Containers含义：一般我们的RTL可能就是纯的RTL代码，但网表里面包含各种门，因此工具对比时就需要进行参照，故需要有一个容器把所有相关的文件放在一个容器里；
形式验证就是一个等价性检查：
①首先假设我们的参考设计是功能正确的；
②确认implementation dasign是不是功能等价于参考设计，如果有功能不同的地方，需要举例出来说明；
③形式验证是利用数学模型把所有的可能性都拿出来进行对比(遍历的)，不会漏掉任何的corner case；
④是一种静态验证，并不需要测试向量；
哪些地方需要形式验证？—只要我们的设计形式发生了变化，就需要形式验证；
我们可以每变化一次形式就验证一次，也可以只将开头和最终的结尾形式进行验证，但这样的验证因为形式变化太大了，工具可能要跑很久，甚至可能无法完成验证，所以最好还是一步一步验证，这样每一步都验证通过了，最后就是通过的；
Compare Point比较点
形式验证的方法论就是：首先确定设计的顶层input & output，比如有100个Primary input，每个input有两种状态，那么一共就是2^100中可能，工具会对比形式变化前后每种可能对应的输出是否一致，不留死角，如果每种都是一致的，那么我们就可以认为这是功能等价的；
一般来说，芯片如果比较复杂，那么对应的Primary input 可能性就会很多，如果直接对比就会很费时间；因此，常规的做法是把芯片拆分成多个模块，每个模块变化前后分别进行对比，这样的一个模块就叫逻辑锥，逻辑锥的特点就是顶端一个点，这个点就是output compare point，下面的底面就是 input；把一整个芯片分成多个模块就是分成多个逻辑锥的意思；
Logic Cone逻辑锥
免责声明：本站所有文章内容,图片，视频等均是来源于用户投稿和互联网及文摘转载整编而成，不代表本站观点，不承担相关法律责任。其著作权各归其原作者或其出版社所有。如发现本站有涉嫌抄袭侵权/违法违规的内容,侵犯到您的权益，请在线联系站长,一经查实,本站将立刻删除。 本文来自网络,若有侵权，请联系删除，如若转载，请注明出处：https://haidsoft.com/129297.html
