SHF: Small:Methodologies and Tools For Verification of Nano-Pipelined Circuits and Systems

纳米技术的持续加速发展预示着未来计算机将真正无处不在。开发微型集成芯片以实现极其复杂的系统的能力将影响从医学到太空探索等人类发展的各个方面。这些应用中的大多数将是安全关键应用，其中故障的成本将导致人员生命损失和极高的经济成本。因此，用于开发可靠和无缺陷设计的纳米级可扩展验证技术是纳米时代数字系统增长和影响的要求。数字化设计中广泛使用的关键优化之一是硬件流水线，其操作类似于流水线化的汽车装配线。纳米级的管道实现非常复杂并且容易出错。本研究旨在开发解决方案，使流水线电路和系统在纳米尺度上的有效和可扩展的验证成为可能。验证解决方案是基于细化的，这是一个等价的概念，用于比较在非常不同的抽象级别上定义的系统。总体方法是使用基于高级改进的转换，以增量步骤减少待验证的纳米流水线电路/系统，使其成为功能等效的非流水线同步机。然后可以使用现有的验证技术轻松地将非流水线机器与高级规格进行比较。

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.