• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
        • Svtv-data
        • Defsvtv$
        • Svtv-run
        • Defsvtv-phasewise
        • Svtv
          • Svtv-chase
            • Svtv-chase-update
            • Svtv-chase-repl1
          • Svtv-p
          • Svtv-to-fsm
          • Make-svtv
          • Svtv-fix
          • Change-svtv
          • Svtv-equiv
          • Svtv->orig-overrides
          • Svtv->orig-internals
          • Svtv->expanded-overrides
          • Svtv->states
          • Svtv->nextstate
          • Svtv->expanded-ins
          • Svtv->outmasks
          • Svtv->outexprs
          • Svtv->orig-outs
          • Svtv->orig-ins
          • Svtv->inmasks
          • Svtv->nphases
          • Svtv->name
          • Svtv->labels
          • Svtv->inmap
          • Svtv->form
        • Svtv-spec
        • Defsvtv
        • Process.lisp
        • Svtv-doc
        • Svtv-chase$
        • Svtv-versus-stv
        • Svtv-debug-fsm
        • Structure.lisp
        • Svtv-debug
        • Def-pipeline-thm
        • Expand.lisp
        • Def-cycle-thm
        • Svtv-utilities
        • Svtv-debug$
        • Defsvtv$-phasewise
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Svtv-chase

Svtv-chase-update

Re-enter the svtv-chase read-eval-print loop, updating the environment but keeping the same SVTV.

Signature

(svtv-chase-update env &key (debugdata 'debugdata) 
                   (moddb 'moddb) 
                   (aliases 'aliases) 
                   (svtv-chase-data 'svtv-chase-data) 
                   (state 'state)) 
 
  → 
(mv new-svtv-chase-data new-state)

Arguments

env — Guard (svex-env-p env).

moddb — Guard (moddb-ok moddb).

Definitions and Theorems

Function: svtv-chase-update-fn

(defun svtv-chase-update-fn
       (env debugdata
            moddb aliases svtv-chase-data state)
 (declare
    (xargs :stobjs (debugdata moddb aliases svtv-chase-data state)))
 (declare (xargs :guard (and (svex-env-p env)
                             (moddb-ok moddb))))
 (declare
   (xargs
        :guard
        (and (open-input-channel-p *standard-oi*
                                   :object state)
             (< (debugdata->modidx debugdata)
                (moddb->nmods moddb))
             (<= (moddb-mod-totalwires (debugdata->modidx debugdata)
                                       moddb)
                 (aliass-length aliases)))))
 (let ((__function__ 'svtv-chase-update))
  (declare (ignorable __function__))
  (b*
   ((evaldata (svtv-chase-inalist-to-evaldata env))
    (svtv-chase-data
         (set-svtv-chase-data->stack nil svtv-chase-data))
    (svtv-chase-data
         (set-svtv-chase-data->evaldata evaldata svtv-chase-data))
    (svtv-chase-data
         (set-svtv-chase-data->smartp t svtv-chase-data))
    (svtv-chase-data
      (set-svtv-chase-data->assigns
           (make-fast-alist (debugdata->override-assigns debugdata))
           svtv-chase-data))
    (svtv-chase-data
         (set-svtv-chase-data->delays
              (make-fast-alist (debugdata->delays debugdata))
              svtv-chase-data))
    (svtv-chase-data
         (set-svtv-chase-data->modidx (debugdata->modidx debugdata)
                                      svtv-chase-data))
    (- (cw! "Entering SVTV-CHASE Read-Eval-Print Loop~%")
       (cw! "Enter X to exit~%")
       (cw! "Enter ? for command list~%"))
    ((mv svtv-chase-data state)
     (svtv-chase-repl)))
   (mv svtv-chase-data state))))