• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
          • Aignet-impl
          • Node
          • Network
            • Lookup-id
            • Lookup-stype
            • Aignet-extension-p
            • Aignet-nodes-ok
            • Aignet-outputs-aux
            • Aignet-nxsts-aux
            • Fanin
            • Aignet-outputs
            • Lookup-reg->nxst
              • Aignet-lit-fix
              • Aignet-fanins
              • Stype-count
              • Aignet-nxsts
              • Aignet-idp
              • Aignet-norm
              • Aignet-norm-p
              • Aignet-id-fix
              • Fanin-count
              • Proper-node-listp
              • Fanin-node-p
              • Node-list
              • Aignet-litp
            • Combinational-type
            • Typecode
            • Stypep
          • Aignet-copy-init
          • Aignet-simplify-with-tracking
          • Aignet-simplify-marked-with-tracking
          • Aignet-cnf
          • Aignet-simplify-marked
          • Aignet-complete-copy
          • Aignet-transforms
          • Aignet-eval
          • Semantics
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Community
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • 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)))