		Search-engine friendly clone of the ACL2 documentation.

Svl-module

Make-svl-module

Basic constructor macro for svl-module structures.

Syntax

(make-svl-module [:rank <rank>] 
                 [:inputs <inputs>] 
                 [:delayed-inputs <delayed-inputs>] 
                 [:outputs <outputs>] 
                 [:occs <occs>])

This is the usual way to construct svl-module structures. It simply conses together a structure with the specified fields.

This macro generates a new svl-module structure from scratch. See also change-svl-module, which can "change" an existing structure, instead.

Definition

This is an ordinary make- macro introduced by fty::defprod.

Macro: make-svl-module

(defmacro make-svl-module (&rest args)
  (std::make-aggregate 'svl-module
                       args
                       '((:rank quote 0)
                         (:inputs)
                         (:delayed-inputs)
                         (:outputs)
                         (:occs))
                       'make-svl-module
                       nil))

Function: svl-module

(defun svl-module (rank inputs delayed-inputs outputs occs)
 (declare (xargs :guard (and (natp rank)
                             (wire-list-p inputs)
                             (sv::svarlist-p delayed-inputs)
                             (wire-list-p outputs)
                             (svl-occ-alist-p occs))))
 (declare (xargs :guard t))
 (let ((acl2::__function__ 'svl-module))
  (declare (ignorable acl2::__function__))
  (b* ((rank (mbe :logic (nfix rank) :exec rank))
       (inputs (mbe :logic (wire-list-fix inputs)
                    :exec inputs))
       (delayed-inputs (mbe :logic (sv::svarlist-fix delayed-inputs)
                            :exec delayed-inputs))
       (outputs (mbe :logic (wire-list-fix outputs)
                     :exec outputs))
       (occs (mbe :logic (svl-occ-alist-fix occs)
                  :exec occs)))
    (list (cons 'rank rank)
          (cons 'inputs inputs)
          (cons 'delayed-inputs delayed-inputs)
          (cons 'outputs outputs)
          (cons 'occs occs)))))