		Search-engine friendly clone of the ACL2 documentation.

Latchsynth

Vl-modulelist-latchsynth

Synthesize latch-like always blocks in a module list, perhaps adding some new, supporting modules.

Signature
(vl-modulelist-latchsynth x careful-p vecp) → new-x
Arguments: x — Guard (vl-modulelist-p x).; careful-p — Guard (booleanp careful-p).
Returns: new-x — Type (and (vl-modulelist-p new-x) (no-duplicatesp-equal (vl-modulelist->names new-x))) , given the guard.

Definitions and Theorems

Function: vl-modulelist-latchsynth

(defun vl-modulelist-latchsynth (x careful-p vecp)
 (declare (xargs :guard (and (vl-modulelist-p x)
                             (booleanp careful-p))))
 (let ((__function__ 'vl-modulelist-latchsynth))
  (declare (ignorable __function__))
  (b*
   ((dupes (duplicated-members (vl-modulelist->names x)))
    ((when dupes)
     (raise
      "Module names must be unique, but found multiple definitions ~
                of ~&0."
      dupes))
    ((mv new-x addmods)
     (vl-modulelist-latchsynth-aux x careful-p vecp))
    (all-mods (union (mergesort new-x)
                     (mergesort addmods)))
    (dupes (duplicated-members (vl-modulelist->names all-mods)))
    ((when dupes)
     (raise "Latchsynth caused a name collision: ~&0."
            dupes)))
   all-mods)))

Theorem: return-type-of-vl-modulelist-latchsynth

(defthm return-type-of-vl-modulelist-latchsynth
  (implies
       (and (force (vl-modulelist-p x))
            (force (booleanp careful-p)))
       (b* ((new-x (vl-modulelist-latchsynth x careful-p vecp)))
         (and (vl-modulelist-p new-x)
              (no-duplicatesp-equal (vl-modulelist->names new-x)))))
  :rule-classes :rewrite)