Reasoning about imperfect digital systems

In order to realise digital systems that operate at high speeds or that have very low power consumptions, it is necessary to work directly at the analog level of abstraction, that is, in terms of analog electronic components such as resistors and transistors. Although the external behaviour of such circuits can be described digitally, their internal operation can only be explained by working at the analog level and by taking account of both voltages and currents. This chapter describes how existing methods of specification and formal verification of digital systems can be extended so as to encompass such analog designs in a fully rigorous manner.