• Top
    • Documentation
    • Books
    • Recursion-and-induction
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
          • Aignet-impl
          • Node
          • Network
          • Combinational-type
            • Ctype
            • Ctype-equiv
            • Ctype-fix
            • Ctypep
          • Stypep
          • Typecode
        • 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
    • Debugging
    • Projects
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Testing-utilities
    • Math
  • Representation

Combinational-type

Combinational type of a logical AIG node.

Recall that a sequential AIG can be viewed as a combinational AIG by ignoring the distinction between register and primary inputs/outputs.

We can implement the combinational view of AIG nodes by mapping the sequential-type of a node to a combinational type. The valid combinational type keywords are:

  • :const for the special constant node
  • :gate for an AND or XOR gate node
  • :input for a combinational input (primary input or register output)
  • :output for a combinational output (primary input or register input)

Subtopics

Ctype
Map a sequential-type keyword to its combinational-type keywords.
Ctype-equiv
Equivalence relation for combinational-type keywords.
Ctype-fix
Fixing function for combinational-type keywords.
Ctypep
Recognizer for valid combinational-type keywords.