• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
      • Syntax
      • Loader
        • Preprocessor
        • Vl-loadconfig
        • Vl-loadstate
        • Lexer
        • Parser
        • Vl-load-merge-descriptions
        • Vl-find-basename/extension
        • Vl-load-file
        • Vl-loadresult
        • Scope-of-defines
        • Vl-find-file
        • Vl-flush-out-descriptions
        • Vl-description
        • Vl-read-file
        • Vl-includeskips-report-gather
        • Vl-load-main
        • Extended-characters
        • Vl-load
        • Vl-load-description
        • Vl-descriptions-left-to-load
        • Inject-warnings
        • Vl-preprocess-debug
        • Vl-write-preprocessor-debug-file
        • Vl-read-file-report-gather
        • Vl-load-descriptions
        • Vl-load-files
        • Translate-off
        • Vl-load-read-file-hook
        • Vl-read-file-report
        • Vl-loadstate-pad
        • Vl-load-summary
        • Vl-collect-modules-from-descriptions
        • Vl-loadstate->warnings
        • Vl-iskips-report
        • Vl-descriptionlist
      • Warnings
      • Getting-started
      • Utilities
      • Printer
      • Kit
      • Mlib
      • Transforms
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Math
  • Testing-utilities

• Loader

Vl-load-merge-descriptions

Merge newly found Verilog descriptions with previously loaded descriptions, warning about any multiply defined descriptions.

Signature

(vl-load-merge-descriptions new old descalist reportcard) 
  → 
(mv merged new-descalist reportcard)

Arguments

new — Guard (vl-descriptionlist-p new).

old — Guard (vl-descriptionlist-p old).

descalist — Guard (equal descalist (vl-make-descalist old)).

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

Returns

merged — Type (vl-descriptionlist-p merged).

new-descalist — Type (equal new-descalist (vl-make-descalist merged)), given (equal descalist (vl-make-descalist old)).

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

As a simple rule, we always keep the first definition of any description we encounter. This function is responsible for enforcing this rule: we merge some newly parsed descriptions in with the already-parsed descriptions. If there are any name clashes, the original definition wins, and we add a warning to the reportcard to say that the original definition is being kept.

Definitions and Theorems

Function: vl-load-merge-descriptions

(defun vl-load-merge-descriptions (new old descalist reportcard)
 (declare
     (xargs :guard (and (vl-descriptionlist-p new)
                        (vl-descriptionlist-p old)
                        (vl-reportcard-p reportcard)
                        (equal descalist (vl-make-descalist old)))))
 (let ((__function__ 'vl-load-merge-descriptions))
  (declare (ignorable __function__))
  (b*
   ((old (vl-descriptionlist-fix old))
    (reportcard (vl-reportcard-fix reportcard))
    ((when (atom new))
     (mv old descalist reportcard))
    (newdesc1 (vl-description-fix (car new)))
    (newname1 (vl-description->name newdesc1))
    ((unless newname1)
     (vl-load-merge-descriptions (cdr new)
                                 (cons newdesc1 old)
                                 descalist reportcard))
    (prevdesc (vl-fast-find-description newname1 old descalist))
    ((unless prevdesc)
     (vl-load-merge-descriptions
          (cdr new)
          (cons newdesc1 old)
          (hons-acons newname1 newdesc1 descalist)
          reportcard))
    (warning
     (make-vl-warning
      :type :vl-warn-multidef
      :msg
      "~m0 is defined multiple times.  Keeping the old ~
                       definition (~a1) and ignoring the new one (~a2)."
      :args (list newname1
                  (vl-description->minloc prevdesc)
                  (vl-description->minloc newdesc1))))
    (reportcard (vl-extend-reportcard newname1 warning reportcard)))
   (vl-load-merge-descriptions (cdr new)
                               old descalist reportcard))))

Theorem: vl-descriptionlist-p-of-vl-load-merge-descriptions.merged

(defthm vl-descriptionlist-p-of-vl-load-merge-descriptions.merged
  (b* (((mv ?merged ?new-descalist ?reportcard)
        (vl-load-merge-descriptions new old descalist reportcard)))
    (vl-descriptionlist-p merged))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-load-merge-descriptions.new-descalist

(defthm return-type-of-vl-load-merge-descriptions.new-descalist
 (implies
   (equal descalist (vl-make-descalist old))
   (b* (((mv ?merged ?new-descalist ?reportcard)
         (vl-load-merge-descriptions new old descalist reportcard)))
     (equal new-descalist
            (vl-make-descalist merged))))
 :rule-classes :rewrite)

Theorem: vl-reportcard-p-of-vl-load-merge-descriptions.reportcard

(defthm vl-reportcard-p-of-vl-load-merge-descriptions.reportcard
  (b* (((mv ?merged ?new-descalist ?reportcard)
        (vl-load-merge-descriptions new old descalist reportcard)))
    (vl-reportcard-p reportcard))
  :rule-classes :rewrite)

Theorem: unique-names-after-vl-load-merge-descriptions

(defthm unique-names-after-vl-load-merge-descriptions
 (implies
   (uniquep (vl-descriptionlist->names old))
   (b* (((mv merged ?descalist ?reportcard)
         (vl-load-merge-descriptions new old descalist reportcard)))
     (no-duplicatesp (vl-descriptionlist->names merged)))))

Theorem: vl-load-merge-descriptions-of-vl-descriptionlist-fix-new

(defthm vl-load-merge-descriptions-of-vl-descriptionlist-fix-new
  (equal (vl-load-merge-descriptions (vl-descriptionlist-fix new)
                                     old descalist reportcard)
         (vl-load-merge-descriptions new old descalist reportcard)))

Theorem: vl-load-merge-descriptions-vl-descriptionlist-equiv-congruence-on-new

(defthm
 vl-load-merge-descriptions-vl-descriptionlist-equiv-congruence-on-new
 (implies
  (vl-descriptionlist-equiv new new-equiv)
  (equal
   (vl-load-merge-descriptions new old descalist reportcard)
   (vl-load-merge-descriptions new-equiv old descalist reportcard)))
 :rule-classes :congruence)

Theorem: vl-load-merge-descriptions-of-vl-descriptionlist-fix-old

(defthm vl-load-merge-descriptions-of-vl-descriptionlist-fix-old
 (equal (vl-load-merge-descriptions new (vl-descriptionlist-fix old)
                                    descalist reportcard)
        (vl-load-merge-descriptions new old descalist reportcard)))

Theorem: vl-load-merge-descriptions-vl-descriptionlist-equiv-congruence-on-old

(defthm
 vl-load-merge-descriptions-vl-descriptionlist-equiv-congruence-on-old
 (implies
  (vl-descriptionlist-equiv old old-equiv)
  (equal
   (vl-load-merge-descriptions new old descalist reportcard)
   (vl-load-merge-descriptions new old-equiv descalist reportcard)))
 :rule-classes :congruence)

Theorem: vl-load-merge-descriptions-of-vl-reportcard-fix-reportcard

(defthm vl-load-merge-descriptions-of-vl-reportcard-fix-reportcard
  (equal (vl-load-merge-descriptions new old descalist
                                     (vl-reportcard-fix reportcard))
         (vl-load-merge-descriptions new old descalist reportcard)))

Theorem: vl-load-merge-descriptions-vl-reportcard-equiv-congruence-on-reportcard

(defthm
 vl-load-merge-descriptions-vl-reportcard-equiv-congruence-on-reportcard
 (implies
  (vl-reportcard-equiv reportcard reportcard-equiv)
  (equal
   (vl-load-merge-descriptions new old descalist reportcard)
   (vl-load-merge-descriptions new old descalist reportcard-equiv)))
 :rule-classes :congruence)