ANSI-C bounded model checker and hardware verification using CBMC
Xiang Li · Computer and Information Technology · 2005
It is essential to examinate software. This article describes a tool that formally verifies ANSI-C programs. The tool implements a technique called Bounded Model Checking(BMC). It can verify the consistency of the HDL implementation. This paper first introduces the function and usage of CBMC and its installation under windows especially then uses CBMC to check a circuit with the Verilog language the example indicate the usage of hardware verification using CBMC.