CHARME: towards formal design and verification for provably correct VLSI hardware
Luc Claesen, D. Borrione, Hans Eveking, George J. Milne, J.-L. Paillet, P. Prinetto · HAL (Le Centre pour la Communication Scientifique Directe) · 1992
This paper presents an overview of the different aspects in the area of the formal verification of VLSI hardware. For particular aspects of the problem area the adequate approaches are being addressed. In this respect an overview of major directions and achievements in the area of formal hardware verification as under research in the CHARME ESPRIT Basic Research Action are presented. The partners in this action combine complementary backgrounds of applied electrical engineering, computer science and mathematics in appropriately addressing the problem of the formal verification of VLSI design. All partners are however convinced that formal verification, given the appropriate methodologies, algorithms and formalisms, will find its place in actual CAD systems for industrial hardware designs. Research results include among others a link-up of formal verification tools to VHDL as well as the demonstrated full formal verification of actual VLSI chips of over 32000 transistors from the layout up to high level algorithmic specifications.