• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
      • Svex-simplify
      • Svl-flatten-design
      • Svl-run
        • Svl-run-phase
        • Svl-run-phase-wog
      • Svl-run->svex-alist
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Svl-run
• Svl-run-phase

Svl-run-phase-wog

Same as svl-run-phase but without guards

Signature

(svl-run-phase-wog modname inputs delayed-env modules) 
  → 
(mv * *)

Please see svl-run-phase for the explanation of the arguments. svl-run-phase-wog has the same functionality as svl-run-phase but it does not have any guards. This can help makes the rewrite-based proof go faster because guards might be executed too many times during such proofs.