Formalizing abstraction mechanisms for hardware verification in higher order logic

Thomas Frederick Melham
Recent advances in microelectronics have given designers of digital hardware the potential to build devices of remarkable size and complexity. Along with this however, it becomes increasingly difficult to ensure that such systems are free from design errors, where complete simulation of even moderately sized circuits is impossible. One solution to these problems is that of hardware verification, where the functional behaviour of the hardware is described mathematically and formal proof is used to show...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.