• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
        • Defstv
          • Defstv-fn
          • Defstv-main
          • Stv-autohyps
          • Stv-autobinds
          • Stv-autoins
        • Stv-compile
        • Symbolic-test-vector-format
        • Stv-implementation-details
        • Compiled-stv-p
        • Stv-run-for-all-dontcares
        • Stv-run
        • Stv-process
        • Stv-run-check-dontcares
        • Symbolic-test-vector-composition
        • Stv-expand
        • Stv-easy-bindings
        • Stv-debug
        • Stv-run-squash-dontcares
        • Stvdata-p
        • Stv-doc
        • Stv2c
        • Stv-widen
        • Stv-out->width
        • Stv-in->width
        • Stv-number-of-phases
        • Stv->outs
        • Stv->ins
        • Stv-suffix-signals
        • Stv->vars
      • Esim-primitives
      • E-conversion
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Defstv

Defstv-fn

Implementation of defstv.

Signature

(defstv-fn name mod-const-name 
           mod inputs outputs internals 
           overrides labels parents short long) 
 
  → 
*

Arguments

name — E.g., mmx-run.
    Guard (symbolp name).

mod-const-name — E.g., the symbol *mmx*.
    Guard (symbolp mod-const-name).

mod — E.g., the actual E module for *mmx*.
    Guard (good-esim-modulep mod).

Definitions and Theorems

Function: defstv-fn

(defun defstv-fn (name mod-const-name
                       mod inputs outputs internals
                       overrides labels parents short long)
 (declare (xargs :guard (and (symbolp name)
                             (symbolp mod-const-name)
                             (good-esim-modulep mod))))
 (let ((__function__ 'defstv-fn))
  (declare (ignorable __function__))
  (b*
   ((labels (if (symbol-listp labels)
                labels
              (raise ":labels need to be a symbol-listp.")))
    (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.")
                           ""))))
    (processed-stv (defstv-main :mod mod
                                :name name
                                :overrides overrides
                                :inputs inputs
                                :outputs outputs
                                :internals internals))
    ((unless processed-stv)
     (raise "Failed to process STV."))
    (compiled-stv (processed-stv->compiled-stv processed-stv))
    (stv (processed-stv->user-stv processed-stv))
    ((unless (stvdata-p stv))
     (raise "stv processing didn't produce good stvdata?"))
    (long
     (if (not want-xdoc-p)
         long
      (str::cat
       "<h3>Simulation Diagram</h3>

<p>This is a <see topic='@(url
acl2::symbolic-test-vectors)'>symbolic test vector</see> defined with @(see
acl2::defstv).</p>"
       (or (stv-to-xml stv compiled-stv labels)
           "Error generating diagram")
       long)))
    (stvconst (intern-in-package-of-symbol
                   (str::cat "*" (symbol-name name) "*")
                   name))
    (modconst
       (intern-in-package-of-symbol (str::cat "*" (symbol-name name)
                                              "-MOD*")
                                    name))
    (name-mod (intern-in-package-of-symbol
                   (str::cat (symbol-name name) "-MOD")
                   name))
    (name-autohyps
         (intern-in-package-of-symbol (str::cat (symbol-name name)
                                                "-AUTOHYPS")
                                      name))
    (name-autoins (intern-in-package-of-symbol
                       (str::cat (symbol-name name) "-AUTOINS")
                       name))
    (name-autobinds
         (intern-in-package-of-symbol (str::cat (symbol-name name)
                                                "-AUTOBINDS")
                                      name))
    (cmds
     (cons
      (cons 'defconst
            (cons stvconst
                  (cons (cons 'quote (cons processed-stv 'nil))
                        'nil)))
      (cons
       (cons
        'defconst
        (cons
         modconst
         (cons
          (cons 'stv-cut-module
                (cons (cons 'compiled-stv->override-paths
                            (cons (cons 'processed-stv->compiled-stv
                                        (cons stvconst 'nil))
                                  'nil))
                      (cons mod-const-name 'nil)))
          'nil)))
       (cons
        (cons 'defund
              (cons name
                    (cons 'nil
                          (cons '(declare (xargs :guard t))
                                (cons stvconst 'nil)))))
        (cons
         (cons 'defthm
               (cons (intern-in-package-of-symbol
                          (str::cat "PROCESSED-STV-P-OF-"
                                    (symbol-name name))
                          name)
                     (cons (cons 'processed-stv-p
                                 (cons (cons name 'nil) 'nil))
                           'nil)))
         (cons
          (cons 'in-theory
                (cons (cons 'disable
                            (cons (cons ':executable-counterpart
                                        (cons name 'nil))
                                  'nil))
                      'nil))
          (cons
           (cons 'defund
                 (cons name-mod
                       (cons 'nil
                             (cons '(declare (xargs :guard t))
                                   (cons modconst 'nil)))))
           (cons
            (cons
             'defmacro
             (cons
                name-autohyps
                (cons 'nil
                      (cons (cons 'quote
                                  (cons (stv-autohyps processed-stv)
                                        'nil))
                            'nil))))
            (cons
             (cons
              'defmacro
              (cons
               name-autoins
               (cons
                'nil
                (cons (cons 'quote
                            (cons (stv-autoins processed-stv) 'nil))
                      'nil))))
             (cons
              (cons
               'defmacro
               (cons
                name-autobinds
                (cons
                     'nil
                     (cons (cons 'quote
                                 (cons (stv-autobinds processed-stv)
                                       '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)))))))