Preventing glitches and short circuits in high-level self-timed chip specifications
Abstract
Self-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare's CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware implementations. For example, two processes sending on the same channel at the same time causes glitches and short circuits in the physical chip implementation. If a CHP program maintains certain invariants, such as only one process is sending on any given channel at a time, it can guarantee an error-free execution that behaves much like a CSP program would. In this paper, we present an inferable effect system for ensuring that these invariants hold, drawing from model-checking methodologies while exploiting language-usage patterns and domain-specific specializations to achieve efficiency. This analysis is sound, and is even complete for the common subset of CHP programs without data-sensitive synchronization. We have implemented the analysis and demonstrated that it scales to validate even microprocessors.
References
[1]
J. V. Arthur, P. A. Merolla, F. Akopyan, R. Alvarez, A. Cassidy, S. Chandra, S. K. Esser, N. Imam, W. Risk, D. B. D. Rubin, et al. Building block of a programmable neuromorphic substrate: A digital neurosynaptic core. In International Joint Conference on Neural Networks, 2012.
[2]
D. Borrione, M. Boubekeur, E. Dumitrescu, M. Renaudin, J.-B. Rigaud, and A. Sirianni. An approach to the introduction of formal validation in an asynchronous circuit design flow. In Hawaii International Conference on System Sciences, 2003.
[3]
A. Cerone and G. J. Milne. A methodology for the formal analysis of asynchronous micropipelines. In Formal Methods in Computer-Aided Design, 2000.
[4]
E. M. Clarke, D. E. Long, and K. L. McMillan. Compositional model checking. In LICS, 1989.
[5]
E. M. Clarke, O. Grumberg, and D. Peled. Model Checking. MIT press, 1999.
[6]
E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM, 18(8):453–457, 1975.
[7]
J. C. Ebergen. Translating Programs into Delay-Insensitive Circuits. Centrum voor Wiskunde en Informatica, 1989.
[8]
D. Fang, J. Teifel, and R. Manohar. A high-performance asynchronous FPGA: Test results. In Symposium on Field-Programmable Custom Computing Machines, 2005.
[9]
P. Godefroid, J. van Leeuwen, J. Hartmanis, G. Goos, and P. Wolper. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem. Springer-Verlag, 1996.
[10]
R. Ho, K. W. Mai, and M. A. Horowitz. The future of wires. Proceedings of the IEEE, 89(4):490–504, 2001.
[11]
C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21:666–677, 1978.
[12]
G. J. Holzmann. The SPIN Model Checker: Primer and Reference Manual. Addison-Wesley Professional, 2004.
[13]
ITRS. International Technology Roadmap for Semiconductors: 2012 update, 2012. URL http://www.itrs.net/.
[14]
M. Kishinevsky, A. Kondratyev, A. Taubin, V. Varshavsky, A. Yakovlev, E. Napelbaum, and O. Reva. Concurrent Hardware: The Theory and Practice of Self-Timed Design. John Wiley & Sons, Inc., 1994.
[15]
A. Lines. Pipelined asynchronous circuits. Master’s thesis, California Institute of Technology, 1998.
[16]
S. Longfield, B. Nkounkou, R. Manohar, and R. Tate. Preventing glitches and short circuits in high-level self-timed chip specifications artifact. Cornell University, 2015.
[17]
R. Manohar and A. J. Martin. Quasi-delay-insensitive circuits are Turing-complete. In International Symposium on Advanced Research in Asynchronous Circuits and Systems, 1996.
[18]
A. Martin, A. Lines, R. Manohar, M. Nystrom, P. Penzes, R. Southworth, U. Cummings, and T. K. Lee. The design of an asynchronous MIPS R3000 microprocessor. In Advanced Research in VLSI, 1997.
[19]
A. J. Martin. The probe: An addition to communication primitives. Information Processing Letters, 20(3):125–130, 1985.
[20]
A. J. Martin. Distributed mutual exclusion on a ring of processes. Science of Computer Programming, 5:265–276, 1985.
[21]
A. J. Martin. Compiling communicating processes into delayinsensitive VLSI circuits. Distributed Computing, 1(4):226–234, 1986.
[22]
A. J. Martin. The design of an asynchronous microprocessor. Technical report, California Institute of Technology, 1989.
[23]
A. J. Martin. The limitations to delay-insensitivity in asynchronous circuits. In MIT Conference on Advanced Research in VLSI, 1990.
[24]
The Coq development team. The Coq proof assistant reference manual. LogiCal Project, 2012. Version 8.4.
[25]
M. Mendler and T. Stroup. Newtonian arbiters cannot be proven correct. Formal Methods in System Design, 3(3):233–257, 1993.
[26]
B. Mishra and E. Clarke. Hierarchical verification of asynchronous circuits using temporal logic. Theoretical Computer Science, 38:269– 291, 1985.
[27]
D. E. Muller and W. S. Bartky. A Theory of Asynchronous Circuits. University of Illinois, Graduate College, Digital Computer Laboratory, 1957.
[28]
T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, 1989.
[29]
K. Papadantonakis. Rigorous Analog Verification of Asynchronous Circuits. PhD thesis, California Institute of Technology, 2005.
[30]
A. W. Roscoe, P. H. B. Gardiner, M. H. Goldsmith, J. R. Hulance, D. M. Jackson, and J. B. Scattergood. Hierarchical compression for model-checking CSP or how to check 1020 dining philosophers for deadlock. In Tools and Algorithms for the Construction and Analysis of Systems, 1995.
[31]
B. R. Sheikh and R. Manohar. An operand-optimized asynchronous IEEE 754 double-precision floating-point adder. In ASYNC, 2010.
[32]
S. F. Smith and A. E. Zwarico. Provably correct synthesis of asynchronous circuits. Designing Correct Circuits, 5:237–260, 1992.
[33]
S. F. Smith and A. E. Zwarico. Correct compilation of specifications to deterministic asynchronous circuits. In Formal Methods in System Design, 1995.
[34]
B. Tang, S. Longfield, S. Bhave, and R. Manohar. A low power asynchronous GPS baseband processor. In ASYNC, 2012.
[35]
R. Tate. The sequential semantics of producer effect systems. In POPL, 2013.
[36]
V. Tiwari, D. Singh, S. Rajgopal, G. Mehta, R. Patel, and F. Baez. Reducing power in high-performance microprocessors. In Design Automation Conference, 1998.
[37]
M. van der Goot. Semantics of VLSI Synthesis. PhD thesis, California Institute of Technology, 1995.
[38]
T. Verhoeff. Delay-insensitive codes – an overview. Distributed Computing, 3(1):1–8, 1988.
Index Terms
- Preventing glitches and short circuits in high-level self-timed chip specifications
Recommendations
Preventing glitches and short circuits in high-level self-timed chip specifications
PLDI '15: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and ImplementationSelf-timed chip designs are commonly specified in a high-level message-passing language called CHP. This language is closely related to Hoare's CSP except it admits erroneous behavior due to the necessary limitations of efficient hardware ...
Optimization of NULL convention self-timed circuits
Self-timed logic design methods are developed using Threshold Combinational Reduction (TCR) within the NULL Convention Logic (NCL) paradigm. NCL logic functions are realized using 27 distinct transistor networks implementing the set of all functions of ...
A pulse-to-static conversion latch with a self-timed control circuit
ICCD '97: Proceedings of the 1997 International Conference on Computer Design (ICCD '97)The design and experimental demonstration of a low-power pulse-to-static conversion latch circuit is described. The circuit includes self-timed control and a 64-bit latch array, both designed utilizing self-resetting CMOS (SRCMOS) circuit techniques. ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2015
630 pages
June 2015630 pages
Copyright © 2015 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 03 June 2015
Published in SIGPLAN Volume 50, Issue 6
Check for updates
Author Tags
Qualifiers
- Research-article
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 187Total Downloads
- Downloads (Last 12 months)8
- Downloads (Last 6 weeks)3
Reflects downloads up to 20 Nov 2024
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in