Modern asynchronous digital circuits are highly concurrent systems composed largely of customized gates, and can be elegantly modeled using the language of
(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
. Our semantics provides a circuit designer with a PR-level circuit interpreter and with a
for checking key circuit properties, including
. 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.