Module quaigh::equiv

Equivalence checking

Functions

• check_equivalence_bounded
  Perform bounded equivalence checking on two sequential networks
• check_equivalence_comb
  Perform equivalence checking on two combinatorial networks
• difference
  Create a network with a single output, representing whether two combinatorial networks give different outputs
• prove
  Find an assignment of the inputs that sets the single output to 1
• unroll
  Unroll a sequential network over a fixed number of steps, making a larger combinatorial networks