基于定理证明器的行波进位加法器开发以及新的芯片设计方法探索  

Development of a ripple carry adder based on theorem prover and exploration of novel chip design method

作　　者：孟月华 陈乡栎 陈钢 MENG Yuehua;CHEN Xiangli;CHEN Gang(College of Computer Science and Technology,Nanjing University of Aeronautics and Astronautics,Nanjing 211106,China)

机构地区：[1]南京航空航天大学计算机科学与技术学院,江苏南京211106

出　　处：《微电子学与计算机》2024年第10期95-105,共11页Microelectronics & Computer

摘　　要：数字芯片的规模已经进入几百亿晶体管的时代,传统的硬件设计方法难以应对日益复杂的电路需求,比如基于Verilog语言的硬件设计。针对这个问题,文章以行波进位加法器为例,探索基于交互式定理证明器Coq的芯片设计方法,该方法不仅在Coq中完成了加法器的RTL描述,而且进行了加法器的功能仿真、形式验证、Verilog代码生成、网表生成和网表仿真。这个案例在单一的编程平台里把RTL设计同前端EDA的主要流程整合在一起,虽然案例简单,但可以初步体现出基于Coq的芯片前端设计的可能性,并且希望能够从此出发探索出新的基于定理证明器的芯片设计流程。文章的主要技术路线是在Coq中开发芯片设计的抽象语法树,然后基于这个抽象语法树展开行波进位加法器的前端开发流程。实验结果表明,Coq在支撑芯片设计方面有巨大的潜力,并且基于定理证明器的验证是可以复用的,这有利于验证大规模的系统。尽管这一方法处于探索阶段,但它为未来的芯片前端设计提供了全新的思路,有希望发展成为一种新型的芯片前端设计方法。syntax tree.Experimental results indicate that Coq holds significant potential in supporting chip design,and theorem prover-based verification can be reused,facilitating the verification of large-scale systems.Although this method is still in the exploratory stage,it offers a fresh perspective on future chip front-end design and holds the potential to evolve into a novel chip front-end design methodology.

关 键 词：定理证明器 芯片设计 COQ 行波进位加法器 

分 类 号：TN401[电子电信—微电子学与固体电子学] TN402