		Search-engine friendly clone of the ACL2 documentation.

Network

Lookup-reg->nxst

Look up the next-state node that corresponds to particular register node.

Signature
(lookup-reg->nxst reg aignet) → nxst-lit
Arguments: reg — Register number for this register.
Guard (natp reg).; aignet — Guard (node-listp aignet).
Returns: nxst-lit — Type (litp nxst-lit).

Note: This is different from the other lookups: it's by ID of the corresponding RO node, not IO number. I think the asymmetry is worth it though.

Definitions and Theorems

Function: lookup-reg->nxst

(defun lookup-reg->nxst (reg aignet)
       (declare (xargs :guard (and (natp reg) (node-listp aignet))))
       (let ((__function__ 'lookup-reg->nxst))
            (declare (ignorable __function__))
            (cond ((endp aignet) 0)
                  ((and (equal (stype (car aignet))
                               (nxst-stype))
                        (b* ((ro (nxst-node->reg (car aignet))))
                            (and (nat-equiv reg ro)
                                 (< ro (stype-count :reg aignet)))))
                   (aignet-lit-fix (nxst-node->fanin (car aignet))
                                   aignet))
                  ((and (equal (stype (car aignet)) (reg-stype))
                        (nat-equiv (stype-count :reg (cdr aignet))
                                   reg))
                   (make-lit (fanin-count aignet) 0))
                  (t (lookup-reg->nxst reg (cdr aignet))))))

Theorem: litp-of-lookup-reg->nxst

(defthm litp-of-lookup-reg->nxst
        (b* ((nxst-lit (lookup-reg->nxst reg aignet)))
            (litp nxst-lit))
        :rule-classes :type-prescription)

Theorem: aignet-litp-of-lookup-reg->nxst

(defthm aignet-litp-of-lookup-reg->nxst
        (aignet-litp (lookup-reg->nxst reg aignet)
                     aignet))

Theorem: lookup-reg->nxst-of-nfix-reg

(defthm lookup-reg->nxst-of-nfix-reg
        (equal (lookup-reg->nxst (nfix reg) aignet)
               (lookup-reg->nxst reg aignet)))

Theorem: lookup-reg->nxst-nat-equiv-congruence-on-reg

(defthm lookup-reg->nxst-nat-equiv-congruence-on-reg
        (implies (nat-equiv reg reg-equiv)
                 (equal (lookup-reg->nxst reg aignet)
                        (lookup-reg->nxst reg-equiv aignet)))
        :rule-classes :congruence)

Theorem: lookup-reg->nxst-of-node-list-fix-aignet

(defthm lookup-reg->nxst-of-node-list-fix-aignet
        (equal (lookup-reg->nxst reg (node-list-fix aignet))
               (lookup-reg->nxst reg aignet)))

Theorem: lookup-reg->nxst-node-list-equiv-congruence-on-aignet

(defthm lookup-reg->nxst-node-list-equiv-congruence-on-aignet
        (implies (node-list-equiv aignet aignet-equiv)
                 (equal (lookup-reg->nxst reg aignet)
                        (lookup-reg->nxst reg aignet-equiv)))
        :rule-classes :congruence)

Theorem: lookup-reg->nxst-id-bound

(defthm lookup-reg->nxst-id-bound
        (<= (lit->var (lookup-reg->nxst n aignet))
            (fanin-count aignet))
        :rule-classes :linear)

Theorem: lookup-reg->nxst-out-of-bounds

(defthm lookup-reg->nxst-out-of-bounds
        (implies (<= (stype-count :reg aignet) (nfix n))
                 (equal (lookup-reg->nxst n aignet) 0)))