• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
      • Svex-stvs
      • Svex-decomposition-methodology
      • Sv-versus-esim
      • Svex-decomp
      • Svex-compose-dfs
      • Svex-compilation
      • Moddb
      • Svmods
        • Address
        • Wire
        • Module
          • Module-fix
          • Make-module
          • Module-vars
          • Module-p
          • Module-equiv
          • Change-module
          • Module->constraints
          • Module->aliaspairs
          • Module->wires
          • Module->insts
          • Module->fixups
          • Module->assigns
          • Module-addr-p
        • Lhs
        • Path
        • Svar-add-namespace
        • Design
        • Modinst
        • Lhs-add-namespace
        • Modalist
        • Path-add-namespace
        • Modname->submodnames
        • Name
        • Constraintlist-addr-p
        • Svex-alist-addr-p
        • Svar-map-addr-p
        • Lhspairs-addr-p
        • Modname
        • Assigns-addr-p
        • Lhs-addr-p
        • Lhatom-addr-p
        • Modhier-list-measure
        • Attributes
        • Modhier-measure
        • Modhier-list-measure-aux
        • Modhier-loopfreelist-p
        • Modhier-loopfree-p
      • Svstmt
      • Sv-tutorial
      • Expressions
      • Symbolic-test-vector
      • Vl-to-svex
    • Fgl
    • Vwsim
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Module

Make-module

Basic constructor macro for module structures.

Syntax

(make-module [:wires <wires>] 
             [:insts <insts>] 
             [:assigns <assigns>] 
             [:fixups <fixups>] 
             [:constraints <constraints>] 
             [:aliaspairs <aliaspairs>]) 

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

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

Definition

This is an ordinary make- macro introduced by defprod.

Macro: make-module

(defmacro make-module (&rest args)
  (std::make-aggregate 'module
                       args
                       '((:wires)
                         (:insts)
                         (:assigns)
                         (:fixups)
                         (:constraints)
                         (:aliaspairs))
                       'make-module
                       nil))

Function: module

(defun module (wires insts
                     assigns fixups constraints aliaspairs)
  (declare (xargs :guard (and (wirelist-p wires)
                              (modinstlist-p insts)
                              (assigns-p assigns)
                              (assigns-p fixups)
                              (constraintlist-p constraints)
                              (lhspairs-p aliaspairs))))
  (declare (xargs :guard t))
  (let ((__function__ 'module))
    (declare (ignorable __function__))
    (b* ((wires (mbe :logic (wirelist-fix wires)
                     :exec wires))
         (insts (mbe :logic (modinstlist-fix insts)
                     :exec insts))
         (assigns (mbe :logic (assigns-fix assigns)
                       :exec assigns))
         (fixups (mbe :logic (assigns-fix fixups)
                      :exec fixups))
         (constraints (mbe :logic (constraintlist-fix constraints)
                           :exec constraints))
         (aliaspairs (mbe :logic (lhspairs-fix aliaspairs)
                          :exec aliaspairs)))
      (list (cons 'wires wires)
            (cons 'insts insts)
            (cons 'assigns assigns)
            (cons 'fixups fixups)
            (cons 'constraints constraints)
            (cons 'aliaspairs aliaspairs)))))