Files in this item



application/pdfrewriting_semantics_of_production_rule_sets.pdf (474kB)
(no description provided)PDF


Title:Rewriting Semantics of Production Rule Sets
Author(s):Katelman, Michael; Keller, Sean; Meseguer, José
Subject(s):rewriting logic semantics
production rule sets
asynchronous vlsi
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.
Issue Date:2012-06-10
Citation Info:JLAP
Publication Status:published or submitted for publication
Peer Reviewed:is peer reviewed
Date Available in IDEALS:2012-06-11

This item appears in the following Collection(s)

Item Statistics