A Computational Temporal Logic for Superconducting Accelerators
A Computational Temporal Logic for Superconducting Accelerators
复制标题
DOI：
10.1145/3373376.3378517
复制
发表时间：
2020-03
期刊：
影响因子：
--
通讯作者：
Georgios Tzimpragos;Dilip P. Vasudevan;Nestan Tsiskaridze;George Michelogiannakis;A. Madhavan;Jennifer Volk;J. Shalf;T. Sherwood
中科院分区：
文献类型：
--
作者：
Georgios Tzimpragos;Dilip P. Vasudevan;Nestan Tsiskaridze;George Michelogiannakis;A. Madhavan;Jennifer Volk;J. Shalf;T. Sherwood
超导逻辑提供了以极快的速度执行计算并节省能源的潜力。然而，传统硬件设计所接受的电平驱动逻辑与最引人注目的超导技术自然支持的脉冲驱动逻辑之间存在“语义差距”。与电平信号不同，脉冲只会在瞬间通过通道。安排超导组件网络，使输入脉冲始终同时到达“逻辑门”，以维持仅布尔计算的错觉，这是一个重大的工程障碍。在本文中，我们探索了一种新的、更本土化的超导逻辑计算：到达时间。基于最近基于延迟的计算工作，我们表明超导逻辑可以自然地直接计算脉冲到达之间的时间关系，这些脉冲到达之间的计算关系可以通过对时间的函数扩展来形式化。我们验证了验证社区中使用的谓词逻辑，并且所得架构可以异步运行并描述真实且有用的计算，我们通过详细的模拟电路模型、对我们的抽象的形式分析以及在几个超导加速器的背景下的评估来验证我们的假设。
Superconducting logic offers the potential to perform computation at tremendous speeds and energy savings. However, a "semantic gap" lies between the level-driven logic that traditional hardware designs accept as a foundation and the pulse-driven logic that is naturally supported by the most compelling superconducting technologies. A pulse, unlike a level signal, will fire through a channel for only an instant. Arranging the network of superconducting components so that input pulses always arrive simultaneously to "logic gates'' to maintain the illusion of Boolean-only evaluation is a significant engineering hurdle. In this paper, we explore computing in a new and more native tongue for superconducting logic: time of arrival. Building on recent work in delay-based computations we show that superconducting logic can naturally compute directly over temporal relationships between pulse arrivals, that the computational relationships between those pulse arrivals can be formalized through a functional extension to a temporal predicate logic used in the verification community, and that the resulting architectures can operate asynchronously and describe real and useful computations. We verify our hypothesis through a combination of detailed analog circuit models, a formal analysis of our abstractions, and an evaluation in the context of several superconducting accelerators.