• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
          • Aignet-impl
          • Node
            • Node-fix
            • Node-p
            • Node-equiv
            • Co-node->fanin
            • Gate-node->fanin1
            • Gate-node->fanin0
            • Stype
            • Nxst-node
              • Nxst-node->reg
              • Nxst-node->fanin
            • Node->type
            • Node->regp
            • Xor-node
            • And-node
            • Po-node
            • Proper-node-p
            • Reg-node
            • Pi-node
            • Const-node
          • Network
          • 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
    • Std
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
    • Software-verification
    • Math
    • Testing-utilities
  • Node

Nxst-node

A next-state node for a register.

This is a product type, introduced by fty::defflexsum in support of node.

Fields
fanin — lit
Literal giving the logical function of the next state.
reg — natp
Index (register number, not ID) of the register for which this is the next state.

Subtopics

Nxst-node->reg
Get the reg field from a nxst-node.
Nxst-node->fanin
Get the fanin field from a nxst-node.