Formal Property Verification

This chapter discusses the concepts and theory behind formal property checking for both hardware and software. It starts with a discussion of the Property Specification Language (PSL), derived from earlier temporal specification languages. It then reviews methods and techniques for hardware formal verification. This is followed by software formal verification, including explicit, symbolic, and bounded model checking. Two update sections cover changes between 2004 and 2015 and improvements from 2016 to 2024, including hardware model checking and the growing interest in software verification and certification.