• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Fgl
      • Fgl-rewrite-rules
      • Fgl-function-mode
      • Fgl-object
      • Fgl-solving
      • Fgl-handling-if-then-elses
      • Fgl-getting-bits-from-objects
      • Fgl-primitive-and-meta-rules
      • Fgl-counterexamples
      • Fgl-interpreter-overview
      • Fgl-correctness-of-binding-free-variables
      • Fgl-debugging
        • Fgl-support-vars
        • Fgl-gatecount
        • Save-fgl-stack
      • Fgl-testbenches
      • Def-fgl-boolean-constraint
      • Fgl-stack
      • Fgl-rewrite-tracing
      • Def-fgl-param-thm
      • Def-fgl-thm
      • Fgl-fast-alist-support
      • Fgl-array-support
      • Advanced-equivalence-checking-with-fgl
      • Fgl-fty-support
      • Fgl-internals
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Fgl-debugging

Save-fgl-stack

Save the FGL stack to a state global for easy inspection.

Saves the stack from the fgl-interpreter-state into an ACL2 state global, :stack by default and otherwise controlled by the :to keyword argument. Examples of usage:

(fgl::save-fgl-stack)               ;; accessed via (@ :stack)
(fgl::save-fgl-stack :to :my-stack) ;; accessed via (@ :my-stack)
(fgl::save-fgl-stack :to a-stack)   ;; accessed via (@ a-stack)

;; if somehow you need to access the stack in an
;; interpreter state other than @('fgl::interp-st'):
(fgl::save-fgl-stack :to :my-stack :interp-st my-interp-st)

;; inspect the bottom 20 frames of the stack:
(nthcdr (- (len (@ :stack)) 20) (@ :stack))