Basic production rules are written as follows:
(Reference to lines of grammar...) (Denotational semantics, type-inference later...)
The dir is either + (pull-up) or - (pull-down). A literal is an occurence of a (bool) node on the left-hand-side of a production rule. A PRS literal and the right-hand-side node must be a refer to a single (scalar) bool instance. A PRS-expr may be any boolean expression using the operators ~, &, |, and literals. (The unary ~ operator has the highest precedence, and the & operator has higher precedence than the | operator.)
The rule arrow -> can be substituted with one of its shorthand forms. The => arrow automatically generates the complementary rule (pulling on opposite direction) using the DeMorgan inverse of the guard. The #> arrow mirrors the rule pulling in the opposite direction with the same topology but inverted literals, mostly useful for writing C-elements. For example:
x & y & z => w-
x & y & z #> c-
expands to
x & y & z -> w-
~x | ~y | ~z -> w+
x & y & z -> c-
~x & ~y & ~z -> c+
Rules involving internal nodes may only use the plain -> notation PRS Internal Nodes.
Since production rules are an abstract description of logic, the rules themselves need not be CMOS-implementable. Enforcement of CMOS-implementability can be introduced by later tools or compiler phases where desired. (TODO: write a CMOS checking pass.)