• 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
          • Vl-modulelist-trunc
          • Vl-make-chopped-id
          • Vl-assign-trunc
          • Vl-truncate-weirdint
          • Vl-truncate-constint
          • Vl-assignlist-trunc
          • Vl-module-trunc
          • Vl-design-trunc
          • Vl-assignlist-can-skip-trunc-p
          • Vl-assign-can-skip-trunc-p
        • Always-top
        • Gatesplit
        • Gate-elim
        • Expression-optimization
        • Elim-supplies
        • Wildelim
        • Drop-blankports
        • Clean-warnings
        • Addinstnames
        • Custom-transform-hooks
        • Annotate
        • Latchcode
        • 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

• Trunc

Vl-assign-trunc

Make any implicit truncation in an assignment explicit.

Signature

(vl-assign-trunc x delta) → (mv assign delta)

Arguments

x — Guard (vl-assign-p x).

delta — Guard (vl-delta-p delta).

Returns

assign — Type (vl-assign-p assign).

delta — Type (vl-delta-p delta).

Definitions and Theorems

Function: vl-assign-trunc

(defun vl-assign-trunc (x delta)
 (declare (xargs :guard (and (vl-assign-p x)
                             (vl-delta-p delta))))
 (let ((__function__ 'vl-assign-trunc))
  (declare (ignorable __function__))
  (b*
   ((x (vl-assign-fix x))
    (delta (vl-delta-fix delta))
    ((vl-assign x) x)
    (lhsw (vl-expr->finalwidth x.lvalue))
    (rhsw (vl-expr->finalwidth x.expr))
    ((when (or (not (posp lhsw))
               (not (posp rhsw))
               (< rhsw lhsw)))
     (mv
      x
      (dwarn
       :type :vl-programming-error
       :msg
       "~a0: expected widths to be computed and never ~
                             thought lhs would never be wider than rhs. LHS ~
                             width: ~x1.  RHS width: ~x2.  LHS: ~a3.  RHS: ~
                             ~a4."
       :args (list x lhsw rhsw x.lvalue x.expr)
       :fatalp t)))
    ((when (eql lhsw rhsw)) (mv x delta))
    ((when (and (vl-fast-atom-p x.expr)
                (vl-fast-constint-p (vl-atom->guts x.expr))
                (eq (vl-expr->finaltype x.expr)
                    :vl-unsigned)
                (vl-expr-welltyped-p x.expr)))
     (b* ((new-rhs (vl-truncate-constint lhsw x.expr))
          (x-prime (change-vl-assign x :expr new-rhs)))
       (mv x-prime delta)))
    ((when (and (vl-fast-atom-p x.expr)
                (vl-fast-weirdint-p (vl-atom->guts x.expr))
                (eq (vl-expr->finaltype x.expr)
                    :vl-unsigned)
                (vl-expr-welltyped-p x.expr)))
     (b* ((new-rhs (vl-truncate-weirdint lhsw x.expr))
          (x-prime (change-vl-assign x :expr new-rhs)))
       (mv x-prime delta)))
    ((vl-delta delta) delta)
    ((mv tmp-name nf)
     (vl-namefactory-indexed-name "trunc" delta.nf))
    (tmp-expr (vl-idexpr tmp-name rhsw :vl-unsigned))
    (type
      (change-vl-coretype *vl-plain-old-wire-type*
                          :pdims (list (vl-make-n-bit-range rhsw))))
    (tmp-decl (make-vl-vardecl :loc x.loc
                               :name tmp-name
                               :nettype :vl-wire
                               :type type))
    (tmp-assign (make-vl-assign :loc x.loc
                                :lvalue tmp-expr
                                :expr x.expr))
    (delta (change-vl-delta delta
                            :vardecls (cons tmp-decl delta.vardecls)
                            :assigns (cons tmp-assign delta.assigns)
                            :nf nf))
    (chop-expr (vl-make-chopped-id tmp-name rhsw lhsw))
    (x-prime
         (change-vl-assign x
                           :expr chop-expr
                           :atts (acons (cat "TRUNC_" (natstr lhsw))
                                        nil x.atts))))
   (mv x-prime delta))))

Theorem: vl-assign-p-of-vl-assign-trunc.assign

(defthm vl-assign-p-of-vl-assign-trunc.assign
  (b* (((mv acl2::?assign ?delta)
        (vl-assign-trunc x delta)))
    (vl-assign-p assign))
  :rule-classes :rewrite)

Theorem: vl-delta-p-of-vl-assign-trunc.delta

(defthm vl-delta-p-of-vl-assign-trunc.delta
  (b* (((mv acl2::?assign ?delta)
        (vl-assign-trunc x delta)))
    (vl-delta-p delta))
  :rule-classes :rewrite)

Theorem: vl-assign-trunc-of-vl-assign-fix-x

(defthm vl-assign-trunc-of-vl-assign-fix-x
  (equal (vl-assign-trunc (vl-assign-fix x)
                          delta)
         (vl-assign-trunc x delta)))

Theorem: vl-assign-trunc-vl-assign-equiv-congruence-on-x

(defthm vl-assign-trunc-vl-assign-equiv-congruence-on-x
  (implies (vl-assign-equiv x x-equiv)
           (equal (vl-assign-trunc x delta)
                  (vl-assign-trunc x-equiv delta)))
  :rule-classes :congruence)

Theorem: vl-assign-trunc-of-vl-delta-fix-delta

(defthm vl-assign-trunc-of-vl-delta-fix-delta
  (equal (vl-assign-trunc x (vl-delta-fix delta))
         (vl-assign-trunc x delta)))

Theorem: vl-assign-trunc-vl-delta-equiv-congruence-on-delta

(defthm vl-assign-trunc-vl-delta-equiv-congruence-on-delta
  (implies (vl-delta-equiv delta delta-equiv)
           (equal (vl-assign-trunc x delta)
                  (vl-assign-trunc x delta-equiv)))
  :rule-classes :congruence)