		Search-engine friendly clone of the ACL2 documentation.

Svl-run

Evaluate SVL designs

Signature
(svl-run modname inputs-env ins-bind-alist out-bind-alist modules) → res
Arguments: modname — Guard (sv::modname-p modname).; inputs-env — Guard (svex-env-p inputs-env).; ins-bind-alist — Guard (alistp ins-bind-alist).; out-bind-alist — Guard (alistp out-bind-alist).; modules — Guard (svl-module-alist-p modules).
Returns: res — Type (alistp res).

SVL-RUN has similar inputs to (@see acl2::def-svtv). However, some of those inputs (i.e., simulation patterns) are supplied to svl-run at runtime (or during the proofs).

modname: Name of the module to run.
inputs-env: An alist that binds input wires to concrete values (during execution) or variables (during proofs).
ins-bind-alist: the simulation pattern for inputs. It should be an alist, an example is given below.
out-bind-alist: same as ins-bind-alist but for outputs instead.

For example:


(defconst *counter-input-binds-alist*
   `(("Clock" 0 ~)
     ("Reset" 1 1 1 1 1)
     ("Enable" 0 0 0 0 0 0 0 0 0 0)
     ("Load" 0 1)
     ("Mode" 0)
     ("Data[8:0]" data8-10)
     ("Data[63:9]" data-rest)))


   (defconst *counter-outputs*
     `(("Count[31:0]" count_low1 _ _ _ _ _ _ _ _ _ count_low8 _ count_low10)
       ("Count[63:32]" count_high1 _ _ _ count_high2)))


(svl-run "COUNTER"
         (make-fast-alist '((count_low1 . -5)
                            (count_low8 . 5)
                            (count_low10 . 10)))
         *counter-input-binds-alist*
         *counter-outputs*
         *counter-svl-design*)))

Definitions and Theorems

Function: svl-run

(defun
 svl-run
 (modname inputs-env
          ins-bind-alist out-bind-alist modules)
 (declare (xargs :guard (and (sv::modname-p modname)
                             (svex-env-p inputs-env)
                             (alistp ins-bind-alist)
                             (alistp out-bind-alist)
                             (svl-module-alist-p modules))))
 (declare (ignorable out-bind-alist))
 (declare
    (xargs :guard (and (string-listp (strip-cars out-bind-alist))
                       (string-listp (strip-cars ins-bind-alist)))))
 (let
   ((acl2::__function__ 'svl-run))
   (declare (ignorable acl2::__function__))
   (b* ((module (assoc-equal modname modules))
        ((unless module)
         (hard-error 'svl-run
                     "Module ~p0 cannot be found! ~%"
                     (list (cons #\0 modname))))
        (module (cdr module))
        (input-wires (svl-module->inputs module))
        (output-wires (strip-cars (svl-module->outputs module)))
        (inputs-unbound
             (svl-generate-inputs ins-bind-alist input-wires))
        ((unless (svex-list-listp inputs-unbound))
         (hard-error
              'svl-run
              "Something went wrong while parsing inputs... ~p0 ~%"
              (list (cons #\0 inputs-unbound))))
        (inputs (svexlist-list-eval-wog inputs-unbound inputs-env)))
       (svl-run-aux modname inputs output-wires
                    out-bind-alist (make-svl-env)
                    modules))))

Theorem: alistp-of-svl-run

(defthm acl2::alistp-of-svl-run
        (b* ((res (svl-run modname inputs-env
                           ins-bind-alist out-bind-alist modules)))
            (alistp res))
        :rule-classes :rewrite)

Subtopics

Svl-run-phase: Run a single phase of svl-run
Svl-run-phase-wog: Same as svl-run-phase but without guards