当前位置: 首页 > 产品中心

产品中心

产品中心


ATEC用于验证两个模型是否等价。 它采用形式化方法,类似于formality(Synopsys)。简单说,ATEC会读入参考和实现的源程序,根据程序语言的语义,建立形式化模型,并利用多种数理逻辑/代数方法,证明两个模型是否相等。

若证明成功:则两个模型相等。即:对于所有可能的输入,两个模型输出都相同。 若证明失败:ATEC会给出导致不等的反例(输入激励),用于侦错(debug)。

 ATEC支持验证:

(1)   C/C++到C/C++的等价性:

证明两个C程序之间的等价性;

(2)    C/C++到Verilog的等价性:

用户编写或转化的Verilog程序与标准C模型的等价性;

(3)   Veirlog到Verilog的等价性:

Clock Gating等价验证,任意两个(部分)相等RTL程序等价验证。

ATEC支持标准的C/C++语言以及1995/2001 Verilog标准。ATEC的编译器把程序首先转化成一种内部定义的中间表达,该表达随后被翻译成统一的形式化模型。ATEC专有算法会建立两个模型之间的对应,调用多种优化技术,对其求解。ATEC后端形式化求解引擎的输入是两个形式化模型。ATEC专有算法会建立两个模型之间的对应,调用多种优化技术,对其求解。

ATEC的自定义内部表达支持语言的紧凑表示,可以支持将近上百万行的程序表示。ATEC优化形式化验证引擎可以求解千万级节点数的问题求解。逻辑错误大部分在10分钟之内找到,对于浮点优化的引擎可以完成大部分浮点运算的自动证明。

©2015 南京创联智软信息科技有限公司 版权所有 南京网站建设:南京同网