• 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-spec
        • Defsvtv
        • Process.lisp
          • Svtv-compile
          • Defsvtv-events
          • Svtv-compile-lazy
          • Svtv-compile-phase
          • Svtv-compile-phases-lazy
          • Svtv-allphases-inputs
          • Svtv-phase-inputs
          • Svtv-inalist-resolve-unassigned
          • Svtv-simplify-outs/states
          • Svtv-collect-inmap
          • Svar-boolmasks-limit-to-bound-vars
          • Svtv-overrides->assigns
          • Svtv-non-override-test-input-vars
          • Svtv-outputs->outalist
          • Svtv-run-squash-dontcares
          • Svtv-inputs->assigns
          • Svtv-phase-var-assigns
          • Defsvtv-fn
          • Svtv-entries->overrideconds
          • Svtv-entries->vars
          • Svtv-easy-bindings-main
          • Svtv-collect-masks
          • Svtv-baseentry-svex
          • Svtv-init-states
          • Lhs->mask
          • Svtv-easy-bindings-svtv-vars
          • Svtv-autoins-aux
          • Svtv-autohyps-aux
          • Svtv-autobinds-aux
          • Svtv-autoins
          • Svtv-autohyps
          • Svtv-autobinds
          • Fast-alist-free-list
          • Defsvtv-default-names
        • 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

• Process.lisp

Defsvtv-events

Signature

(defsvtv-events svtv design-const define-macros 
                define-mod parents short long) 
 
  → 
*

Arguments

svtv — Guard (svtv-p svtv).

design-const — Guard (symbolp design-const).

Definitions and Theorems

Function: defsvtv-events

(defun defsvtv-events (svtv design-const define-macros
                            define-mod parents short long)
 (declare (xargs :guard (and (svtv-p svtv)
                             (symbolp design-const))))
 (let ((__function__ 'defsvtv-events))
  (declare (ignorable __function__))
  (b*
   (((svtv svtv))
    (name svtv.name)
    (labels svtv.labels)
    (want-xdoc-p (or parents short long))
    (short (cond ((stringp short) short)
                 ((not short) "")
                 (t (progn$ (raise ":short must be a string.")
                            ""))))
    (long (cond ((stringp long) long)
                ((not long) "")
                (t (progn$ (raise ":long must be a string.")
                           ""))))
    (long
     (if (not want-xdoc-p)
         long
      (cat
       "<h3>Simulation Diagram</h3>

<p>This is a <see topic='@(url sv::svex-stvs)'>svex symbolic test vector</see>
defined with @(see sv::defsvtv).</p>"
       (or (svtv-to-xml svtv labels)
           "Error generating diagram")
       long)))
    (stvconst
       (intern-in-package-of-symbol (cat "*" (symbol-name name) "*")
                                    name))
    (modconst (intern-in-package-of-symbol
                   (cat "*" (symbol-name name) "-MOD*")
                   name))
    (name-mod
        (intern-in-package-of-symbol (cat (symbol-name name) "-MOD")
                                     name))
    (name-autohyps (intern-in-package-of-symbol
                        (cat (symbol-name name) "-AUTOHYPS")
                        name))
    (name-autohyps-fn (intern-in-package-of-symbol
                           (cat (symbol-name name) "-AUTOHYPS-FN")
                           name))
    (name-autohyps-body
         (intern-in-package-of-symbol (cat (symbol-name name)
                                           "-AUTOHYPS-BODY")
                                      name))
    (name-alist-autohyps
         (intern-in-package-of-symbol (cat (symbol-name name)
                                           "-ALIST-AUTOHYPS")
                                      name))
    (name-env-autohyps (intern-in-package-of-symbol
                            (cat (symbol-name name) "-ENV-AUTOHYPS")
                            name))
    (name-autoins (intern-in-package-of-symbol
                       (cat (symbol-name name) "-AUTOINS")
                       name))
    (name-autoins-fn (intern-in-package-of-symbol
                          (cat (symbol-name name) "-AUTOINS-FN")
                          name))
    (name-autoins-body (intern-in-package-of-symbol
                            (cat (symbol-name name) "-AUTOINS-BODY")
                            name))
    (name-alist-autoins
         (intern-in-package-of-symbol (cat (symbol-name name)
                                           "-ALIST-AUTOINS")
                                      name))
    (name-env-autoins (intern-in-package-of-symbol
                           (cat (symbol-name name) "-ENV-AUTOINS")
                           name))
    (name-env-autoins-in-terms-of-svex-env-extract
         (intern-in-package-of-symbol
              (cat (symbol-name name)
                   "-ENV-AUTOINS-IN-TERMS-OF-SVEX-ENV-EXTRACT")
              name))
    (name-autobinds (intern-in-package-of-symbol
                         (cat (symbol-name name) "-AUTOBINDS")
                         name))
    (invars (mergesort (alist-keys (svtv->inmasks svtv))))
    (inmap (svtv->inmap svtv))
    ((with-fast inmap))
    (non-override-test-invars
         (svtv-non-override-test-input-vars invars inmap))
    (non-override-test-invars-unsorted
         (svtv-non-override-test-input-vars
              (alist-keys (svtv->inmasks svtv))
              inmap))
    (invar-defaults
         (defsvtv-default-names non-override-test-invars))
    (cmds
     (cons
      (cons 'defconst
            (cons stvconst
                  (cons (cons 'quote (cons svtv 'nil))
                        'nil)))
      (append
       (and
        define-mod
        (cons
           (cons 'defconst
                 (cons modconst (cons design-const 'nil)))
           (cons (cons 'defund
                       (cons name-mod
                             (cons 'nil
                                   (cons '(declare (xargs :guard t))
                                         (cons modconst 'nil)))))
                 'nil)))
       (cons
        (cons
         'define
         (cons
          name
          (cons
           'nil
           (cons
            ':returns
            (cons
             '(svtv svtv-p)
             (cons
              ':parents
              (cons
               'nil
               (cons
                stvconst
                (cons
                 '///
                 (cons
                  (cons
                   'defthm
                   (cons
                    (intern-in-package-of-symbol
                         (cat "SVTV->OUTS-OF-" (symbol-name name))
                         name)
                    (cons
                     (cons
                      'equal
                      (cons
                          (cons 'svtv->outs
                                (cons (cons name 'nil) 'nil))
                          (cons (cons 'quote
                                      (cons (svtv->outs svtv) 'nil))
                                'nil)))
                     'nil)))
                  (cons
                   (cons
                    'defthm
                    (cons
                     (intern-in-package-of-symbol
                          (cat "SVTV->INS-OF-" (symbol-name name))
                          name)
                     (cons
                      (cons
                       'equal
                       (cons
                           (cons 'svtv->ins
                                 (cons (cons name 'nil) 'nil))
                           (cons (cons 'quote
                                       (cons (svtv->ins svtv) 'nil))
                                 'nil)))
                      'nil)))
                   (cons
                    (cons 'in-theory
                          (cons (cons 'disable
                                      (cons (cons name 'nil) 'nil))
                                'nil))
                    (cons
                     (cons
                      'add-to-ruleset!
                      (cons
                       'svtv-execs
                       (cons
                            (cons 'quote
                                  (cons (cons (cons name 'nil) 'nil)
                                        'nil))
                            'nil)))
                     'nil)))))))))))))
        (if define-macros
         (cons
          (cons 'define
                (cons name-autohyps
                      (cons (cons '&key invar-defaults)
                            (cons (svtv-autohyps svtv) 'nil))))
          (cons
           (cons
            'defmacro
            (cons
                 name-autohyps-body
                 (cons 'nil
                       (cons (cons 'quote
                                   (cons (svtv-autohyps svtv) 'nil))
                             'nil))))
           (cons
            (cons
             'define
             (cons
              name-alist-autohyps
              (cons
               '((x alistp))
               (cons
                ':guard-hints
                (cons
                 '(("Goal"
                    :in-theory
                    (e/d**
                        (consp-of-assoc-when-alistp
                             (eqlablep)
                             acl2::assoc-eql-exec-is-assoc-equal))))
                 (cons
                  '(declare (ignorable x))
                  (cons
                   (cons
                    'b*
                    (cons
                     (cons
                       (cons (cons 'assocs non-override-test-invars)
                             '(x))
                       'nil)
                     (cons (cons name-autohyps 'nil) 'nil)))
                   'nil)))))))
            (cons
             (cons 'add-to-ruleset!
                   (cons 'gl::shape-spec-obj-in-range-backchain
                         (cons name-autohyps-fn 'nil)))
             (cons
              (cons 'add-to-ruleset!
                    (cons 'gl::shape-spec-obj-in-range-open
                          (cons name-autohyps-fn 'nil)))
              (cons
               (cons
                'define
                (cons
                 name-env-autohyps
                 (cons
                  '((x svex-env-p))
                  (cons
                   '(declare (ignorable x))
                   (cons
                    (cons
                     'b*
                     (cons
                         (cons (cons (cons 'svassocs
                                           non-override-test-invars)
                                     '(x))
                               'nil)
                         (cons (cons name-autohyps 'nil) 'nil)))
                    'nil)))))
               (cons
                (cons 'add-to-ruleset!
                      (cons 'svtv-autohyps
                            (cons name-autohyps-fn 'nil)))
                (cons
                 (cons 'add-to-ruleset!
                       (cons 'svtv-alist-autohyps
                             (cons name-alist-autohyps 'nil)))
                 (cons
                  (cons 'add-to-ruleset!
                        (cons 'svtv-env-autohyps
                              (cons name-env-autohyps 'nil)))
                  (cons
                   (cons
                      'define
                      (cons name-autoins
                            (cons (cons '&key invar-defaults)
                                  (cons (svtv-autoins svtv) 'nil))))
                   (cons
                    (cons
                     'defthm
                     (cons
                      (intern-in-package-of-symbol
                           (cat (symbol-name name)
                                "-AUTOINS-LOOKUP")
                           name)
                      (cons
                       (cons
                        'implies
                        (cons
                         '(syntaxp (quotep k))
                         (cons
                          (cons
                           'equal
                           (cons
                            (cons
                             'assoc
                             (cons
                              'k
                              (cons (cons name-autoins 'nil) 'nil)))
                            (cons
                             (cons
                              'case
                              (cons 'k
                                    (autoins-lookup-cases
                                         non-override-test-invars)))
                             'nil)))
                          'nil)))
                       (cons
                        ':hints
                        (cons
                         (cons
                          (cons
                           '"goal"
                           (cons
                            ':in-theory
                            (cons
                             (cons
                              'e/d**
                              (cons
                               (cons
                                name-autoins-fn
                                '(assoc-of-acons
                                      assoc-of-nil car-cons cdr-cons
                                      member-equal (member-equal)))
                               'nil))
                             (if
                              (consp non-override-test-invars)
                              (cons
                               ':cases
                               (cons
                                   (autoins-lookup-casesplit
                                        non-override-test-invars 'k)
                                   'nil))
                              nil))))
                          'nil)
                         'nil)))))
                    (cons
                     (cons
                      'defthm
                      (cons
                       (intern-in-package-of-symbol
                        (cat
                            "SVEX-ENV-LOOKUP-OF-" (symbol-name name)
                            "-AUTOINS")
                        name)
                       (cons
                        (cons
                         'implies
                         (cons
                          '(syntaxp (quotep k))
                          (cons
                           (cons
                            'equal
                            (cons
                             (cons
                                'svex-env-lookup
                                (cons 'k
                                      (cons (cons name-autoins 'nil)
                                            'nil)))
                             (cons
                              (cons
                               'case
                               (cons
                                    '(svar-fix k)
                                    (autoins-svex-env-lookup-cases
                                         non-override-test-invars)))
                              'nil)))
                           'nil)))
                        (cons
                         ':hints
                         (cons
                          (cons
                           (cons
                            '"goal"
                            (cons
                             ':in-theory
                             (cons
                              (cons
                               'e/d**
                               (cons
                                (cons
                                  name-autoins-fn
                                  '(svex-env-lookup-of-cons
                                        svex-env-lookup-in-empty
                                        car-cons cdr-cons (svar-p)))
                                'nil))
                              (if
                               (consp non-override-test-invars)
                               (cons
                                 ':cases
                                 (cons (autoins-lookup-casesplit
                                            non-override-test-invars
                                            '(svar-fix k))
                                       'nil))
                               nil))))
                           'nil)
                          'nil)))))
                     (cons
                      (cons
                       'defthm
                       (cons
                        (intern-in-package-of-symbol
                         (cat
                            "SVEX-ENV-BOUNDP-OF-" (symbol-name name)
                            "-AUTOINS")
                         name)
                        (cons
                         (cons
                          'implies
                          (cons
                           '(syntaxp (quotep k))
                           (cons
                            (cons
                             'iff
                             (cons
                              (cons
                                'svex-env-boundp
                                (cons 'k
                                      (cons (cons name-autoins 'nil)
                                            'nil)))
                              (cons
                               (cons
                                'member-equal
                                (cons
                                 '(svar-fix k)
                                 (cons
                                  (cons
                                   'quote
                                   (cons
                                     non-override-test-invars 'nil))
                                  'nil)))
                               'nil)))
                            'nil)))
                         (cons
                          ':hints
                          (cons
                           (cons
                            (cons
                             '"goal"
                             (cons
                              ':in-theory
                              (cons
                               (cons
                                'e/d**
                                (cons
                                 (cons
                                  name-autoins-fn
                                  '(svex-env-boundp-of-cons
                                       svex-env-boundp-of-nil
                                       car-cons cdr-cons (svar-p)
                                       member-equal (member-equal)))
                                 'nil))
                               (if
                                (consp non-override-test-invars)
                                (cons
                                 ':cases
                                 (cons (autoins-lookup-casesplit
                                            non-override-test-invars
                                            '(svar-fix k))
                                       'nil))
                                nil))))
                            'nil)
                           'nil)))))
                      (cons
                       (cons
                        'defmacro
                        (cons
                         name-autoins-body
                         (cons
                          'nil
                          (cons
                              (cons 'quote
                                    (cons (svtv-autoins svtv) 'nil))
                              'nil))))
                       (cons
                        (cons
                         'define
                         (cons
                          name-alist-autoins
                          (cons
                           '((x alistp))
                           (cons
                            ':guard-hints
                            (cons
                             '(("Goal"
                                :in-theory
                                (e/d**
                                 (consp-of-assoc-when-alistp
                                  (eqlablep)
                                  acl2::assoc-eql-exec-is-assoc-equal))))
                             (cons
                              '(declare (ignorable x))
                              (cons
                               (cons
                                'b*
                                (cons
                                 (cons
                                  (cons
                                     (cons 'assocs
                                           non-override-test-invars)
                                     '(x))
                                  'nil)
                                 (cons (cons name-autoins 'nil)
                                       'nil)))
                               'nil)))))))
                        (cons
                         (cons
                          'define
                          (cons
                           name-env-autoins
                           (cons
                            '((x svex-env-p))
                            (cons
                             '(declare (ignorable x))
                             (cons
                              ':returns
                              (cons
                               (cons
                                'env
                                (cons
                                 'svex-env-p
                                 (cons
                                  ':hints
                                  (cons
                                   (cons
                                    (cons
                                     '"Goal"
                                     (cons
                                      ':in-theory
                                      (cons
                                       (cons
                                           'enable
                                           (cons name-autoins 'nil))
                                       'nil)))
                                    'nil)
                                   'nil))))
                               (cons
                                (cons
                                 'b*
                                 (cons
                                  (cons
                                   (cons
                                     (cons 'svassocs
                                           non-override-test-invars)
                                     '(x))
                                   'nil)
                                  (cons (cons name-autoins 'nil)
                                        'nil)))
                                (cons
                                 '///
                                 (cons
                                  (cons
                                   'defret
                                   (cons
                                    name-env-autoins-in-terms-of-svex-env-extract
                                    (cons
                                     (cons
                                      'equal
                                      (cons
                                       'env
                                       (cons
                                        (cons
                                         'svex-env-extract
                                         (cons
                                          (cons
                                           'quote
                                           (cons
                                            (rev
                                             non-override-test-invars-unsorted)
                                            'nil))
                                          '(x)))
                                        'nil)))
                                     (cons
                                      ':hints
                                      (cons
                                       (cons
                                        (cons
                                         '"Goal"
                                         (cons
                                          ':in-theory
                                          (cons
                                           (cons
                                            'enable
                                            (cons
                                             'svex-env-extract
                                             (cons
                                                name-autoins 'nil)))
                                           'nil)))
                                        'nil)
                                       'nil)))))
                                  'nil)))))))))
                         (cons
                          (cons 'add-to-ruleset!
                                (cons 'svtv-autoins
                                      (cons name-autoins-fn 'nil)))
                          (cons
                           (cons
                              'add-to-ruleset!
                              (cons 'svtv-alist-autoins
                                    (cons name-alist-autoins 'nil)))
                           (cons
                            (cons
                             'add-to-ruleset!
                             (cons
                              'svtv-env-autoins
                              (cons
                               name-env-autoins-in-terms-of-svex-env-extract
                               'nil)))
                            (cons
                             (cons
                              'add-to-ruleset!
                              (cons
                               'svtv-env-autoins-in-terms-of-svex-env-extract
                               (cons
                                name-env-autoins-in-terms-of-svex-env-extract
                                'nil)))
                             (cons
                              (cons
                               'defthm
                               (cons
                                (intern-in-package-of-symbol
                                   (cat (symbol-name name)
                                        "-ALIST-AUTOINS-IDEMPOTENT")
                                   name)
                                (cons
                                 (cons
                                  'equal
                                  (cons
                                   (cons
                                    name-alist-autoins
                                    (cons
                                      (cons name-alist-autoins '(x))
                                      'nil))
                                   (cons
                                      (cons name-alist-autoins '(x))
                                      'nil)))
                                 (cons
                                  ':hints
                                  (cons
                                   (cons
                                    (cons
                                     '"Goal"
                                     (cons
                                      ':in-theory
                                      (cons
                                       (cons
                                        'e/d**
                                        (cons
                                         (cons
                                          name-alist-autoins
                                          (cons
                                           name-autoins-fn
                                           '(assoc-of-acons
                                                 car-cons
                                                 cdr-cons (assoc))))
                                         'nil))
                                       'nil)))
                                    'nil)
                                   'nil)))))
                              (cons
                               (cons
                                'defthm
                                (cons
                                 (intern-in-package-of-symbol
                                      (cat (symbol-name name)
                                           "-ALIST-AUTOINS-LOOKUP")
                                      name)
                                 (cons
                                  (cons
                                   'equal
                                   (cons
                                    (cons
                                     'assoc
                                     (cons
                                      'k
                                      (cons
                                       (cons
                                            name-alist-autoins '(x))
                                       'nil)))
                                    (cons
                                     (cons
                                      'and
                                      (cons
                                       (cons
                                        'member
                                        (cons
                                         'k
                                         (cons
                                          (cons
                                               'svtv->ins
                                               (cons stvconst 'nil))
                                          'nil)))
                                       (cons
                                        (cons
                                         'not
                                         (cons
                                          (cons
                                           'equal
                                           (cons
                                            (cons
                                             'cdr
                                             (cons
                                              (cons
                                               'assoc
                                               (cons
                                                'k
                                                (cons
                                                 (cons
                                                  'svtv->inmap
                                                  (cons
                                                     stvconst 'nil))
                                                 'nil)))
                                              'nil))
                                            '(:override-test)))
                                          'nil))
                                        '((cons
                                            k (cdr (assoc k x)))))))
                                     'nil)))
                                  (cons
                                   ':hints
                                   (cons
                                    (cons
                                     (cons
                                      '"goal"
                                      (cons
                                       ':in-theory
                                       (cons
                                        (cons
                                         'e/d**
                                         (cons
                                          (cons
                                           name-alist-autoins
                                           (cons
                                            name-autoins-fn
                                            '(assoc-of-acons
                                               assoc-of-nil car-cons
                                               cdr-cons member-equal
                                               (svtv->ins)
                                               (svtv->inmap))))
                                          'nil))
                                        'nil)))
                                     'nil)
                                    'nil)))))
                               (cons
                                (cons
                                 'defthm
                                 (cons
                                  (intern-in-package-of-symbol
                                   (cat
                                       (symbol-name name)
                                       "-ALIST-AUTOHYPS-OF-AUTOINS")
                                   name)
                                  (cons
                                   (cons
                                    'equal
                                    (cons
                                     (cons
                                      name-alist-autohyps
                                      (cons
                                       (cons
                                            name-alist-autoins '(x))
                                       'nil))
                                     (cons
                                      (cons
                                           name-alist-autohyps '(x))
                                      'nil)))
                                   (cons
                                    ':hints
                                    (cons
                                     (cons
                                      (cons
                                       '"Goal"
                                       (cons
                                        ':in-theory
                                        (cons
                                         (cons
                                          'e/d**
                                          (cons
                                           (cons
                                            name-alist-autohyps
                                            (cons
                                             name-alist-autoins
                                             (cons
                                              name-autoins-fn
                                              '(assoc-of-acons
                                                car-cons
                                                cdr-cons (assoc)))))
                                           'nil))
                                         'nil)))
                                      'nil)
                                     'nil)))))
                                (cons
                                 (cons
                                  'defthm
                                  (cons
                                   (intern-in-package-of-symbol
                                    (cat (symbol-name name)
                                         "-ENV-AUTOHYPS-OF-AUTOINS")
                                    name)
                                   (cons
                                    (cons
                                     'equal
                                     (cons
                                      (cons
                                       name-env-autohyps
                                       (cons
                                        (cons name-env-autoins '(x))
                                        'nil))
                                      (cons
                                       (cons name-env-autohyps '(x))
                                       'nil)))
                                    (cons
                                     ':hints
                                     (cons
                                      (cons
                                       (cons
                                        '"Goal"
                                        (cons
                                         ':in-theory
                                         (cons
                                          (cons
                                           'e/d**
                                           (cons
                                            (cons
                                             name-env-autohyps
                                             (cons
                                              name-env-autoins
                                              (cons
                                               name-autoins-fn
                                               '(svex-env-lookup-of-cons
                                                 svex-env-lookup-in-empty
                                                 car-cons
                                                 cdr-cons (4vec-fix)
                                                 (svar-p)
                                                 4vec-fix-of-4vec
                                                 4vec-p-of-svex-env-lookup
                                                 (svar-fix)))))
                                            'nil))
                                          'nil)))
                                       'nil)
                                      'nil)))))
                                 (cons
                                  (cons
                                   'defmacro
                                   (cons
                                    name-autobinds
                                    (cons
                                     'nil
                                     (cons
                                      (cons
                                         'quote
                                         (cons (svtv-autobinds svtv)
                                               'nil))
                                      'nil))))
                                  'nil)))))))))))))))))))))))))
         nil)))))
    (cmds
     (if (not want-xdoc-p)
         cmds
      (cons
       (cons
        'defxdoc
        (cons
         name
         (cons
              ':parents
              (cons parents
                    (cons ':short
                          (cons short
                                (cons ':long (cons long 'nil))))))))
       cmds))))
   (cons 'with-output
         (cons ':off
               (cons '(event)
                     (cons (cons 'progn cmds) 'nil)))))))