The continuing and accelerated advancement of nanotechnology promises a future in which computing will be truly ubiquitous. The ability to develop minuscule Integrated Chips that implement exceedingly complex systems will impact all aspects of human development ranging from medicine to space exploration. A majority of these applications will be safety critical applications in which the cost of failure will result in loss of human life and exceedingly high economic costs. Scalable verification technology at the nanoscale for developing reliable and bug-free designs is therefore a requirement for the growth and impact of digital systems in the nano-era. One of the key optimizations used extensively in digital design is hardware pipelining, which is similar in operation to the pipelined automotive assembly line. Pipeline implementations at the nanoscale are very complex and prone to errors.
This research seeks to develop solutions to enable efficient and scalable verification of pipelined circuits and systems at the nanoscale. The verification solutions are based on refinement, a notion of equivalence used to compare systems defined at very disparate levels of abstraction. The overall approach is to use high-level refinement-based transformations to reduce the nano-pipelined circuit/system to be verified, in incremental steps, to a functionally equivalent non-pipelined synchronous machine. The non-pipelined machine can then be easily compared with high-level specifications using existing verification techniques.
