Formal design of arithmetic circuits based on arithmetic description language
Formal design of arithmetic circuits based on arithmetic description language
复制标题
DOI：
10.1093/ietfec/e89-a.12.3500
复制
发表时间：
2006-12-01
影响因子：
0.5
通讯作者：
Higuchi, Tatsuo
中科院分区：
文献类型：
--
作者：
Homma, Naofumi;Watanabe, Yuki;Higuchi, Tatsuo
本文使用称为Arith的算术描述语言对算术电路进行了形式设计。 Arith中的关键思想是直接用高级数学对象（即数字表示系统和算术操作/公式）来描述算术算法。使用Arith，我们可以提供对算术算法（包括使用非常规数系统的算法算法）的正式描述。另外，可以通过配方操作对等效检查进行正式验证所述的算术算法。经过验证的ARITH描述很容易转换为等效的HDL描述。在本文中，我们还介绍了算术模块生成器的应用程序，该应用程序支持2个操作系统加法器，多手术器和添加器，乘数，恒定的乘数和乘积累加器的多种硬件算法。发电机中包含的Arith语言处理系统验证了正式方法的Arith描述的正确性。结果，我们可以获得高度可靠的算术模块，其函数在算法级别得到了完全验证。
This paper presents a formal design of arithmetic circuits using an arithmetic description language called ARITH. The key idea in ARITH is to describe arithmetic algorithms directly with high-level mathematical objects (i.e., number representation systems and arithmetic operations/formulae). Using ARITH, we can provide formal description of arithmetic algorithms including those using unconventional number systems. In addition, the described arithmetic algorithms can be formally verified by equivalence checking with formula manipulations. The verified ARITH descriptions are easily translated into the equivalent HDL descriptions. In this paper, we also present an application of ARITH to an arithmetic module generator, which supports a variety of hardware algorithms for 2-operand adders, multi-operand adders, multipliers, constant-coefficient multipliers and multiply accumulators. The language processing system of ARITH incorporated in the generator verifies the correctness of ARITH descriptions in a formal method. As a result, we can obtain highly-reliable arithmetic modules whose functions are completely verified at the algorithm level.