• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Projects
    • Debugging
    • Std
    • Community
    • Proof-automation
    • Macro-libraries
    • ACL2
    • Interfacing-tools
    • Hardware-verification
      • Gl
      • Esim
      • Vl2014
      • Sv
        • Svex-stvs
          • Svtv-data
          • Defsvtv$
          • Svtv-run
          • Defsvtv-phasewise
          • Svtv
          • Svtv-spec
          • Defsvtv
          • Process.lisp
          • Svtv-doc
          • Svtv-chase$
          • Svtv-versus-stv
          • Svtv-debug-fsm
          • Structure.lisp
          • Svtv-debug
            • Vcd.lisp
            • Debug.lisp
              • Svtv-debug-writephases
              • Svtv-debug-fsm-writephases
              • Svtv-debug-set-ios-logic
              • Svtv-debug-run-fsm
              • Svtv-debug-fsm-core
              • Svtv-debug-run-logic
              • Svtv-debug-init
              • Svtv-debug-eval-aliases-track
              • Svtv-debug-core
                • Svtv-debug-set-svtv
                • Svtv-debug-lhs-eval
                • Svtv-debug-eval-aliases
                • Svtv-debug-set-ios
                • Svtv-debug-run
                • Debugdata-status-p
            • 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
        • Fgl
        • Vwsim
        • Vl
        • X86isa
        • Svl
        • Rtl
      • Software-verification
      • Math
      • Testing-utilities
    • Debug.lisp

    Svtv-debug-core

    Signature
    (svtv-debug-core x inalist 
                     &key (filename '"svtv-debug.vcd") 
                     (moddb 'moddb) 
                     (aliases 'aliases) 
                     (debugdata 'debugdata) 
                     (vcd-wiremap 'vcd-wiremap) 
                     (vcd-vals 'vcd-vals) 
                     (rewrite 't) 
                     (state 'state)) 
     
      → 
    (mv moddb aliases debugdata vcd-wiremap vcd-vals state)
    Arguments
    x — Guard (svtv-p x).
    inalist — Guard (svex-env-p inalist).
    filename — Guard (stringp filename).

    Definitions and Theorems

    Function: svtv-debug-core-fn

    (defun svtv-debug-core-fn
           (x inalist filename moddb aliases debugdata
              vcd-wiremap vcd-vals rewrite state)
     (declare
          (xargs :stobjs (moddb aliases
                                debugdata vcd-wiremap vcd-vals state)))
     (declare (xargs :guard (and (svtv-p x)
                                 (svex-env-p inalist)
                                 (stringp filename))))
     (let ((__function__ 'svtv-debug-core))
      (declare (ignorable __function__))
      (b*
       (((svtv x))
        (mod-fn
          (intern-in-package-of-symbol (cat (symbol-name x.name) "-MOD")
                                       x.name))
        ((mv err design)
         (magic-ev-fncall mod-fn nil state t t))
        ((when err)
         (raise "Error: couldn't run ~x0: ~@1~%"
                mod-fn err)
         (mv moddb aliases
             debugdata vcd-wiremap vcd-vals state))
        ((unless (and (design-p design)
                      (modalist-addr-p (design->modalist design))))
         (raise "Error: ~x0 returned a malformed design~%"
                mod-fn)
         (mv moddb aliases
             debugdata vcd-wiremap vcd-vals state))
        ((mv err moddb aliases debugdata)
         (svtv-debug-init design))
        ((when err)
         (mv moddb aliases
             debugdata vcd-wiremap vcd-vals state))
        (debugdata (svtv-debug-set-svtv x
                                        :rewrite rewrite))
        ((mv vcd-wiremap vcd-vals state)
         (svtv-debug-run-logic inalist
                               :filename filename)))
       (mv moddb aliases
           debugdata vcd-wiremap vcd-vals state))))

    Theorem: svtv-debug-core-fn-of-svtv-fix-x

    (defthm svtv-debug-core-fn-of-svtv-fix-x
     (equal (svtv-debug-core-fn (svtv-fix x)
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)
            (svtv-debug-core-fn x
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)))

    Theorem: svtv-debug-core-fn-svtv-equiv-congruence-on-x

    (defthm svtv-debug-core-fn-svtv-equiv-congruence-on-x
     (implies
       (svtv-equiv x x-equiv)
       (equal
            (svtv-debug-core-fn x
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)
            (svtv-debug-core-fn x-equiv
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)))
     :rule-classes :congruence)

    Theorem: svtv-debug-core-fn-of-svex-env-fix-inalist

    (defthm svtv-debug-core-fn-of-svex-env-fix-inalist
     (equal (svtv-debug-core-fn x (svex-env-fix inalist)
                                filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)
            (svtv-debug-core-fn x
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)))

    Theorem: svtv-debug-core-fn-svex-env-equiv-congruence-on-inalist

    (defthm svtv-debug-core-fn-svex-env-equiv-congruence-on-inalist
     (implies
       (svex-env-equiv inalist inalist-equiv)
       (equal
            (svtv-debug-core-fn x
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)
            (svtv-debug-core-fn x inalist-equiv
                                filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)))
     :rule-classes :congruence)

    Theorem: svtv-debug-core-fn-of-str-fix-filename

    (defthm svtv-debug-core-fn-of-str-fix-filename
     (equal (svtv-debug-core-fn x inalist (str-fix filename)
                                moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)
            (svtv-debug-core-fn x
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)))

    Theorem: svtv-debug-core-fn-streqv-congruence-on-filename

    (defthm svtv-debug-core-fn-streqv-congruence-on-filename
     (implies
       (acl2::streqv filename filename-equiv)
       (equal
            (svtv-debug-core-fn x
                                inalist filename moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)
            (svtv-debug-core-fn x inalist
                                filename-equiv moddb aliases debugdata
                                vcd-wiremap vcd-vals rewrite state)))
     :rule-classes :congruence)