Macro for node type case splits.
(aignet-case typecode reg-bit
Where typecode is the typecode for this node, i.e., it is a
number, not a sequential-type keyword, and where reg-bit is a
bitp such as from regp.
An :otherwise keyword can be provided to cover all the cases not mentioned.
Alternately, you can combine:
- The :pi and :reg (register output) cases into a
:ci (combinational input) or :in case.
- The :po and :nxst (register input) cases into a
:co (combinational output) or :out case.
- The :and and :xor cases into a :gate case.
If none of :pi, :reg, :po, :nxst, :and, or
:xor are used, then the reg-bit argument may be skipped. If it is
provided anyway, it will be ignored in that case.
That is, using this combined syntax you can write:
Definitions and Theorems
(defun keyword-value-keys (x)
(declare (xargs :guard (keyword-value-listp x)))
(if (atom x)
(cons (car x)
(keyword-value-keys (cddr x)))))