• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
      • Warnings
      • Primitives
      • Use-set
      • Syntax
      • Getting-started
      • Utilities
      • Loader
      • Transforms
        • Expression-sizing
        • Occform
        • Oprewrite
        • Expand-functions
        • Delayredux
        • Unparameterization
        • Caseelim
        • Split
        • Selresolve
        • Weirdint-elim
        • Vl-delta
        • Replicate-insts
        • Rangeresolve
        • Propagate
        • Clean-selects
        • Clean-params
        • Blankargs
        • Inline-mods
        • Expr-simp
        • Trunc
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
          • Vl-latchcode-synth-always
          • Vl-match-latch-main
          • Vl-careful-match-latch
          • Vl-careless-match-latch
          • Vl-latchcode-synth-alwayses
          • Vl-make-n-bit-latch-vec
          • Vl-make-n-bit-latch
        • Elim-unused-vars
        • Problem-modules
      • Lint
      • Mlib
      • Server
      • Kit
      • Printer
      • Esim-vl
      • Well-formedness
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Latchcode

Vl-latchcode-synth-always

Try to synthesize a single always block into a latch.

Signature

(vl-latchcode-synth-always x scary-regs 
                           vars cvtregs delta careful-p vecp) 
 
  → 
(mv new-x? cvtregs delta)

Arguments

x — always block to try to synthesize.
    Guard (vl-always-p x).

scary-regs — names of registers that are assigned to by multiple always blocks; these are too scary to try to synthesize.
    Guard (and (string-listp scary-regs) (setp scary-regs)).

vars — all the variables for the module.
    Guard (vl-vardecllist-p vars).

cvtregs — accumulator for names of registers to convert into nets.
    Guard (string-listp cvtregs).

delta — delta for the new nets, instances, etc.
    Guard (vl-delta-p delta).

careful-p — should we be careful or not?.
    Guard (booleanp careful-p).

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-latchcode-synth-always

(defun vl-latchcode-synth-always
       (x scary-regs
          vars cvtregs delta careful-p vecp)
 (declare (xargs :guard (and (vl-always-p x)
                             (and (string-listp scary-regs)
                                  (setp scary-regs))
                             (vl-vardecllist-p vars)
                             (string-listp cvtregs)
                             (vl-delta-p delta)
                             (booleanp careful-p))))
 (let ((__function__ 'vl-latchcode-synth-always))
  (declare (ignorable __function__))
  (b*
   (((vl-always x) x)
    ((unless (or (eq x.type :vl-always)
                 (eq x.type :vl-always-latch)))
     (mv x cvtregs delta))
    ((when (eq x.type :vl-always-latch))
     (mv
       x cvtregs
       (dwarn
            :type :vl-latchcode-fail
            :msg "~a0: always_latch blocks are not yet implemented."
            :args (list x))))
    (warnings (vl-delta->warnings delta))
    ((mv warnings test lhs rhs delay)
     (if careful-p (vl-careful-match-latch x warnings)
       (vl-careless-match-latch x warnings)))
    (delta (change-vl-delta delta
                            :warnings warnings))
    ((unless test) (mv x cvtregs delta))
    (lhs-names (mergesort (vl-expr-names lhs)))
    ((unless (consp lhs-names))
     (mv
      x cvtregs
      (dwarn
       :type :vl-latchcode-fail
       :msg
       "~a0: not synthesize a latch since the lhs doesn't ~
                         even have any names?  lhs: ~a1."
       :args (list x lhs-names))))
    (warning (vl-always-check-regs lhs-names vars x))
    ((when warning)
     (mv x cvtregs (vl-warn-delta warning)))
    (lhs-scary (intersect lhs-names scary-regs))
    ((unless (emptyp lhs-scary))
     (mv
      x cvtregs
      (dwarn
       :type :vl-latchcode-fail
       :msg
       "~a0: cowardly refusing to synthesize always block ~
                         for ~a1 since other always blocks write to ~a1."
       :args (list x lhs-scary))))
    ((unless (eql (vl-expr->finalwidth test) 1))
     (mv
      x cvtregs
      (dwarn
       :type :vl-latchcode-fail
       :msg
       "~a0: statement is too complex to synthesize.  The ~
                         enable for this latch is ~a1, which we expected ~
                         to have width 1, but its width is ~a2."
       :args (list x test (vl-expr->finalwidth test)))))
    (width (vl-expr->finalwidth lhs))
    ((unless (posp width))
     (mv
      x cvtregs
      (dwarn
       :type :vl-latchcode-fail
       :msg
       "~a0: can't synthesize always block becasue the width ~
                         of the lhs, ~a1, hasn't been computed or isn't a ~
                         positive number.  Its width is ~a2."
       :args (list x lhs width))))
    ((vl-delta delta) delta)
    (lhs-name (car lhs-names))
    ((mv inst-name nf)
     (vl-namefactory-plain-name (cat lhs-name "_latch")
                                delta.nf))
    ((when vecp)
     (b*
      ((addmods (vl-make-n-bit-latch-vec width (or delay 0)))
       (latchmod (car addmods))
       (inst (vl-simple-instantiate
                  latchmod inst-name (list lhs test rhs)
                  :loc x.loc))
       (delta
        (change-vl-delta
            delta
            :nf nf
            :modinsts (cons inst delta.modinsts)
            :addmods (append-without-guard addmods delta.addmods))))
      (mv nil (append lhs-names cvtregs)
          delta)))
    ((mv next-name nf)
     (vl-namefactory-plain-name (cat lhs-name "_next")
                                nf))
    ((mv delfree-name nf)
     (vl-namefactory-plain-name (cat lhs-name "_delfree")
                                nf))
    ((mv next-expr next-decl)
     (vl-occform-mkwire next-name width
                        :loc x.loc))
    ((mv delfree-expr delfree-decl)
     (vl-occform-mkwire delfree-name width
                        :loc x.loc))
    (delfree-decl
         (change-vl-vardecl
              delfree-decl
              :atts (acons "VL_TARGET_REG"
                           lhs (vl-vardecl->atts delfree-decl))))
    (next-ass (make-vl-assign :lvalue next-expr
                              :expr rhs
                              :loc x.loc))
    (addmods (vl-make-n-bit-latch width))
    (inst (vl-simple-instantiate (car addmods)
                                 inst-name
                                 (list delfree-expr test next-expr)
                                 :loc x.loc))
    (main-ass
         (make-vl-assign
              :lvalue lhs
              :expr delfree-expr
              :loc x.loc
              :delay (and delay
                          (let ((amt-expr (vl-make-index delay)))
                            (make-vl-gatedelay :rise amt-expr
                                               :fall amt-expr
                                               :high amt-expr)))))
    (cvtregs (append lhs-names cvtregs))
    (delta
       (change-vl-delta
            delta
            :nf nf
            :vardecls (list* next-decl delfree-decl delta.vardecls)
            :assigns (list* next-ass main-ass delta.assigns)
            :modinsts (cons inst delta.modinsts)
            :addmods (append-without-guard addmods delta.addmods))))
   (mv nil cvtregs delta))))

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

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

Theorem: string-listp-of-vl-latchcode-synth-always.cvtregs

(defthm string-listp-of-vl-latchcode-synth-always.cvtregs
 (implies
  (and (force (vl-always-p x))
       (force (if (string-listp scary-regs)
                  (setp scary-regs)
                'nil))
       (force (vl-vardecllist-p vars))
       (force (string-listp cvtregs))
       (force (vl-delta-p delta))
       (force (booleanp careful-p)))
  (b*
   (((mv ?new-x? ?cvtregs ?delta)
     (vl-latchcode-synth-always x scary-regs
                                vars cvtregs delta careful-p vecp)))
   (string-listp cvtregs)))
 :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-latchcode-synth-always.delta

(defthm vl-delta-p-of-vl-latchcode-synth-always.delta
 (implies
  (and (force (vl-always-p x))
       (force (if (string-listp scary-regs)
                  (setp scary-regs)
                'nil))
       (force (vl-vardecllist-p vars))
       (force (string-listp cvtregs))
       (force (vl-delta-p delta))
       (force (booleanp careful-p)))
  (b*
   (((mv ?new-x? ?cvtregs ?delta)
     (vl-latchcode-synth-always x scary-regs
                                vars cvtregs delta careful-p vecp)))
   (vl-delta-p delta)))
 :rule-classes :rewrite)