• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Proof-automation
      • Gl
      • Witness-cp
      • Ccg
      • Install-not-normalized
      • Rewrite$
      • Removable-runes
      • Fgl
      • Efficiency
      • Rewrite-bounds
      • Bash
      • Def-dag-measure
      • Bdd
      • Remove-hyps
      • Contextual-rewriting
      • Simp
      • Rewrite$-hyps
      • Bash-term-to-dnf
      • Use-trivial-ancestors-check
      • Minimal-runes
      • Clause-processor-tools
        • Rp-rewriter
          • Rp-ruleset
          • Defthmrp
          • Rp-rewriter/meta-rules
          • Rp-utilities
          • Rp-rewriter-demo
          • Rp-rewriter/debugging
          • Rp-rewriter/applications
            • Vescmul
              • Multiplier-verification-demo-2
              • Vescmul-heuristics
                • Multiplier-verification-heuristics
                • Vescmul-verify
                • Multiplier-verification-demo-3
                • Vesmul-parse
                • Multiplier-verification-demo-1
              • Svex-simplify
              • Multiplier-verification
        • Fn-is-body
        • Without-subsumption
        • Rewrite-equiv-hint
        • Def-bounds
        • Rewrite$-context
        • Try-gl-concls
        • Hint-utils
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Vescmul-heuristics

    Multiplier-verification-heuristics

    Verified Implementation of S-C-Rewriting algorithm for Multiplier Verification

    See vescmul-heuristics