CaltechAUTHORS
  A Caltech Library Service

Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits

Katelman, Michael and Keller, Sean and Meseguer, José (2010) Concurrent Rewriting Semantics and Analysis of Asynchronous Digital Circuits. In: Rewriting Logic and Its Applications. Lecture Notes in Computer Science. No.6381. Springer , Berlin, pp. 140-156. ISBN 978-3-642-16309-8. https://resolver.caltech.edu/CaltechAUTHORS:20200603-081819155

Full text is not posted in this repository. Consult Related URLs below.

Use this Persistent URL to link to this item: https://resolver.caltech.edu/CaltechAUTHORS:20200603-081819155

Abstract

Modern asynchronous digital circuits are highly concurrent systems composed largely of customized gates, and can be elegantly modeled using the language of production rules (PRs). One of the present limitations of the state of the art in asynchronous circuit design is that no formal executable semantics of asynchronous circuits has yet been given at the PR level. The primary contribution of this paper is to define, using rewriting logic and Maude, an executable formal semantics of asynchronous circuits at the PR level under three common timing assumptions. Our semantics provides a circuit designer with a PR-level circuit interpreter and with a decision procedure for checking key circuit properties, including hazard-freedom and deadlock-freedom. We describe several reductions and optimizations that can be used to reduce the state space of circuits in our formal semantics and investigate the impact of these reductions experimentally. The analysis scales up to circuits of over 100 PRs in spite of the high levels of concurrency involved.


Item Type:Book Section
Related URLs:
URLURL TypeDescription
https://doi.org/10.1007/978-3-642-16310-4_10DOIArticle
https://rdcu.be/b4BgYPublisherFree ReadCube access
Additional Information:© 2010 Springer-Verlag Berlin Heidelberg.
Subject Keywords:Model Check; Production Rule; Disjunctive Normal Form; Nand Gate; Asynchronous Circuit
Series Name:Lecture Notes in Computer Science
Issue or Number:6381
Record Number:CaltechAUTHORS:20200603-081819155
Persistent URL:https://resolver.caltech.edu/CaltechAUTHORS:20200603-081819155
Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:103659
Collection:CaltechAUTHORS
Deposited By: Tony Diaz
Deposited On:03 Jun 2020 16:10
Last Modified:03 Jun 2020 16:10

Repository Staff Only: item control page