• 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-make-chopped-id

Generate the expression to truncate a wire.

Signature

(vl-make-chopped-id name name-width trunc-width) → expr

Arguments

name — name of an unsigned wire to be truncated.
    Guard (stringp name).

name-width — width of name.
    Guard (posp name-width).

trunc-width — width to truncate to.
    Guard (posp trunc-width).

Returns

expr — expression like name[truncwidth-1:0].
    Type (vl-expr-p expr).

We require that trunc-width is strictly less than width. We return the expression to truncate name down to this new trunc-width, with all of the intermediate widths set up correctly.

Definitions and Theorems

Function: vl-make-chopped-id

(defun vl-make-chopped-id (name name-width trunc-width)
  (declare (xargs :guard (and (stringp name)
                              (posp name-width)
                              (posp trunc-width))))
  (declare (xargs :guard (< trunc-width name-width)))
  (let ((__function__ 'vl-make-chopped-id))
    (declare (ignorable __function__))
    (b* ((trunc-width (lposfix trunc-width))
         (name-width (lposfix name-width))
         (name-expr (vl-idexpr name name-width :vl-unsigned))
         (left (vl-make-index (- trunc-width 1)))
         (zero (vl-make-index 0))
         ((when (eql trunc-width 1))
          (make-vl-nonatom :op :vl-bitselect
                           :args (list name-expr zero)
                           :finalwidth 1
                           :finaltype :vl-unsigned)))
      (make-vl-nonatom :op :vl-partselect-colon
                       :args (list name-expr left zero)
                       :finalwidth trunc-width
                       :finaltype :vl-unsigned))))

Theorem: vl-expr-p-of-vl-make-chopped-id

(defthm vl-expr-p-of-vl-make-chopped-id
  (b* ((expr (vl-make-chopped-id name name-width trunc-width)))
    (vl-expr-p expr))
  :rule-classes :rewrite)

Theorem: vl-make-chopped-id-of-str-fix-name

(defthm vl-make-chopped-id-of-str-fix-name
  (equal (vl-make-chopped-id (str-fix name)
                             name-width trunc-width)
         (vl-make-chopped-id name name-width trunc-width)))

Theorem: vl-make-chopped-id-streqv-congruence-on-name

(defthm vl-make-chopped-id-streqv-congruence-on-name
 (implies
     (streqv name name-equiv)
     (equal (vl-make-chopped-id name name-width trunc-width)
            (vl-make-chopped-id name-equiv name-width trunc-width)))
 :rule-classes :congruence)

Theorem: vl-make-chopped-id-of-pos-fix-name-width

(defthm vl-make-chopped-id-of-pos-fix-name-width
  (equal (vl-make-chopped-id name (pos-fix name-width)
                             trunc-width)
         (vl-make-chopped-id name name-width trunc-width)))

Theorem: vl-make-chopped-id-pos-equiv-congruence-on-name-width

(defthm vl-make-chopped-id-pos-equiv-congruence-on-name-width
 (implies
     (acl2::pos-equiv name-width name-width-equiv)
     (equal (vl-make-chopped-id name name-width trunc-width)
            (vl-make-chopped-id name name-width-equiv trunc-width)))
 :rule-classes :congruence)

Theorem: vl-make-chopped-id-of-pos-fix-trunc-width

(defthm vl-make-chopped-id-of-pos-fix-trunc-width
  (equal (vl-make-chopped-id name name-width (pos-fix trunc-width))
         (vl-make-chopped-id name name-width trunc-width)))

Theorem: vl-make-chopped-id-pos-equiv-congruence-on-trunc-width

(defthm vl-make-chopped-id-pos-equiv-congruence-on-trunc-width
 (implies
     (acl2::pos-equiv trunc-width trunc-width-equiv)
     (equal (vl-make-chopped-id name name-width trunc-width)
            (vl-make-chopped-id name name-width trunc-width-equiv)))
 :rule-classes :congruence)