This is a program of research and education centered on development of efficient, formally verified CAD tools for high-level synthesis and codesign of digital systems. The notion here is to develop CAD tools which are, themselves, formally verified and guaranteed to synthesize correct designs. This eliminates the need for designers to master application of formal methods. The aim is to produce code running on an embedded processor and custom hardware on field programmable gate arrays. The tools are designed to partition a design into hardware and software components, to generate microprocessor code, and to do high-level synthesis. Verification is done by providing semantic models for the representation languages used in the system (behavioral specification, register- transfer level description, gate-level circuit, machine code) and proving that the tools produce designs whose meanings are refinements of the meanings of their specifications. Theoretical and practical classroom courses which compliment this research are being developed.
