compilerbitch

Indeed. PE for the simpler classes of circuit is actually pretty straigtforward, and can be easily shown to work. It does get tricky when dealing with asynchronous circuits, however, which I suspect will probably end up taking up more of my time. The problem is that if you don't care about glitches (hazards in some of the EE literature), the familiar axiom of replacement for Boolean expressions is fine. However, if the glitches matter, as they do in many cases inside asynchronous logic, the standard axiom of replacement falls apart and needs to be redefined. I'm fiddling around with a 5-value logic that captures the notion of transitions between states (and their relative cleanliness) -- it looks likely that it will provide a way of defining a hierarchy of alternative axioms of replacement that can be chosen to match the expected semantics of the underlying hardware. It's a bit of a sledgehammer approach in that it is much more general than is really necessary just to support PE, but if it gets the job done I'll be happy!