Merge remote-tracking branch 'remotes/origin/master'

books/centaur/vl/loader/parser/top.lisp

@@ -38,6 +38,7 @@
 (include-book "classes")
 (include-book "configs")
 (include-book "imports")
+(include-book "std/strings/fast-cat" :dir :system)
 (local (include-book "../../util/arithmetic"))
 
 (local (in-theory (disable (tau-system))))

books/centaur/vl/simpconfig.lisp

@@ -38,87 +38,91 @@
   :short "Options for how to simplify Verilog modules."
   :tag :vl-simpconfig
 
-  ((compress-p   booleanp
-                 "Hons the modules at various points.  This takes some time,
-                  but can produce smaller translation files."
-                 :rule-classes :type-prescription)
-
-   (problem-mods string-listp
-                 "Names of modules that should thrown out, perhaps because they
-                  cause some kind of problems."
-                 :default nil)
-
-   (already-annotated booleanp
-                      "Denotes that we've already annotated the design and shouldn't
-                       do it again.")
-
-   (unroll-limit natp
-                 "Maximum number of iterations to unroll for loops, etc., when
-                  rewriting statements.  This is just a safety valve."
-                 :rule-classes :type-prescription
-                 :default 1000)
-
-   (uniquecase-conservative natp :default 0
-                            "For @('unique case') and @('unique0 case') statements,
-                             a synthesis tool is allowed to assume that the cases
-                             are mutually exclusive and simplify the logic accordingly.
-                             For @('unique') they can assume that exactly one of
-                             the tests will be true.  This configuration flag is
-                             a natural number that sets the degree of conservativity,
-                             as follows: When 0 (the default), the logic we generate
-                             emulates a simulator, which always executes the first
-                             matching case.  When 1, if uniqueness is violated,
-                             then we pretend that all tests that were 1 instead
-                             evaluated to X, or if all tests were 0 then we pretend
-                             all instead evaluated to X.  When 2 or greater, when
-                             the condition is violated we pretend all tests evaluated
-                             to X.  When 3 or greater, we additionally pretend that
-                             all assignments within the case statement write X
-                             instead of the given value.  The intention behind
-                             this is to make it likely that our logic is conservative
-                             with respect to anything a synthesis tool might
-                             produce.")
-
-   (uniquecase-constraints booleanp
-                           "Generate constraints for @('unique case') and @('unique0
-                            case') statements.  Likely you do not want both this
-                            and @('uniquecase-conservative') to be set, because
-                            they are two different approaches for dealing with
-                            a synthesis tool's flexibility in dealing with unique
-                            and unique0 case statements.  When this is set, we
-                            separately store a constraint saying that the cases
-                            are one-hot or one/zero-hot, respectively.  This constraint
-                            is stored in the SV modules when they are generated
-                            by @(see vl-design->svex-design).")
-
-   (enum-constraints "Generate constraints for variables of @('enum') datatypes,
-                      or compound datatypes that have @('enum') subfields. These
-                      constraints are saved in the SV modules when they are generated
-                      by @(see vl-design->svex-design).  Each constraint says that
-                      an enum field's value is one of the proper values of an enum
-                      type.  If NIL (the default), these constraints are not generated.
-                      If T or any nonnil object other than the keyword :ALL, then
-                      the constraints are generated except for port variables.
-                       If :ALL, then these are generated for ports as well.")
-
-   (enum-fixups "Generate fixups for variables of @('enum') datatypes, or compound
-                 datatypes that have @('enum') subfields. These cause svex compilation
-                 to fix up enum values to be X if not one of the allowed values.
-                 If NIL (the default), this fixing will not be done.  Similar to
-                 the @('enum-constraints') option, fixups are only done for non-port
-                 variables unless this option is set to the keyword :ALL.")
-
-   (sv-simplify booleanp :default t
-                "Apply svex rewriting to the results of compiling procedural blocks.")
-
-   (sv-simplify-verbosep booleanp
-                         "Verbosely report svex rewriting statistics.")
-
-   (nb-latch-delay-hack booleanp
-                        "Artificially add a delay to nonblocking assignments in latch-like contexts.")
-
-   (name-without-default-params booleanp
-                                "Omit non-overridden parameters from module names generated by unparameterization.")))
+  ((compress-p
+    booleanp
+    "Hons the modules at various points.  This takes some time, but can produce
+     smaller translation files."
+    :rule-classes :type-prescription)
+
+   (problem-mods
+    string-listp
+    "Names of modules that should thrown out, perhaps because they cause some kind
+     of problems."
+    :default nil)
+
+   (already-annotated
+    booleanp
+    "Denotes that we've already annotated the design and shouldn't do it
+     again.")
+
+   (unroll-limit
+    natp
+    "Maximum number of iterations to unroll for loops, etc., when rewriting statements.
+      This is just a safety valve."
+    :rule-classes :type-prescription
+    :default 1000)
+
+   (uniquecase-conservative
+    natp :default 0
+    "For @('unique case') and @('unique0 case') statements, a synthesis tool is
+     allowed to assume that the cases are mutually exclusive and simplify the logic
+     accordingly. For @('unique') they can assume that exactly one of the tests
+     will be true.  This configuration flag is a natural number that sets the degree
+     of conservativity, as follows: When 0 (the default), the logic we generate
+     emulates a simulator, which always executes the first matching case.  When
+     1, if uniqueness is violated, then we pretend that all tests that were 1 instead
+     evaluated to X, or if all tests were 0 then we pretend all instead evaluated
+     to X.  When 2 or greater, when the condition is violated we pretend all tests
+     evaluated to X.  When 3 or greater, we additionally pretend that all assignments
+     within the case statement write X instead of the given value.  The intention
+     behind this is to make it likely that our logic is conservative with respect
+     to anything a synthesis tool might produce.")
+
+   (uniquecase-constraints
+    booleanp
+    "Generate constraints for @('unique case') and @('unique0 case') statements.
+      Likely you do not want both this and @('uniquecase-conservative') to be set,
+     because they are two different approaches for dealing with a synthesis tool's
+     flexibility in dealing with unique and unique0 case statements.  When this
+     is set, we separately store a constraint saying that the cases are one-hot
+     or one/zero-hot, respectively.  This constraint is stored in the SV modules
+     when they are generated by @(see vl-design->svex-design).")
+
+   (enum-constraints
+    "Generate constraints for variables of @('enum') datatypes, or compound datatypes
+     that have @('enum') subfields. These constraints are saved in the SV modules
+     when they are generated by @(see vl-design->svex-design).  Each constraint
+     says that an enum field's value is one of the proper values of an enum type.
+      If NIL (the default), these constraints are not generated. If T or any nonnil
+     object other than the keyword :ALL, then the constraints are generated except
+     for port variables. If :ALL, then these are generated for ports as well.")
+
+   (enum-fixups
+    "Generate fixups for variables of @('enum') datatypes, or compound datatypes
+     that have @('enum') subfields. These cause svex compilation to fix up enum
+     values to be X if not one of the allowed values. If NIL (the default), this
+     fixing will not be done.  Similar to the @('enum-constraints') option, fixups
+     are only done for non-port variables unless this option is set to the keyword
+     :ALL.")
+
+   (sv-simplify
+    booleanp :default t
+    "Apply svex rewriting to the results of compiling procedural blocks.")
+
+   (sv-simplify-verbosep
+    booleanp
+    "Verbosely report svex rewriting statistics.")
+
+   (nb-latch-delay-hack
+    booleanp
+    "Artificially add a delay to nonblocking assignments in latch-like contexts.")
+
+   (name-without-default-params 
+    booleanp
+    "Omit non-overridden parameters from module names generated by unparameterization.")
+   (unparam-bad-instance-fatalp
+    booleanp :default t
+    "Make a fatal warning when a nonexistent parameter is overridden by a module instance.")))
 
 (defconst *vl-default-simpconfig*
   (make-vl-simpconfig))

books/centaur/vl/transforms/unparam/lineup.lisp

@@ -153,6 +153,7 @@
   :short "Line up parameter arguments with parameter declarations."
   ((formals  vl-paramdecllist-p "In proper order, from the submodule.")
    (actuals  vl-paramargs-p     "From the instance.")
+   (bad-instance-fatalp booleanp)
    (warnings vl-warninglist-p   "Warnings accumulator for the superior module."))
   :returns
   (mv (successp  booleanp :rule-classes :type-prescription)
@@ -172,7 +173,7 @@
 
       (:vl-paramargs-named
        (b* ((actual-names (vl-namedparamvaluelist->names actuals.args))
-            (formal-names (vl-paramdecllist->names (vl-nonlocal-paramdecls formals)))
+            (?formal-names (vl-paramdecllist->names (vl-nonlocal-paramdecls formals)))
 
             ((unless (uniquep actual-names))
              (mv nil
@@ -184,15 +185,15 @@
             (illegal-names
              ;; Actuals that are NOT actually declarations.
              (difference (mergesort actual-names) (mergesort formal-names)))
-            ((when illegal-names)
-             (mv nil
-                 (fatal :type :vl-bad-instance
-                        :msg "parameter~s1 ~&2 ~s2."
-                        :args (list nil
-                                    (if (vl-plural-p illegal-names) "s" "")
-                                    illegal-names
-                                    (if (vl-plural-p illegal-names) "do not exist" "does not exist")))
-                 nil))
+            (warnings (if illegal-names
+                          (warn :type :vl-bad-instance
+                                :msg "parameter~s1 ~&2 ~s2."
+                                :args (list nil
+                                            (if (vl-plural-p illegal-names) "s" "")
+                                            illegal-names
+                                            (if (vl-plural-p illegal-names) "do not exist" "does not exist"))
+                                :fatalp bad-instance-fatalp)
+                        warnings))
 
             ;; No confusion: everything is unique, the instance mentions only
             ;; the non-localparams, etc.  Good enough.

books/centaur/vl/transforms/unparam/top.lisp

@@ -269,7 +269,9 @@ with, we can safely remove @('plus') from our module list.</p>")
                (elabindex "with the overridden parameter values")
                (final-paramdecls vl-paramdecllist-p))
   (b* (((mv ok warnings overrides)
-        (vl-make-paramdecloverrides formals actuals warnings))
+        (vl-make-paramdecloverrides formals actuals
+                                    (vl-simpconfig->unparam-bad-instance-fatalp config)
+                                    warnings))
        ((unless ok)
         (mv nil warnings elabindex nil))
        (mod-ss (vl-elabindex->ss))
@@ -906,7 +908,6 @@ for each usertype is stored in the res field.</p>"
        (elabindex (vl-elabindex-sync-scopes))
        (scopes (vl-elabindex->scopes))
        ((mv mod mod-ss) (vl-scopestack-find-definition/ss inst.modname ss))
-
        ((unless (and mod
                      (or (eq (tag mod) :vl-module)
                          (eq (tag mod) :vl-interface))))

books/centaur/vl/util/defs.lisp

@@ -45,7 +45,7 @@
 (include-book "centaur/misc/alist-equiv" :dir :system)
 (include-book "centaur/misc/hons-extra" :dir :system)
 (include-book "std/strings/top" :dir :system)
-(include-book "std/strings/fast-cat" :dir :system)
+(include-book "std/strings/cat" :dir :system)
 (include-book "misc/assert" :dir :system)
 (include-book "misc/definline" :dir :system) ;; bozo
 (include-book "std/system/non-parallel-book" :dir :system)

books/centaur/vl2014/loader/top.lisp

@@ -43,6 +43,7 @@
 (include-book "../mlib/scopestack")
 (include-book "../util/cwtime")
 (include-book "../util/gc")
+(include-book "std/strings/fast-cat" :dir :system)
 (include-book "centaur/misc/hons-extra" :dir :system)
 (include-book "defsort/duplicated-members" :dir :system)
 (local (include-book "../util/arithmetic"))

books/centaur/vl2014/util/defs.lisp

@@ -45,7 +45,7 @@
 (include-book "centaur/misc/alist-equiv" :dir :system)
 (include-book "centaur/misc/hons-extra" :dir :system)
 (include-book "std/strings/top" :dir :system)
-(include-book "std/strings/fast-cat" :dir :system)
+(include-book "std/strings/cat" :dir :system)
 (include-book "misc/assert" :dir :system)
 (include-book "misc/definline" :dir :system) ;; bozo
 (include-book "std/system/non-parallel-book" :dir :system)

books/doc/relnotes.lisp

@@ -247,6 +247,12 @@
  by recoding several functions that previously used Lisp bignums to use a
  @(see bitops::sparseint) based encoding.</p>
 
+ <h4><see topic='@(url acl2::xdoc)'>Xdoc</see></h4>
+
+ <p>Added a utility, @(see xdoc::archive-xdoc), that saves the documentation
+ generated by a series of local events, partially preprocessing it to avoid
+ references to definitions that might only be locally available.</p>
+
  <h3>Licensing Changes</h3>
 
  <h3>Build System Updates</h3>

books/doc/top.lisp

@@ -64,6 +64,7 @@
 (include-book "practices")
 
 (include-book "xdoc/save" :dir :system)
+(include-book "xdoc/archive" :dir :system)
 
 (include-book "build/doc" :dir :system)
 

books/std/util/define.lisp

@@ -1751,16 +1751,36 @@ with a single return value.</p>
 formal if there is a return value that has the same name.  To work around this,
 the @(':pre-bind') argument accepts a list of @(see b*) bindings that occur
 before the binding of the return values.  You may also just want to not share
-names between your formals and returns.</p>")
-
-(defun dumb-strsubst (old new from str)
-  (b* (((when (>= from (length str))) "")
-       (next (search old str :start2 from))
-       ((unless next) (subseq str from nil)))
-    (concatenate 'string
-                 (subseq str from next)
-                 new
-                 (dumb-strsubst old new (+ (length old) next) str))))
+names between your formals and returns.</p>
+
+<h3>Features</h3>
+
+<ul>
+
+<li>The return value names specified by @(':returns') for the function are
+bound in the body of the theorem.  This way if the function is changed to
+e.g. return an additional value, @('defret') forms don't necessarily need to
+change as long as the @(':returns') specifiers are kept up to date.</li>
+
+<li>The return value names are substituted for appropriate expressions in the
+hints and rule-classes.  E.g., in the above example, an occurrence of @('d') in
+the hints or rule-classes would be replaced by @('(mv-nth 0 (my-function a b
+c))').</li>
+
+<li>Any symbol named @('<CALL>') (in any package) is replaced by the call of
+the function in the body, hints, and rule-classes.  Similarly any symbol named
+@('<FN>') is replaced by the function name or macro alias; additionally, any
+symbol named @('<FN!>') is replaced by strictly the function name (not the
+macro alias).</li>
+
+<li>The substrings @('\"<FN>\"') and @('\"<FN!>\"') are replaced in the theorem name by
+the names of the function/macro alias and function (respectively), so that
+similar theorems for different functions can be copied/pasted without editing
+the names.</li>
+
+</ul>
+
+")
 
 
 (defun defret-core (name concl-term kwd-alist disablep guts world)
@@ -1790,13 +1810,15 @@ names between your formals and returns.</p>")
                 `(implies ,hyp ,concl)
               concl))
        (thmname (intern-in-package-of-symbol
-                 (dumb-strsubst "<FN>" (symbol-name fn) 0 (symbol-name name))
+                 (dumb-str-sublis `(("<FN>" . ,(symbol-name fn))
+                                    ("<FN!>" . ,(symbol-name guts.name-fn)))
+                                  (symbol-name name))
                  name)))
     `(,(if disablep 'defthmd 'defthm) ,thmname
-      ,(sublis body-subst thm)
-      ,@(and hints?        `(:hints ,(sublis hint-subst (cdr hints?))))
+      ,(returnspec-sublis body-subst thm)
+      ,@(and hints?        `(:hints ,(returnspec-sublis hint-subst (cdr hints?))))
       ,@(and otf-flg?      `(:otf-flg ,(cdr otf-flg?)))
-      ,@(and rule-classes? `(:rule-classes ,(sublis hint-subst (cdr rule-classes?)))))))
+      ,@(and rule-classes? `(:rule-classes ,(returnspec-sublis hint-subst (cdr rule-classes?)))))))
 
 
 (defun defret-fn (name args disablep world)

books/std/util/defines.lisp

@@ -540,9 +540,9 @@ encapsulate), and is mainly meant as a tool for macro developers.</dd>
                      (concatenate 'string "RETURN-TYPE-OF-" (symbol-name fnname)
                                   "." (symbol-name x.name))
                      fnname)
-             ,(sublis body-subst formula)
-             :hints ,(sublis hint-subst x.hints)
-             :rule-classes ,(sublis hint-subst x.rule-classes)
+             ,(returnspec-sublis body-subst formula)
+             :hints ,(returnspec-sublis hint-subst x.hints)
+             :rule-classes ,(returnspec-sublis hint-subst x.rule-classes)
              :flag ,flag)
           (returnspecs-flag-entries (cdr retspecs) flag fnname binds body-subst hint-subst world))))