		Search-engine friendly clone of the ACL2 documentation.

Edgesynth

Vl-always-edgesynth

Try to synthesize a single always block.

Signature
(vl-always-edgesynth x scary vars cvtregs delta &key vecp) → (mv new-x? cvtregs delta)
Arguments: x — Always block to synthesize.
Guard (vl-always-p x).; scary — The vl-always-scary-regs for this module.
Guard (string-listp scary).; vars — All of the registers in the module.
Guard (vl-vardecllist-p vars).; cvtregs — Accumulator for the names of registers to convert into nets.
Guard (string-listp cvtregs).; delta — Delta for new nets, instances, etc.
Guard (vl-delta-p delta).
Returns: new-x? — nil on success, x unchanged on failure.
Type (equal (vl-always-p new-x?) (if new-x? t nil)), given the guard.; cvtregs — Type (string-listp cvtregs), given the guard.; delta — Type (vl-delta-p delta), given the guard.

Definitions and Theorems

Function: vl-always-edgesynth-fn

(defun vl-always-edgesynth-fn (x scary vars cvtregs delta vecp)
 (declare (xargs :guard (and (vl-always-p x)
                             (string-listp scary)
                             (vl-vardecllist-p vars)
                             (string-listp cvtregs)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-always-edgesynth))
  (declare (ignorable __function__))
  (b*
   (((vl-always x) x)
    ((unless (or (eq x.type :vl-always)
                 (eq x.type :vl-always-ff)))
     (mv x cvtregs delta))
    ((mv body ?ctrl edges)
     (vl-match-always-at-some-edges x.stmt))
    ((unless (and body (vl-edgesynth-stmt-p body)))
     (mv x cvtregs delta))
    (- (and *edgesynth-debug*
            (vl-cw-ps-seq
                 (vl-cw "~%~%--- Synthesizing Edge-Triggered ~a0.~%"
                        x)
                 (vl-pp-always x))))
    (clocks (vl-evatomlist->exprs edges))
    ((unless
          (and (vl-idexprlist-p clocks)
               (all-equalp 1 (vl-exprlist->finalwidths clocks))
               (not (member nil (vl-exprlist->finaltypes clocks)))))
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because some edges are too complex.  We ~
                                   only support simple edges like @@(posedge ~
                                   clk) or @@(negedge clk), where clk is a ~
                                   one-bit expression."
       :args (list x))))
    (edgetable (vl-make-edgetable edges))
    (clknames (alist-keys edgetable))
    (dupeclks (duplicated-members clknames))
    ((when dupeclks)
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because its sensitivity list has multiple ~
                                   occurrences of clock signals ~&1."
       :args (list x clknames))))
    (assigns (vl-edgesynth-stmt-assigns body))
    (lhses (vl-assignstmtlist->lhses assigns))
    (controls (vl-assignstmtlist->controls assigns))
    (lhs-names (mergesort (vl-idexprlist->names lhses)))
    ((when (atom lhs-names))
     (mv nil cvtregs delta))
    ((unless (eql (len lhs-names) 1))
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because more than one register gets ~
                                   written to.  Normally the edgesplit ~
                                   transform should handle this.  Did it get ~
                                   run?  Registers written: ~&1."
       :args (list x lhs-names))))
    (target-lvalue (car lhses))
    ((unless (vl-idexpr-p target-lvalue))
     (raise "impossible")
     (mv nil cvtregs delta))
    (target-name (vl-idexpr->name target-lvalue))
    (w (vl-always-check-reg target-name vars x))
    ((when w)
     (mv x cvtregs (vl-warn-delta w)))
    ((when (member-equal target-name scary))
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because the target register ~w1, is ~
                                   written to by other always blocks, which ~
                                   is too scary."
       :args (list x target-name))))
    (width (vl-expr->finalwidth target-lvalue))
    ((unless (and (posp width)
                  (all-equalp width
                              (vl-exprlist->finalwidths lhses))))
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because the target register width is not ~
                                   consistent: ~x1."
       :args (list x width))))
    ((unless (vl-edgesynth-delays-okp controls))
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because it uses unsupported or mixed delays."
       :args (list x))))
    (delay (vl-edgesynth-get-delay controls))
    (-
     (and *edgesynth-debug*
          (vl-cw-ps-seq (vl-cw ";; Initial sanity checks pass~%"))))
    (body (vl-edgesynth-stmt-blockelim body (make-vl-nullstmt)))
    (- (and *edgesynth-debug*
            (vl-cw-ps-seq (vl-cw ";; After block elimination: ~%")
                          (vl-pp-stmt body))))
    (body (vl-edgesynth-stmt-clklift body edgetable))
    (- (and *edgesynth-debug*
            (vl-cw-ps-seq (vl-cw ";; After clock-lifting: ~%")
                          (vl-pp-stmt body))))
    (clocks-in-rhs
     (intersect
      (mergesort clknames)
      (mergesort
       (vl-exprlist-names (vl-assignstmtlist->rhses
                               (vl-edgesynth-stmt-assigns body))))))
    ((when clocks-in-rhs)
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because clock signals are used in the ~
                                   right-hand sides of assignments.  This ~
                                   might be a race condition: ~&1."
       :args (list x clocks-in-rhs)
       :fatalp nil)))
    ((mv body new-nf new-vardecls new-assigns)
     (vl-edgesynth-flatten-data-ifs
          body edgetable (vl-delta->nf delta)
          (vl-delta->vardecls delta)
          (vl-delta->assigns delta)))
    (delta (change-vl-delta delta :nf new-nf))
    (new-delta (change-vl-delta delta
                                :nf new-nf
                                :vardecls new-vardecls
                                :assigns new-assigns))
    (- (and *edgesynth-debug*
            (vl-cw-ps-seq (vl-cw ";; After flattening data ifs: ~%")
                          (vl-pp-stmt body))))
    (body (vl-edgesynth-normalize-ifs body edgetable))
    (-
     (and *edgesynth-debug*
          (vl-cw-ps-seq (vl-cw ";; After normalizing clock ifs: ~%")
                        (vl-pp-stmt body))))
    ((mv okp priority-clknames rhslist final-rhs)
     (vl-edgesynth-pattern-match target-lvalue body edgetable))
    ((unless okp)
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because it did not match a supported pattern."
       :args (list x)
       :fatalp nil)))
    ((unless (uniquep priority-clknames))
     (mv
      x cvtregs
      (dwarn
       :type :vl-edgesynth-fail
       :msg
       "~a0: failing to synthesize always block ~
                                   because the IF structure ends up with ~
                                   multiple occurrences through ~&1."
       :args (list x
                   (duplicated-members priority-clknames))
       :fatalp nil)))
    (missing-clocks
         (set-difference-equal clknames priority-clknames))
    (priority-clknames (append priority-clknames missing-clocks))
    (rhslist (append rhslist
                     (replicate (len missing-clocks)
                                final-rhs)))
    ((unless (subsetp-equal priority-clknames clknames))
     (raise "Clock name problem -- this should not be possible.")
     (mv x cvtregs delta))
    (priority-edges
         (vl-edgesynth-sort-edges priority-clknames edgetable))
    ((unless (and (consp priority-edges)
                  (same-lengthp priority-edges rhslist)))
     (raise "Edge/data length problem.  Should not be possible.")
     (mv x cvtregs delta))
    (cvtregs (cons target-name cvtregs))
    (delta (vl-edgesynth-create target-lvalue priority-edges
                                rhslist delay x.loc new-delta
                                :vecp vecp)))
   (mv nil cvtregs delta))))

Theorem: return-type-of-vl-always-edgesynth.new-x?

(defthm return-type-of-vl-always-edgesynth.new-x?
 (implies
    (and (force (vl-always-p x))
         (force (string-listp scary))
         (force (vl-vardecllist-p vars))
         (force (string-listp cvtregs))
         (force (vl-delta-p delta)))
    (b* (((mv ?new-x? ?cvtregs ?delta)
          (vl-always-edgesynth-fn x scary vars cvtregs delta vecp)))
      (equal (vl-always-p new-x?)
             (if new-x? t nil))))
 :rule-classes :rewrite)

Theorem: string-listp-of-vl-always-edgesynth.cvtregs

(defthm string-listp-of-vl-always-edgesynth.cvtregs
 (implies
    (and (force (vl-always-p x))
         (force (string-listp scary))
         (force (vl-vardecllist-p vars))
         (force (string-listp cvtregs))
         (force (vl-delta-p delta)))
    (b* (((mv ?new-x? ?cvtregs ?delta)
          (vl-always-edgesynth-fn x scary vars cvtregs delta vecp)))
      (string-listp cvtregs)))
 :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-always-edgesynth.delta

(defthm vl-delta-p-of-vl-always-edgesynth.delta
 (implies
    (and (force (vl-always-p x))
         (force (string-listp scary))
         (force (vl-vardecllist-p vars))
         (force (string-listp cvtregs))
         (force (vl-delta-p delta)))
    (b* (((mv ?new-x? ?cvtregs ?delta)
          (vl-always-edgesynth-fn x scary vars cvtregs delta vecp)))
      (vl-delta-p delta)))
 :rule-classes :rewrite)