• Top
    • Documentation
    • Books
    • Boolean-reasoning
      • Ipasir
      • Aignet
        • Base-api
        • Aignet-construction
        • Representation
        • Aignet-copy-init
        • Aignet-simplify-with-tracking
        • Aignet-simplify-marked-with-tracking
        • Aignet-cnf
        • Aignet-simplify-marked
        • Aignet-complete-copy
        • Aignet-transforms
        • Aignet-eval
          • Vector-simulation
            • Aignet-vecsim
            • Aignet-vecsim1
            • S32v
            • Random-sim
            • Exhaustive-sim
            • S32v-randomize-inputs
            • S32v-randomize-regs
            • Aignet-vecsim-top
        • 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
  • Aignet-eval

Vector-simulation

Simulating the network by running many tests in parallel using vector logic operations

32-bit bitwise logic operations can be used to effectively run 32 ANDs, XORs, or NOTs with one operation, so we can use this to run many evaluations of an AIG very quickly. See subtopics for various utilities.

Subtopics

Aignet-vecsim
Simulate an AIG on N*32 parallel input vectors.
Aignet-vecsim1
Simulate an AIG on 32 parallel input vectors.
S32v
Stobj containing a 2-dimensional array of 32-bit signed integers. Used to store the data for vector-simulation.
Random-sim
Exhaustively simulate an AIG with one output node to determine if it is satisfiable
Exhaustive-sim
Exhaustively simulate an AIG with one output node to determine if it is satisfiable
S32v-randomize-inputs
Assign random values to the PI nodes of an AIG in an s32v
S32v-randomize-regs
Assign random values to the register nodes of an AIG in an s32v
Aignet-vecsim-top
Logically same as aignet-vecsim, but optimizes by calling aignet-vecsim1 when s32v has only 1 column