| |
Stephen Longfield, Brittany Nkounkou, Rajit Manohar, and Ross Tate
Self-timed chip designs are commonly specified in a high-level
message-passing language called CHP [21]. This language is closely
related to Hoare's CSP [11] 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.
|
|
