Development of a ripple carry adder based on theorem prover and exploration of novel chip design method
The scale of digital chip design has entered the era of hundreds of billions of transistors,and traditional hardware design methods struggle to meet the increasingly complex circuit demands,such as those based on the Verilog language.In response to this issue,the article takes the example of a ripple carry adder to explore a chip design method based on the interactive theorem prover Coq.This method not only completes the adder's RTL description in Coq but also encompasses adder functional simulation,formal verification,Verilog code generation,netlist generation,and netlist simulation.This case integrates RTL design with the main front-end EDA processes in a single programming platform.While the case itself is relatively simple,it provides an initial demonstration of the potential of Coq-based chip front-end design.The hope is to use this as a starting point to explore new chip design workflows based on theorem provers.The primary technical approach in the article involves developing an abstract syntax tree for chip design within Coq.Subsequently,the ripple carry adder's front-end development process is unfolded based on this abstract 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.
NETL
NSTL
万方数据
