Rewriting semantics of production rule sets

Michael Katelman, Sean Keller, José Meseguer

Research output: Contribution to journalArticle

Abstract

This paper is about the semantics of production rule sets, a language used to model asynchronous digital circuits. Two formal semantics are developed and proved equivalent: a set-theoretic semantics that improves upon an earlier effort of ours, and an executable semantics in rewriting logic. The set-theoretic semantics is especially suited to meta-level proofs about production rule sets, whereas the executable semantics can be used with existing tools to establish, automatically, desirable properties of individual circuits. Experiments involving several small circuits are detailed wherein the executable semantics and the rewriting logic tool Maude are used to automatically check two important properties: hazard and deadlock freedom. In doing so, we derive several useful optimizations that make automatic checking of these properties more tractable.

Original languageEnglish (US)
Pages (from-to)929-956
Number of pages28
JournalJournal of Logic and Algebraic Programming
Volume81
Issue number7-8
DOIs
StatePublished - Oct 1 2012

Keywords

  • Asynchronous digital circuits
  • Deadlock freedom
  • Formal semantics
  • Formal verification
  • Hazard freedom
  • Quasi-delay-insensitive circuits
  • Rewriting logic semantics

ASJC Scopus subject areas

  • Software
  • Theoretical Computer Science
  • Logic
  • Computational Theory and Mathematics

Fingerprint Dive into the research topics of 'Rewriting semantics of production rule sets'. Together they form a unique fingerprint.

  • Cite this