• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
          • Aignet-case
            • Aignet-init
            • Aignet-add-xor
            • Aignet-add-and
            • Gate-id->fanin1
            • Gate-id->fanin0
            • Ci-id->ionum
            • Literal
            • Aignet-set-nxst
            • Aignet-clear
            • Aignet-add-out
            • Regnum->nxst
            • Id->slot1
            • Id->phase
            • Num-regs
            • Num-ins
            • Num-fanins
            • Id->slot0
            • Regnum->id
            • Id->type
            • Id->regp
            • Outnum->fanin
            • Innum->id
            • Id-existsp
            • Aignet-add-reg
            • Aignet-add-in
            • Num-gates
            • Aignet-rollback
            • Num-outs
            • Num-nxsts
            • Fanin-litp
          • Aignet-construction
          • Representation
          • Aignet-copy-init
          • Aignet-simplify-marked-with-tracking
          • Aignet-cnf
          • Aignet-simplify-with-tracking
          • Aignet-complete-copy
          • Aignet-eval
          • Semantics
          • Aignet-transforms
          • Aignet-simplify-marked
          • Aignet-read-aiger
          • Aignet-write-aiger
          • Aignet-abc-interface
          • Utilities
        • Aig
        • Satlink
        • Truth
        • Ubdds
        • Bdd
        • Faig
        • Bed
        • 4v
      • Projects
      • Debugging
      • Std
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Testing-utilities
      • Math
    • Base-api

    Aignet-case

    Macro for node type case splits.

    Basic example:

    (aignet-case typecode reg-bit
      :pi ...
      :reg ...
      :and ...
      :xor ...
      :const ...)

    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:

    (aignet-case typecode
      :ci ...
      :gate ...
      :const ...)

    Definitions and Theorems

    Function: keyword-value-keys

    (defun keyword-value-keys (x)
           (declare (xargs :guard (keyword-value-listp x)))
           (if (atom x)
               nil
               (cons (car x)
                     (keyword-value-keys (cddr x)))))