...
...
Papers:
[FMSD’12]
Constructive Boolean circuits and the exactness of timed ternary simulation
M. Mendler, T. R. Shiple, G. Berry.
Formal Methods in System Design (FMSD), Volume 40, Issue 3, June 2012: 283-329.
Abstract. We classify gate level circuits with cycles based on their stabilization behavior. We define a formal class of combinational circuits, the constructive circuits, for which signals settle to a unique value in bounded time, for any input, under a simple conservative delay model, called the up-bounded non-inertial (UN) delay. Since circuits with combinational cycles can exhibit asynchronous behavior, such as non-determinism or metastability, it is crucial to ground their analysis in a formal delay model, which previous work in this area did not do.
We prove that ternary simulation, such as the practical algorithm proposed by Malik, decides the class of constructive circuits. We prove that three-valued algebra is able to maintain correct and exact stabilization information under the UN-delay model, and thus provides an adequate electrical interpretation of Malik’s algorithm, which has been missing in the literature. Previous work on combinational circuits used the upbounded inertial (UI) delay to justify ternary simulation. We show that the match is not exact and that stabilization under the UI-model, in general, cannot be decided by ternary simulation. We argue for the superiority of the UN-model for reasons of complexity, compositionality and electrical adequacy. The UN-model, in contrast to the UI-model, is consistent with the hypothesis that physical mechanisms cannot implement non-deterministic choice in bounded time.
As the corner-stone of our main results we introduce UN-Logic, an axiomatic specification language for UN-delay circuits that mediates between the real-time behavior and its abstract simulation in the ternary domain. We present a symbolic simulation calculus for circuit theories expressed in UN-logic and prove it sound and complete for the UN-model. This provides, for the first time, a correctness and exactness result for the timing analysis of cyclic circuits. Our algorithm is a timed extension of Malik’s pure ternary algorithm and closely related to the timed algorithm proposed by Riedel and Bruck, which however was not formally linked with real-time execution models.
[DATE’13]
Sequentially Constructive Concurrency: A Conservative Extension of the Synchronous Model of Computation. (slides)
R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brian.
Design, Automation Test in Europe Conference (DATE’13), March 2013: 581-586.
...
A Game Semantics for Instantaneous Esterel Reactions. (pdf)
J. Aguado.
CSI Journal of Computing (CSIJC). Vol.2, No.1-2, e-ISSN 2277-7091, 2013: 30-44.
...
Grounding Synchronous Deterministic Concurrency in Sequential Programming. (slides)
J. Aguado, M. Mendler, R. von Hanxleden, I. Fuhrmann.
Proceedings of the 23rd European Symposium on Programming (ESOP'14), April 2014: 229-248.
...
SCCharts: Sequentially Constructive Statecharts for Safety-Critical Applications (HW/SW-Synthesis for a Conservative Extension of Synchronous Statecharts).
R. von Hanxleden, B. Duderstadt, C. Motika, S. Smyth, M. Mendler, J. Aguado, S. Mercer, O. O'Brian.
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI’14), June 2014.
...
Sequentially Constructive Concurrency—A Conservative Extension of the Synchronous Model of Computation.
R. von Hanxleden, M. Mendler, J. Aguado, B. Duderstadt, I. Fuhrmann, C. Motika, S. Mercer, O. O'Brian, P. Roop.
ACM Transactions on Embedded Computing Systems (ACM TECS) - Special Issue on Applications of Concurrency to System Design, to appear 2014.
...