新思公开V-SDC验证格式

为了简化形式验证工具的使用而让新思公司开放它的V-SDC格式不仅仅是出于利他主义。这更多的是关系到新思公司的切身利益,因为这么做既可以满足用户要求,还有可能拓宽等效检查工具的市场。

Tcl文件跟踪寄存器名称。

新思公司最近通过Tap-In伙伴项目将V-SDC以开放源码的方式免费向公众提供。V-SDC(“V”代表验证)是被广泛采用的新思设计约束格式(SDC)的扩展,是一种记录实现过程中发生的优化操作的Tcl文件。为了避免进行人工设置,V-SDC必须与等效检查器进行通信。

等效检查器依靠寄存器映射来验证两个设计描述是否等效。等效检查器会把设计分割成若干被寄存器空间限制的逻辑单元。但包括综合和布局在内的实现工具经常会让人毫无知觉地移动、删除、增加或重命名寄存器,进而使用户必须通过冗长的设置过程才能与等效检查器进行通信。

“大量设计优化可以表明,没有预知的更改对等效检查器来说是很大的挑战。”新思公司Formality等效检查器产品行销经理Robert Vallelunga说。他表示,新思公司利用V-SDC格式跟踪综合过程中寄存器的变化,实现了Formality设置的自动化。

结果是许多新思用户希望他们自己的实现工具也能使用V-SDC格式,Vallelunga表示。将V-SDC以开源代码的形式提供给用户后,新思公司就无需再逐个解决这样的用户问题了。

另外一个推动因素是仍有许多ASIC设计师没有使用等效检查,Vallelunga指出。“采用等效检查工具的阻碍之一是等效检查很难设置。”他说,“通过改进设置过程,如果V-SDC开放出来并被其它第三方供应商采纳,那么必将极大地鼓励设计师采用等效检查。”

但在等效检查市场上新思公司的主要竞争对手Cadence设计系统公司并没有购买V-SDC。

“我们认为,如果设计工具把V-SDC中这种未经验证的假设传递给验证工具的话将是十分危险的。”Cadence公司Conformal等效检查器行销部总监Sean Torsney说,“这样的流程会从根本上损害所进行的验证的完整性。”

Torsney 认为,Cadence的开发重点是改进公司的验证工具,使验证工具无需“辅助文件”就能处理复杂的设计。

明导公司非常赞成这样的想法。“确实需要从实现工具那儿交换转换信息来提高等效检查的效率,特别是当逻辑综合器在执行明显有问题的优化的时候。”明导公司0-In产品行销经理Kenneth Larsen说。“提供这些转换信息的开放源码格式对用户群体来说非常有益,”Larsen表示。

使用V-SDC,综合或物理版图工具会把有关寄存器优化的信息记录到Tcl文件,然后等效检查器就可以读取这个文件,这样就不再需要手工提供信息。

在最近的新思互操作性论坛上,Vallelunga描述了可能会给等效检查器造成问题的一些优化。其中之一是无法预料的名称更改。在他引用的一个用户例子中,综合工具以完全随机的方式修改了寄存器的名字,结果导致验证过程中比较点或逻辑单元输出的错误匹配。

另外一个问题是在优化面积或扇出时通常会引起复制或合并寄存器。实现工具经常会修改设计中的寄存器数量,从而会改变等效检查工具正在比较的两个设计之间的逻辑单元数量。寄存器名字可能是匹配的,但功能不再等效,因此验证会失败,使得用户得出错误的结论。

第三个问题是有限状态机的重新编码,这会增加寄存器。默认情况下,工具通常采用二进制编码方式,除非在RTL中明确定义了其它条件。重新编码会改变逻辑单元,从而造成验证失败。

目前新思的Design Compiler和Formality工具都支持V-SDC。不过,要想使用它,还需要可以编写V-SDC的实现工具和可以读取V-SDC的验证工具。在其它EDA供应商对V-SDC提供支持之前,V-SDC仍将主要用于那些拥有自己工具的设计团队。

作者:葛立伟