Department of Computer Science and Technology

Technical reports

On the application of program analysis and transformation to high reliability hardware

Sarah Thompson

July 2006, 215 pages

This technical report is based on a dissertation submitted April 2006 by the author for the degree of Doctor of Philosophy to the University of Cambridge, St Edmund’s College.

DOI: 10.48456/tr-670

Abstract

Safety- and mission-critical systems must be both correct and reliable. Electronic systems must behave as intended and, where possible, do so at the first attempt – the fabrication costs of modern VLSI devices are such that the iterative design/code/test methodology endemic to the software world is not financially feasible. In aerospace applications it is also essential to establish that systems will, with known probability, remain operational for extended periods, despite being exposed to very low or very high temperatures, high radiation, large G-forces, hard vacuum and severe vibration.

Hardware designers have long understood the advantages of formal mathematical techniques. Notably, model checking and automated theorem proving both gained acceptance within the electronic design community at an early stage, though more recently the research focus in validation and verification has drifted toward software. As a consequence, the newest and most powerful techniques have not been significantly applied to hardware; this work seeks to make a modest contribution toward redressing the imbalance.

An abstract interpretation-based formalism is introduced, transitional logic, that supports formal reasoning about dynamic behaviour of combinational asynchronous circuits. The behaviour of majority voting circuits with respect to single-event transients is analysed, demonstrating that such circuits are not SET-immune. This result is generalised to show that SET immunity is impossible for all delay-insensitive circuits.

An experimental hardware partial evaluator, HarPE, is used to demonstrate the 1st Futamura projection in hardware – a small CPU is specialised with respect to a ROM image, yielding results that are equivalent to compiling the program into hardware. HarPE is then used alongside an experimental non-clausal SAT solver to implement an automated transformation system that is capable of repairing FPGAs that have suffered cosmic ray damage. This approach is extended to support automated configuration, dynamic testing and dynamic error recovery of reconfigurable spacecraft wiring harnesses.

Full text

PDF (5.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-670,
  author =	 {Thompson, Sarah},
  title = 	 {{On the application of program analysis and transformation
         	   to high reliability hardware}},
  year = 	 2006,
  month = 	 jul,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-670.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-670},
  number = 	 {UCAM-CL-TR-670}
}