← Back to branch summary

~ubuntu-branches/ubuntu/wily/acl2/wily

« back to all changes in this revision

Viewing changes to books/centaur/vl/transforms/xf-wildeq.lisp

  • Committer: Package Import Robot
  • Author(s): Camm Maguire
  • Date: 2015-01-16 10:35:45 UTC
  • mfrom: (3.3.26 sid)
  • Revision ID: package-import@ubuntu.com-20150116103545-prehe9thgo79o8w8
Tags: 7.0-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/centaur/vl/transforms/xf-wildeq.lisp
29
29
; Original author: Jared Davis <jared@centtech.com>
30
30
 
31
31
(in-package "VL")
32
 
(include-book "always/caseelim")
 
32
;; (include-book "always/caseelim")
33
33
(include-book "../mlib/delta")
34
34
(include-book "occform/util")
 
35
(include-book "../mlib/caremask")
 
36
(include-book "../mlib/blocks")
35
37
(local (include-book "../util/arithmetic"))
36
38
(local (include-book "centaur/bitops/ihsext-basics" :dir :system))
37
39
(local (std::add-default-post-define-hook :fix))
38
40
 
 
41
(local (in-theory (disable (tau-system))))
 
42
 
39
43
(local (defthm natp-when-unsigned-byte-p-width
40
44
         (implies (unsigned-byte-p n x)
41
45
                  (natp n))))
44
48
         (implies (unsigned-byte-p n x)
45
49
                  (natp x))))
46
50
 
 
51
(local (defthm vl-expr-fix-type
 
52
         (consp (vl-expr-fix x))
 
53
         :hints(("Goal" :in-theory (enable (tau-system))))
 
54
         :rule-classes :type-prescription))
 
55
 
47
56
 
48
57
(defsection wildelim
49
58
  :parents (transforms)
89
98
 
90
99
(local (xdoc::set-default-parents vl-expr-wildelim))
91
100
 
92
 
(define vl-wildeq-msb-bits-to-care-mask
93
 
  :short "Construct a bit-mask that captures the non-wild bits from the
94
 
right-hand side of a @('==?') or @('!=?') expression."
95
 
  ((msb-bits vl-bitlist-p "MSB-ordered bits from the RHS.")
96
 
   (value    natp         "Value we're constructing, zero to begin with."))
97
 
  :returns (care-mask natp :rule-classes :type-prescription)
98
 
  (b* ((value (lnfix value))
99
 
       ((when (atom msb-bits))
100
 
        value)
101
 
       (bit1  (vl-bit-fix (car msb-bits)))
102
 
       (value (if (or (eq bit1 :vl-0val)
103
 
                      (eq bit1 :vl-1val))
104
 
                  (logior 1 (ash value 1))
105
 
                (ash value 1))))
106
 
    (vl-wildeq-msb-bits-to-care-mask (cdr msb-bits) value))
107
 
  ///
108
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-zval) 0) #b0))
109
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-1val) 0) #b1))
110
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-zval :vl-zval) 0) #b00))
111
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-zval :vl-1val) 0) #b01))
112
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-1val :vl-zval) 0) #b10))
113
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-1val :vl-1val) 0) #b11))
114
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-1val :vl-zval :vl-0val :vl-1val :vl-xval) 0) #b10110))
115
 
  (assert! (equal (vl-wildeq-msb-bits-to-care-mask '(:vl-zval :vl-zval :vl-1val :vl-zval) 0) #b0010))
116
 
 
117
 
  (local (defun my-induct (n msb-bits value)
118
 
           (if (atom msb-bits)
119
 
               (list n msb-bits value)
120
 
             (my-induct (+ 1 n)
121
 
                        (cdr msb-bits)
122
 
                        (let ((bit1 (vl-bit-fix (car msb-bits))))
123
 
                          (if (or (eq bit1 :vl-0val)
124
 
                                  (eq bit1 :vl-1val))
125
 
                              (logior 1 (ash value 1))
126
 
                            (ash value 1)))))))
127
 
 
128
 
  (defthm unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-general
129
 
    (implies (unsigned-byte-p n value)
130
 
             (unsigned-byte-p (+ n (len msb-bits))
131
 
                              (vl-wildeq-msb-bits-to-care-mask msb-bits value)))
132
 
    :hints(("Goal"
133
 
            :do-not '(generalize fertilize)
134
 
            :do-not-induct t
135
 
            :induct (my-induct n msb-bits value)
136
 
            :in-theory (e/d (acl2::ihsext-recursive-redefs
137
 
                             acl2::unsigned-byte-p**)
138
 
                            (unsigned-byte-p)))))
139
 
 
140
 
  (defthm unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-zero
141
 
    (unsigned-byte-p (len msb-bits) (vl-wildeq-msb-bits-to-care-mask msb-bits 0))
142
 
    :hints(("Goal"
143
 
            :in-theory (disable unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-general
144
 
                                vl-wildeq-msb-bits-to-care-mask
145
 
                                unsigned-byte-p)
146
 
            :use ((:instance unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-general
147
 
                   (value 0) (n 0))))))
148
 
 
149
 
  (defthm upper-bound-of-vl-wildeq-msb-bits-to-care-mask-zero
150
 
    (< (vl-wildeq-msb-bits-to-care-mask msb-bits 0)
151
 
       (expt 2 (len msb-bits)))
152
 
    :rule-classes ((:rewrite) (:linear))
153
 
    :hints(("Goal" :in-theory (disable unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-zero
154
 
                                       unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-general
155
 
                                       vl-wildeq-msb-bits-to-care-mask
156
 
                                       unsigned-byte-p)
157
 
            :use ((:instance unsigned-byte-p-of-vl-wildeq-msb-bits-to-care-mask-zero))))))
158
 
 
159
 
(define vl-wildeq-msb-bits-zap
160
 
  :short "Zero out the wild bits from the right-hand side of a @('==?') or
161
 
  @('!=?') expression."
162
 
  ((msb-bits vl-bitlist-p "MSB-ordered bits from the RHS.")
163
 
   (value    natp         "Value we're constructing, zero to begin with."))
164
 
  :returns (new-value natp :rule-classes :type-prescription)
165
 
  (b* ((value (lnfix value))
166
 
       ((when (atom msb-bits))
167
 
        value)
168
 
       (bit1  (vl-bit-fix (car msb-bits)))
169
 
       (value (if (eq bit1 :vl-1val)
170
 
                  (logior 1 (ash value 1))
171
 
                ;; Just replace any other bit with 0.
172
 
                (ash value 1))))
173
 
    (vl-wildeq-msb-bits-zap (cdr msb-bits) value))
174
 
  ///
175
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-zval) 0) #b0))
176
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-xval) 0) #b0))
177
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-0val) 0) #b0))
178
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-1val) 0) #b1))
179
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-zval :vl-zval) 0) #b00))
180
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-zval :vl-1val) 0) #b01))
181
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-1val :vl-zval) 0) #b10))
182
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-1val :vl-1val) 0) #b11))
183
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-zval :vl-zval) 0) #b00))
184
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-zval :vl-0val) 0) #b00))
185
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-0val :vl-zval) 0) #b00))
186
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-0val :vl-0val) 0) #b00))
187
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-1val :vl-zval :vl-0val :vl-1val :vl-xval) 0) #b10010))
188
 
  (assert! (equal (vl-wildeq-msb-bits-zap '(:vl-zval :vl-zval :vl-1val :vl-zval) 0) #b0010))
189
 
 
190
 
  (local (defun my-induct (n msb-bits value)
191
 
           (if (atom msb-bits)
192
 
               (list n msb-bits value)
193
 
             (my-induct (+ 1 n)
194
 
                        (cdr msb-bits)
195
 
                        (let ((bit1 (vl-bit-fix (car msb-bits))))
196
 
                          (if (eq bit1 :vl-1val)
197
 
                              (logior 1 (ash value 1))
198
 
                            (ash value 1)))))))
199
 
 
200
 
  (defthm unsigned-byte-p-of-vl-wildeq-msb-bits-zap-general
201
 
    (implies (unsigned-byte-p n value)
202
 
             (unsigned-byte-p (+ n (len msb-bits))
203
 
                              (vl-wildeq-msb-bits-zap msb-bits value)))
204
 
    :hints(("Goal"
205
 
            :do-not '(generalize fertilize)
206
 
            :do-not-induct t
207
 
            :induct (my-induct n msb-bits value)
208
 
            :in-theory (e/d (acl2::ihsext-recursive-redefs
209
 
                             acl2::unsigned-byte-p**)
210
 
                            (unsigned-byte-p)))))
211
 
 
212
 
  (defthm unsigned-byte-p-of-vl-wildeq-msb-bits-zap-zero
213
 
    (unsigned-byte-p (len msb-bits) (vl-wildeq-msb-bits-zap msb-bits 0))
214
 
    :hints(("Goal"
215
 
            :in-theory (disable unsigned-byte-p-of-vl-wildeq-msb-bits-zap-general
216
 
                                vl-wildeq-msb-bits-zap
217
 
                                unsigned-byte-p)
218
 
            :use ((:instance unsigned-byte-p-of-vl-wildeq-msb-bits-zap-general
219
 
                   (value 0) (n 0))))))
220
 
 
221
 
  (defthm upper-bound-of-vl-wildeq-msb-bits-zap-zero
222
 
    (< (vl-wildeq-msb-bits-zap msb-bits 0)
223
 
       (expt 2 (len msb-bits)))
224
 
    :rule-classes ((:rewrite) (:linear))
225
 
    :hints(("Goal" :in-theory (disable unsigned-byte-p-of-vl-wildeq-msb-bits-zap-zero
226
 
                                       unsigned-byte-p-of-vl-wildeq-msb-bits-zap-general
227
 
                                       vl-wildeq-msb-bits-zap
228
 
                                       unsigned-byte-p)
229
 
            :use ((:instance unsigned-byte-p-of-vl-wildeq-msb-bits-zap-zero))))))
 
101
 
 
102
 
 
103
 
230
104
 
231
105
 
232
106
(define vl-wildeq-decompose-rhs
238
112
               (care-mask (equal (vl-expr-p care-mask) (if okp t nil)))
239
113
               (zapped    (equal (vl-expr-p zapped)    (if okp t nil))))
240
114
  :verify-guards nil
241
 
  (b* (((mv okp msb-bits) (vl-casezx-match-bits rhs))
 
115
  (b* (((mv okp msb-bits) (vl-intliteral-msb-bits rhs))
242
116
       ((unless okp)
243
117
        (mv nil nil nil))
244
118
 
245
 
       ;; Note that by len-of-vl-casezx-match-bits we know that the finalwidth
 
119
       ;; Note that by len-of-vl-intliteral-msb-bits we know that the finalwidth
246
120
       ;; is exactly the length of msb-bits.
247
121
       (finalwidth (vl-expr->finalwidth rhs))
248
122
       (finaltype  (vl-expr->finaltype rhs))
260
134
        (mv nil nil nil))
261
135
 
262
136
       ;; Care mask computation.
263
 
       (cm-value (vl-wildeq-msb-bits-to-care-mask msb-bits 0))
 
137
       (cm-value (vl-msb-bits-to-zx-care-mask msb-bits 0))
264
138
       (cm-guts  (make-vl-constint :value cm-value
265
139
                                   :origwidth finalwidth
266
140
                                   :origtype finaltype))
269
143
                               :finaltype finaltype))
270
144
 
271
145
       ;; Zapped value computation.
272
 
       (zap-value (vl-wildeq-msb-bits-zap msb-bits 0))
273
 
       (zap-guts  (make-vl-constint :value zap-value
274
 
                                    :origwidth finalwidth
275
 
                                    :origtype finaltype))
276
 
       (zap-expr  (make-vl-atom :guts zap-guts
277
 
                                :finalwidth finalwidth
278
 
                                :finaltype finaltype)))
 
146
       (zap-bits (vl-msb-bits-zap-dontcares-zx msb-bits))
 
147
       (zap-expr (vl-msb-bits-to-intliteral zap-bits finaltype)))
279
148
    (mv t cm-expr zap-expr))
280
149
  ///
 
150
  (local (defthmd consp-by-len
 
151
           (implies (posp (len x))
 
152
                    (consp x))))
281
153
  (verify-guards vl-wildeq-decompose-rhs
282
154
    :hints(("Goal"
283
 
            :in-theory (disable upper-bound-of-vl-wildeq-msb-bits-to-care-mask-zero)
284
 
            :use ((:instance upper-bound-of-vl-wildeq-msb-bits-to-care-mask-zero
285
 
                   (msb-bits (mv-nth 1 (vl-casezx-match-bits rhs))))))))
 
155
            :in-theory (e/d (consp-by-len)
 
156
                            (upper-bound-of-vl-msb-bits-to-care-mask-zero))
 
157
            :use ((:instance upper-bound-of-vl-msb-bits-to-care-mask-zero
 
158
                   (msb-bits (mv-nth 1 (vl-intliteral-msb-bits rhs)))
 
159
                   (cares '(:vl-0val :vl-1val)))))))
286
160
 
287
161
  (local (in-theory (enable vl-expr-welltyped-p
288
162
                            vl-atom-welltyped-p)))
438
312
 
439
313
 
440
314
(define vl-wildeq-rewrite-main ((x        vl-expr-p)
441
 
                                (elem     vl-modelement-p)
 
315
                                (ctx      vl-context-p)
442
316
                                (warnings vl-warninglist-p))
443
317
  :guard (and (not (vl-atom-p x))
444
318
              (or (eq (vl-nonatom->op x) :vl-binary-wildeq)
447
321
               (new-x        vl-expr-p))
448
322
  :verify-guards nil
449
323
  (b* ((x    (vl-expr-fix x))
450
 
       (elem (vl-modelement-fix elem))
 
324
       (ctx (vl-context-fix ctx))
451
325
 
452
326
       ((unless (vl-expr-welltyped-p x))
453
327
        (mv (warn :type :vl-wildeq-fail
454
328
                  :msg "~a0: failing to simplify wildcard equality operator ~
455
329
                        because it is not well-typed: ~a1."
456
 
                  :args (list elem x))
 
330
                  :args (list ctx x))
457
331
            x))
458
332
 
459
333
       ((vl-nonatom x) x)
465
339
                  :msg  "~a0: right-hand side of wildcard equality operator ~
466
340
                         is too complex; we only support constants.  ~
467
341
                         Expression: ~a1."
468
 
                  :args (list elem x))
 
342
                  :args (list ctx x))
469
343
            x))
470
344
 
471
345
       (new-x (if (eq x.op :vl-binary-wildeq)
494
368
                  (not (vl-atom-p x))
495
369
                  (or (eq (vl-nonatom->op x) :vl-binary-wildeq)
496
370
                      (eq (vl-nonatom->op x) :vl-binary-wildneq)))
497
 
             (b* (((mv ?warnings new-x) (vl-wildeq-rewrite-main x elem warnings)))
 
371
             (b* (((mv ?warnings new-x) (vl-wildeq-rewrite-main x ctx warnings)))
498
372
               (and (vl-expr-welltyped-p new-x)
499
373
                    (equal (vl-expr->finalwidth new-x)
500
374
                           (vl-expr->finalwidth x))
509
383
  (define vl-wildeq-rewrite-expr
510
384
    :short "Eliminate @('==?') and @('!=?') operators from an expression."
511
385
    ((x        vl-expr-p       "Expression to process.")
512
 
     (elem     vl-modelement-p "Context for error messages.")
 
386
     (ctx      vl-context-p "Context for error messages.")
513
387
     (warnings vl-warninglist-p))
514
388
    :verify-guards nil
515
389
    :returns (mv (new-warnings vl-warninglist-p)
527
401
          (mv (ok) x))
528
402
 
529
403
         ((mv warnings new-args)
530
 
          (vl-wildeq-rewrite-exprlist x.args elem warnings))
 
404
          (vl-wildeq-rewrite-exprlist x.args ctx warnings))
531
405
         (new-x (change-vl-nonatom x :args new-args))
532
406
 
533
407
         ((when (or (eq x.op :vl-binary-wildeq)
534
408
                    (eq x.op :vl-binary-wildneq)))
535
 
          (vl-wildeq-rewrite-main new-x elem warnings)))
 
409
          (vl-wildeq-rewrite-main new-x ctx warnings)))
536
410
 
537
411
      (mv warnings (change-vl-nonatom x :args new-args))))
538
412
 
539
413
  (define vl-wildeq-rewrite-exprlist
540
414
    :short "Eliminate @('==?') and @('!=?') operators from an expression list."
541
415
    ((x        vl-exprlist-p)
542
 
     (elem     vl-modelement-p)
 
416
     (ctx      vl-context-p)
543
417
     (warnings vl-warninglist-p))
544
418
    :returns (mv (warnings vl-warninglist-p)
545
419
                 (new-x    (and (vl-exprlist-p new-x)
548
422
    :flag :list
549
423
    (b* (((when (atom x))
550
424
          (mv (ok) x))
551
 
         ((mv warnings car) (vl-wildeq-rewrite-expr (car x) elem warnings))
552
 
         ((mv warnings cdr) (vl-wildeq-rewrite-exprlist (cdr x) elem warnings)))
 
425
         ((mv warnings car) (vl-wildeq-rewrite-expr (car x) ctx warnings))
 
426
         ((mv warnings cdr) (vl-wildeq-rewrite-exprlist (cdr x) ctx warnings)))
553
427
      (mv warnings (cons car cdr))))
554
428
 
555
429
  ///
565
439
 
566
440
  (defthm vl-wildeq-rewrite-exprlist-when-atom
567
441
    (implies (atom x)
568
 
             (equal (vl-wildeq-rewrite-exprlist x elem warnings)
 
442
             (equal (vl-wildeq-rewrite-exprlist x ctx warnings)
569
443
                    (mv (ok) x))))
570
444
 
571
445
  (defthm vl-wildeq-rewrite-exprlist-of-cons
572
 
    (equal (vl-wildeq-rewrite-exprlist (cons a x) elem warnings)
573
 
           (b* (((mv warnings car) (vl-wildeq-rewrite-expr a elem warnings))
574
 
                ((mv warnings cdr) (vl-wildeq-rewrite-exprlist x elem warnings)))
 
446
    (equal (vl-wildeq-rewrite-exprlist (cons a x) ctx warnings)
 
447
           (b* (((mv warnings car) (vl-wildeq-rewrite-expr a ctx warnings))
 
448
                ((mv warnings cdr) (vl-wildeq-rewrite-exprlist x ctx warnings)))
575
449
             (mv warnings (cons car cdr)))))
576
450
 
577
451
  (defthm len-of-vl-wildeq-rewrite-exprlist
578
 
    (equal (len (mv-nth 1 (vl-wildeq-rewrite-exprlist x elem warnings)))
 
452
    (equal (len (mv-nth 1 (vl-wildeq-rewrite-exprlist x ctx warnings)))
579
453
           (len x)))
580
454
 
581
455
  (local (defthm l0
593
467
  (defthm-vl-wildeq-rewrite-expr-flag
594
468
    (defthm vl-wildeq-rewrite-expr-optimization
595
469
      (implies (not (vl-expr-has-ops '(:vl-binary-wildeq :vl-binary-wildneq) x))
596
 
               (equal (vl-wildeq-rewrite-expr x elem warnings)
 
470
               (equal (vl-wildeq-rewrite-expr x ctx warnings)
597
471
                      (mv (ok) (vl-expr-fix x))))
598
472
      :flag :expr)
599
473
    (defthm vl-wildeq-rewrite-exprlist-optimization
600
474
      (implies (not (vl-exprlist-has-ops '(:vl-binary-wildeq :vl-binary-wildneq) x))
601
 
               (equal (vl-wildeq-rewrite-exprlist x elem warnings)
 
475
               (equal (vl-wildeq-rewrite-exprlist x ctx warnings)
602
476
                      (mv (ok) (vl-exprlist-fix x))))
603
477
      :flag :list)
604
478
    :hints(("Goal"
605
 
            :expand ((vl-wildeq-rewrite-expr x elem warnings)
 
479
            :expand ((vl-wildeq-rewrite-expr x ctx warnings)
606
480
                     (vl-exprlist-ops x))
607
481
            :do-not '(generalize fertilize)))))
608
482
 
612
486
          expression.  Avoids reconsing when there are no @('==?') or @('!=?')
613
487
          operators."
614
488
  ((x        vl-expr-p)
615
 
   (elem     vl-modelement-p)
 
489
   (ctx      vl-context-p)
616
490
   (warnings vl-warninglist-p))
617
491
  :returns (mv (new-warnings vl-warninglist-p)
618
492
               (new-x vl-expr-p))
619
493
  :enabled t
620
494
  (mbe :logic
621
 
       (vl-wildeq-rewrite-expr x elem warnings)
 
495
       (vl-wildeq-rewrite-expr x ctx warnings)
622
496
       :exec
623
497
       (if (not (vl-expr-has-ops '(:vl-binary-wildeq :vl-binary-wildneq) x))
624
498
           (mv warnings x)
625
 
         (vl-wildeq-rewrite-expr x elem warnings))))
 
499
         (vl-wildeq-rewrite-expr x ctx warnings))))
626
500
 
627
501
 
628
502
 
632
506
 
633
507
(local (xdoc::set-default-parents vl-design-wildelim))
634
508
 
635
 
(defmacro def-vl-wildelim (name &key body takes-elem enabled inline)
 
509
(defmacro def-vl-wildelim (name &key body takes-ctx enabled (inline ':default))
636
510
  (b* ((mksym-package-symbol (pkg-witness "VL"))
637
511
       (fn   (mksym name '-wildelim))
638
512
       (fix  (mksym name '-fix))
639
513
       (type (mksym name '-p)))
640
514
    `(define ,fn ((x      ,type)
641
 
                  ,@(and takes-elem '((elem vl-modelement-p)))
 
515
                  ,@(and takes-ctx '((ctx  vl-context-p)))
642
516
                  (warnings vl-warninglist-p))
643
517
       :short ,(cat "Eliminate @('==?') and @('!=?') operators throughout a @(see " (symbol-name type) ")")
644
518
       :returns (mv (warnings vl-warninglist-p)
649
523
            (warnings (vl-warninglist-fix warnings)))
650
524
         ,body))))
651
525
 
652
 
(defmacro def-vl-wildelim-list (name &key element takes-elem)
 
526
(defmacro def-vl-wildelim-list (name &key element takes-ctx)
653
527
  (b* ((mksym-package-symbol (pkg-witness "VL"))
654
528
       (fn      (mksym name    '-wildelim))
655
 
       (elem-fn (mksym element '-wildelim))
 
529
       (ctx-fn (mksym element '-wildelim))
656
530
       (type    (mksym name    '-p))
657
531
       (formals (append '(x)
658
 
                        (if takes-elem '(elem) nil)
 
532
                        (if takes-ctx '(ctx) nil)
659
533
                        '(warnings))))
660
534
    `(define ,fn ((x      ,type)
661
 
                  ,@(and takes-elem '((elem vl-modelement-p)))
 
535
                  ,@(and takes-ctx '((ctx  vl-context-p)))
662
536
                  (warnings vl-warninglist-p))
663
537
       :returns (mv (warnings vl-warninglist-p)
664
538
                    (new-x    ,type))
665
539
       :short ,(cat "Eliminate @('==?') and @('!=?') operators throughout a @(see " (symbol-name type) ").")
666
540
       (b* (((when (atom x))
667
541
             (mv (ok) x))
668
 
            ((mv warnings car-prime) (,elem-fn . ,(subst '(car x) 'x formals)))
 
542
            ((mv warnings car-prime) (,ctx-fn . ,(subst '(car x) 'x formals)))
669
543
            ((mv warnings cdr-prime) (,fn . ,(subst '(cdr x) 'x formals))))
670
544
         (mv warnings (cons car-prime cdr-prime)))
671
545
       ///
676
550
 
677
551
       (defthm ,(mksym fn '-of-cons)
678
552
         (equal (,fn . ,(subst '(cons a x) 'x formals))
679
 
                (b* (((mv warnings car-prime) (,elem-fn . ,(subst 'a 'x formals)))
 
553
                (b* (((mv warnings car-prime) (,ctx-fn . ,(subst 'a 'x formals)))
680
554
                     ((mv warnings cdr-prime) (,fn . ,formals)))
681
555
                  (mv warnings (cons car-prime cdr-prime)))))
682
556
 
685
559
                (len x))))))
686
560
 
687
561
(def-vl-wildelim vl-exprlist
688
 
  :takes-elem t
 
562
  :takes-ctx t
689
563
  :enabled t
690
564
  :body
691
565
  (mbe :logic
692
 
       (vl-wildeq-rewrite-exprlist x elem warnings)
 
566
       (vl-wildeq-rewrite-exprlist x ctx warnings)
693
567
       :exec
694
568
       ;; Optimization to avoid reconsing.  If there aren't any ==? or !=?
695
569
       ;; operators, don't do anything.
696
570
       (if (not (vl-exprlist-has-ops '(:vl-binary-wildeq :vl-binary-wildneq) x))
697
571
           (mv warnings x)
698
 
         (vl-wildeq-rewrite-exprlist x elem warnings))))
 
572
         (vl-wildeq-rewrite-exprlist x ctx warnings))))
699
573
 
700
574
(def-vl-wildelim vl-maybe-expr
701
 
  :takes-elem t
 
575
  :takes-ctx t
702
576
  :inline t
703
577
  :body (if x
704
 
            (vl-expr-wildelim x elem warnings)
 
578
            (vl-expr-wildelim x ctx warnings)
705
579
          (mv warnings nil)))
706
580
 
707
581
(def-vl-wildelim vl-range
708
 
  :takes-elem t
 
582
  :takes-ctx t
709
583
  :body (b* (((vl-range x) x)
710
 
             ((mv warnings msb-prime) (vl-expr-wildelim x.msb elem warnings))
711
 
             ((mv warnings lsb-prime) (vl-expr-wildelim x.lsb elem warnings))
 
584
             ((mv warnings msb-prime) (vl-expr-wildelim x.msb ctx warnings))
 
585
             ((mv warnings lsb-prime) (vl-expr-wildelim x.lsb ctx warnings))
712
586
             (x-prime  (change-vl-range x
713
587
                                        :msb msb-prime
714
588
                                        :lsb lsb-prime)))
715
589
          (mv warnings x-prime)))
716
590
 
717
591
(def-vl-wildelim vl-maybe-range
718
 
  :takes-elem t
 
592
  :takes-ctx t
719
593
  :inline t
720
594
  :body (if x
721
 
            (vl-range-wildelim x elem warnings)
 
595
            (vl-range-wildelim x ctx warnings)
722
596
          (mv warnings nil)))
723
597
 
724
598
(def-vl-wildelim-list vl-rangelist
725
 
  :takes-elem t
 
599
  :takes-ctx t
726
600
  :element vl-range)
727
601
 
728
602
(def-vl-wildelim vl-packeddimension
729
 
  :takes-elem t
 
603
  :takes-ctx t
730
604
  :inline t
731
605
  :body
732
606
  (b* ((x (vl-packeddimension-fix x)))
733
607
    (if (eq x :vl-unsized-dimension)
734
608
        (mv warnings x)
735
 
      (vl-range-wildelim x elem warnings))))
 
609
      (vl-range-wildelim x ctx warnings))))
736
610
 
737
611
(def-vl-wildelim vl-maybe-packeddimension
738
 
  :takes-elem t
 
612
  :takes-ctx t
739
613
  :inline t
740
614
  :body
741
615
  (if x
742
 
      (vl-packeddimension-wildelim x elem warnings)
 
616
      (vl-packeddimension-wildelim x ctx warnings)
743
617
    (mv warnings x)))
744
618
 
745
619
(def-vl-wildelim-list vl-packeddimensionlist
746
 
  :takes-elem t
 
620
  :takes-ctx t
747
621
  :element vl-packeddimension)
748
622
 
749
623
(def-vl-wildelim vl-enumbasetype
750
 
  :takes-elem t
 
624
  :takes-ctx t
751
625
  :body (b* (((vl-enumbasetype x) x)
752
626
             ((mv warnings dim)
753
 
              (vl-maybe-packeddimension-wildelim x.dim elem warnings)))
 
627
              (vl-maybe-packeddimension-wildelim x.dim ctx warnings)))
754
628
          (mv warnings (change-vl-enumbasetype x :dim dim))))
755
629
 
756
630
(def-vl-wildelim vl-enumitem
757
 
  :takes-elem t
 
631
  :takes-ctx t
758
632
  :body
759
633
  (b* (((vl-enumitem x) x)
760
 
       ((mv warnings new-range) (vl-maybe-range-wildelim x.range elem warnings))
761
 
       ((mv warnings new-value) (vl-maybe-expr-wildelim x.value elem warnings))
 
634
       ((mv warnings new-range) (vl-maybe-range-wildelim x.range ctx warnings))
 
635
       ((mv warnings new-value) (vl-maybe-expr-wildelim x.value ctx warnings))
762
636
       (new-x    (change-vl-enumitem x
763
637
                                     :range new-range
764
638
                                     :value new-value)))
765
639
    (mv warnings new-x)))
766
640
 
767
641
(def-vl-wildelim-list vl-enumitemlist
768
 
  :takes-elem t
 
642
  :takes-ctx t
769
643
  :element vl-enumitem)
770
644
 
771
645
 
773
647
  :verify-guards nil
774
648
 
775
649
  (define vl-datatype-wildelim ((x        vl-datatype-p)
776
 
                                (elem     vl-modelement-p)
 
650
                                (ctx      vl-context-p)
777
651
                                (warnings vl-warninglist-p))
778
652
    :returns (mv (warnings vl-warninglist-p)
779
653
                 (new-x    vl-datatype-p))
780
654
    :measure (vl-datatype-count x)
781
655
    (vl-datatype-case x
782
656
      (:vl-coretype
783
 
       (b* (((mv warnings new-dims) (vl-packeddimensionlist-wildelim x.dims elem warnings))
784
 
            (new-x (change-vl-coretype x :dims new-dims)))
 
657
       (b* (((mv warnings new-pdims) (vl-packeddimensionlist-wildelim x.pdims ctx warnings))
 
658
            ((mv warnings new-udims) (vl-packeddimensionlist-wildelim x.udims ctx warnings))
 
659
            (new-x (change-vl-coretype x :pdims new-pdims :udims new-udims)))
785
660
         (mv warnings new-x)))
786
661
      (:vl-struct
787
 
       (b* (((mv warnings new-members) (vl-structmemberlist-wildelim x.members elem warnings))
788
 
            ((mv warnings new-dims) (vl-packeddimensionlist-wildelim x.dims elem warnings))
789
 
            (new-x    (change-vl-struct x :members new-members :dims new-dims)))
 
662
       (b* (((mv warnings new-members) (vl-structmemberlist-wildelim x.members ctx warnings))
 
663
            ((mv warnings new-pdims) (vl-packeddimensionlist-wildelim x.pdims ctx warnings))
 
664
            ((mv warnings new-udims) (vl-packeddimensionlist-wildelim x.udims ctx warnings))
 
665
            (new-x    (change-vl-struct x :members new-members :pdims new-pdims :udims new-udims)))
790
666
         (mv warnings new-x)))
791
667
      (:vl-union
792
 
       (b* (((mv warnings new-members) (vl-structmemberlist-wildelim x.members elem warnings))
793
 
            ((mv warnings new-dims) (vl-packeddimensionlist-wildelim x.dims elem warnings))
794
 
            (new-x    (change-vl-union x :members new-members :dims new-dims)))
 
668
       (b* (((mv warnings new-members) (vl-structmemberlist-wildelim x.members ctx warnings))
 
669
            ((mv warnings new-pdims) (vl-packeddimensionlist-wildelim x.pdims ctx warnings))
 
670
            ((mv warnings new-udims) (vl-packeddimensionlist-wildelim x.udims ctx warnings))
 
671
            (new-x    (change-vl-union x :members new-members :pdims new-pdims :udims new-udims)))
795
672
         (mv warnings new-x)))
796
673
      (:vl-enum
797
 
       (b* (((mv warnings new-basetype) (vl-enumbasetype-wildelim x.basetype elem warnings))
798
 
            ((mv warnings new-items) (vl-enumitemlist-wildelim x.items elem warnings))
799
 
            ((mv warnings new-dims) (vl-packeddimensionlist-wildelim x.dims elem warnings))
 
674
       (b* (((mv warnings new-basetype) (vl-enumbasetype-wildelim x.basetype ctx warnings))
 
675
            ((mv warnings new-items) (vl-enumitemlist-wildelim x.items ctx warnings))
 
676
            ((mv warnings new-pdims) (vl-packeddimensionlist-wildelim x.pdims ctx warnings))
 
677
            ((mv warnings new-udims) (vl-packeddimensionlist-wildelim x.udims ctx warnings))
800
678
            (new-x    (change-vl-enum x
801
679
                                      :basetype new-basetype
802
680
                                      :items new-items
803
 
                                      :dims new-dims)))
 
681
                                      :pdims new-pdims :udims new-udims)))
804
682
         (mv warnings new-x)))
805
683
      (:vl-usertype
806
 
       (b* (((mv warnings new-kind) (vl-expr-wildelim x.kind elem warnings))
807
 
            ((mv warnings new-dims) (vl-packeddimensionlist-wildelim x.dims elem warnings))
808
 
            (new-x    (change-vl-usertype x :kind new-kind :dims new-dims)))
 
684
       (b* (((mv warnings new-kind) (vl-expr-wildelim x.kind ctx warnings))
 
685
            ((mv warnings new-pdims) (vl-packeddimensionlist-wildelim x.pdims ctx warnings))
 
686
            ((mv warnings new-udims) (vl-packeddimensionlist-wildelim x.udims ctx warnings))
 
687
            (new-x    (change-vl-usertype x :kind new-kind :pdims new-pdims :udims new-udims)))
809
688
         (mv warnings new-x)))))
810
689
 
811
690
  (define vl-structmemberlist-wildelim ((x        vl-structmemberlist-p)
812
 
                                        (elem     vl-modelement-p)
 
691
                                        (ctx      vl-context-p)
813
692
                                        (warnings vl-warninglist-p))
814
693
    :returns (mv (warnings vl-warninglist-p)
815
694
                 (new-x    vl-structmemberlist-p))
816
695
    :measure (vl-structmemberlist-count x)
817
696
    (b* (((when (atom x))
818
697
          (mv (ok) nil))
819
 
         ((mv warnings new-car) (vl-structmember-wildelim (car x) elem warnings))
820
 
         ((mv warnings new-cdr) (vl-structmemberlist-wildelim (cdr x) elem warnings))
 
698
         ((mv warnings new-car) (vl-structmember-wildelim (car x) ctx warnings))
 
699
         ((mv warnings new-cdr) (vl-structmemberlist-wildelim (cdr x) ctx warnings))
821
700
         (new-x    (cons new-car new-cdr)))
822
701
      (mv warnings new-x)))
823
702
 
824
703
  (define vl-structmember-wildelim ((x        vl-structmember-p)
825
 
                                    (elem     vl-modelement-p)
 
704
                                    (ctx      vl-context-p)
826
705
                                    (warnings vl-warninglist-p))
827
706
    :returns (mv (warnings vl-warninglist-p)
828
707
                 (new-x    vl-structmember-p))
829
708
    :measure (vl-structmember-count x)
830
709
    (b* (((vl-structmember x) x)
831
 
         ((mv warnings new-type) (vl-datatype-wildelim x.type elem warnings))
832
 
         ((mv warnings new-dims) (vl-packeddimensionlist-wildelim x.dims elem warnings))
833
 
         ((mv warnings new-rhs) (vl-maybe-expr-wildelim x.rhs elem warnings))
 
710
         ((mv warnings new-type) (vl-datatype-wildelim x.type ctx warnings))
 
711
         ((mv warnings new-rhs) (vl-maybe-expr-wildelim x.rhs ctx warnings))
834
712
         (new-x    (change-vl-structmember x
835
713
                                           :type new-type
836
 
                                           :dims new-dims
837
714
                                           :rhs new-rhs)))
838
715
      (mv warnings new-x)))
839
716
  ///
840
717
  (verify-guards vl-datatype-wildelim)
841
718
  (deffixequiv-mutual vl-datatype-wildelim))
842
719
 
 
720
(def-vl-wildelim vl-maybe-datatype
 
721
  :takes-ctx t
 
722
  :inline t
 
723
  :body
 
724
  (if x
 
725
      (vl-datatype-wildelim x ctx warnings)
 
726
    (mv warnings x)))
 
727
 
843
728
(def-vl-wildelim vl-gatedelay
844
 
  :takes-elem t
 
729
  :takes-ctx t
845
730
  :body (b* (((vl-gatedelay x) x)
846
 
             ((mv warnings rise-prime) (vl-expr-wildelim x.rise elem warnings))
847
 
             ((mv warnings fall-prime) (vl-expr-wildelim x.fall elem warnings))
848
 
             ((mv warnings high-prime) (vl-maybe-expr-wildelim x.high elem warnings))
 
731
             ((mv warnings rise-prime) (vl-expr-wildelim x.rise ctx warnings))
 
732
             ((mv warnings fall-prime) (vl-expr-wildelim x.fall ctx warnings))
 
733
             ((mv warnings high-prime) (vl-maybe-expr-wildelim x.high ctx warnings))
849
734
             (x-prime  (change-vl-gatedelay x
850
735
                                            :rise rise-prime
851
736
                                            :fall fall-prime
853
738
          (mv warnings x-prime)))
854
739
 
855
740
(def-vl-wildelim vl-maybe-gatedelay
856
 
  :takes-elem t
 
741
  :takes-ctx t
857
742
  :inline t
858
743
  :body (if x
859
 
            (vl-gatedelay-wildelim x elem warnings)
 
744
            (vl-gatedelay-wildelim x ctx warnings)
860
745
          (mv warnings x)))
861
746
 
862
747
(def-vl-wildelim vl-assign
863
748
  :body
864
749
  (b* (((vl-assign x) x)
865
 
       (elem x)
866
 
       ((mv warnings lhs-prime)   (vl-expr-wildelim x.lvalue elem warnings))
867
 
       ((mv warnings rhs-prime)   (vl-expr-wildelim x.expr elem warnings))
868
 
       ((mv warnings delay-prime) (vl-maybe-gatedelay-wildelim x.delay elem warnings))
 
750
       (ctx x)
 
751
       ((mv warnings lhs-prime)   (vl-expr-wildelim x.lvalue ctx warnings))
 
752
       ((mv warnings rhs-prime)   (vl-expr-wildelim x.expr ctx warnings))
 
753
       ((mv warnings delay-prime) (vl-maybe-gatedelay-wildelim x.delay ctx warnings))
869
754
       (x-prime
870
755
        (change-vl-assign x
871
756
                          :lvalue lhs-prime
877
762
 
878
763
 
879
764
(def-vl-wildelim vl-plainarg
880
 
  :takes-elem t
 
765
  :takes-ctx t
881
766
  :body (b* (((vl-plainarg x) x)
882
767
             ((unless x.expr)
883
768
              (mv warnings x))
884
 
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr elem warnings))
 
769
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr ctx warnings))
885
770
             (x-prime (change-vl-plainarg x :expr expr-prime)))
886
771
          (mv warnings x-prime)))
887
772
 
888
773
(def-vl-wildelim-list vl-plainarglist
889
 
  :takes-elem t
 
774
  :takes-ctx t
890
775
  :element vl-plainarg)
891
776
 
892
777
(def-vl-wildelim vl-namedarg
893
 
  :takes-elem t
 
778
  :takes-ctx t
894
779
  :body (b* (((vl-namedarg x) x)
895
780
             ((unless x.expr)
896
781
              (mv warnings x))
897
 
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr elem warnings))
 
782
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr ctx warnings))
898
783
             (x-prime (change-vl-namedarg x :expr expr-prime)))
899
784
          (mv warnings x-prime)))
900
785
 
901
786
(def-vl-wildelim-list vl-namedarglist
902
 
  :takes-elem t
 
787
  :takes-ctx t
903
788
  :element vl-namedarg)
904
789
 
905
790
(def-vl-wildelim vl-arguments
906
 
  :takes-elem t
 
791
  :takes-ctx t
907
792
  :body
908
793
  (vl-arguments-case x
909
 
    :named
910
 
    (b* (((mv warnings args-prime) (vl-namedarglist-wildelim x.args elem warnings))
 
794
    :vl-arguments-named
 
795
    (b* (((mv warnings args-prime) (vl-namedarglist-wildelim x.args ctx warnings))
911
796
         (x-prime (change-vl-arguments-named x :args args-prime)))
912
797
      (mv warnings x-prime))
913
 
    :plain
914
 
    (b* (((mv warnings args-prime) (vl-plainarglist-wildelim x.args elem warnings))
 
798
    :vl-arguments-plain
 
799
    (b* (((mv warnings args-prime) (vl-plainarglist-wildelim x.args ctx warnings))
915
800
         (x-prime (change-vl-arguments-plain x :args args-prime)))
916
801
      (mv warnings x-prime))))
917
802
 
 
803
(def-vl-wildelim vl-paramvalue
 
804
  :takes-ctx t
 
805
  :body
 
806
  (vl-paramvalue-case x
 
807
    :expr     (vl-expr-wildelim x ctx warnings)
 
808
    :datatype (vl-datatype-wildelim x ctx warnings)))
 
809
 
 
810
(def-vl-wildelim-list vl-paramvaluelist
 
811
  :takes-ctx t
 
812
  :element vl-paramvalue)
 
813
 
 
814
(def-vl-wildelim vl-maybe-paramvalue
 
815
  :takes-ctx t
 
816
  :inline t
 
817
  :body (if x
 
818
            (vl-paramvalue-wildelim x ctx warnings)
 
819
          (mv warnings x)))
 
820
 
 
821
(def-vl-wildelim vl-namedparamvalue
 
822
  :takes-ctx t
 
823
  :body
 
824
  (b* (((vl-namedparamvalue x) x)
 
825
       ((mv warnings value) (vl-maybe-paramvalue-wildelim x.value ctx warnings)))
 
826
    (mv warnings (change-vl-namedparamvalue x :value value))))
 
827
 
 
828
(def-vl-wildelim-list vl-namedparamvaluelist
 
829
  :takes-ctx t
 
830
  :element vl-namedparamvalue)
 
831
 
 
832
(def-vl-wildelim vl-paramargs
 
833
  :takes-ctx t
 
834
  :body
 
835
  (vl-paramargs-case x
 
836
    :vl-paramargs-named
 
837
    (b* (((mv warnings args) (vl-namedparamvaluelist-wildelim x.args ctx warnings)))
 
838
      (mv warnings (change-vl-paramargs-named x :args args)))
 
839
    :vl-paramargs-plain
 
840
    (b* (((mv warnings args) (vl-paramvaluelist-wildelim x.args ctx warnings)))
 
841
      (mv warnings (change-vl-paramargs-plain x :args args)))))
 
842
 
918
843
(def-vl-wildelim vl-modinst
919
844
  :body
920
845
  (b* (((vl-modinst x) x)
921
 
       (elem x)
922
 
       ((mv warnings portargs-prime)  (vl-arguments-wildelim x.portargs elem warnings))
923
 
       ((mv warnings paramargs-prime) (vl-arguments-wildelim x.paramargs elem warnings))
924
 
       ((mv warnings range-prime)     (vl-maybe-range-wildelim x.range elem warnings))
925
 
       ((mv warnings delay-prime)     (vl-maybe-gatedelay-wildelim x.delay elem warnings))
 
846
       (ctx x)
 
847
       ((mv warnings portargs-prime)  (vl-arguments-wildelim x.portargs ctx warnings))
 
848
       ((mv warnings paramargs-prime) (vl-paramargs-wildelim x.paramargs ctx warnings))
 
849
       ((mv warnings range-prime)     (vl-maybe-range-wildelim x.range ctx warnings))
 
850
       ((mv warnings delay-prime)     (vl-maybe-gatedelay-wildelim x.delay ctx warnings))
926
851
       (x-prime (change-vl-modinst x
927
852
                                   :portargs portargs-prime
928
853
                                   :paramargs paramargs-prime
935
860
(def-vl-wildelim vl-gateinst
936
861
  :body
937
862
  (b* (((vl-gateinst x) x)
938
 
       (elem x)
939
 
       ((mv warnings args-prime) (vl-plainarglist-wildelim x.args elem warnings))
940
 
       ((mv warnings range-prime) (vl-maybe-range-wildelim x.range elem warnings))
941
 
       ((mv warnings delay-prime) (vl-maybe-gatedelay-wildelim x.delay elem warnings))
 
863
       (ctx x)
 
864
       ((mv warnings args-prime) (vl-plainarglist-wildelim x.args ctx warnings))
 
865
       ((mv warnings range-prime) (vl-maybe-range-wildelim x.range ctx warnings))
 
866
       ((mv warnings delay-prime) (vl-maybe-gatedelay-wildelim x.delay ctx warnings))
942
867
       (x-prime (change-vl-gateinst x
943
868
                                    :args args-prime
944
869
                                    :range range-prime
949
874
 
950
875
 
951
876
(def-vl-wildelim vl-port
952
 
  :body (b* (((vl-port x) x)
953
 
             (elem x)
954
 
             ((mv warnings expr-prime) (vl-maybe-expr-wildelim x.expr elem warnings))
955
 
             (x-prime (change-vl-port x :expr expr-prime)))
 
877
  :body (b* ((x (vl-port-fix x))
 
878
             (ctx (vl-context x))
 
879
             ((when (eq (tag x) :vl-interfaceport))
 
880
              (b* (((vl-interfaceport x))
 
881
                   ((mv warnings udims-prime)
 
882
                    (vl-packeddimensionlist-wildelim x.udims ctx warnings)))
 
883
                (mv warnings (change-vl-interfaceport x :udims udims-prime))))
 
884
             ((vl-regularport x) x)
 
885
             ((mv warnings expr-prime) (vl-maybe-expr-wildelim x.expr ctx warnings))
 
886
             (x-prime (change-vl-regularport x
 
887
                                      :expr expr-prime)))
956
888
          (mv warnings x-prime)))
957
889
 
958
890
(def-vl-wildelim-list vl-portlist :element vl-port)
964
896
 
965
897
(def-vl-wildelim vl-portdecl
966
898
  :body (b* (((vl-portdecl x) x)
967
 
             (elem x)
968
 
             ((mv warnings range-prime) (vl-maybe-range-wildelim x.range elem warnings))
969
 
             (x-prime (change-vl-portdecl x :range range-prime)))
 
899
             (ctx x)
 
900
             ((mv warnings type-prime) (vl-datatype-wildelim x.type ctx warnings))
 
901
             (x-prime (change-vl-portdecl x :type type-prime)))
970
902
          (mv warnings x-prime)))
971
903
 
972
904
(def-vl-wildelim-list vl-portdecllist :element vl-portdecl)
973
905
 
974
 
(def-vl-wildelim vl-netdecl
975
 
  :body
976
 
  (b* (((vl-netdecl x) x)
977
 
       (elem x)
978
 
       ((mv warnings range-prime)   (vl-maybe-range-wildelim x.range elem warnings))
979
 
       ((mv warnings arrdims-prime) (vl-rangelist-wildelim x.arrdims elem warnings))
980
 
       ((mv warnings delay-prime)   (vl-maybe-gatedelay-wildelim x.delay elem warnings))
981
 
       (x-prime  (change-vl-netdecl x
982
 
                                    :range range-prime
983
 
                                    :arrdims arrdims-prime
984
 
                                    :delay delay-prime)))
985
 
    (mv warnings x-prime)))
986
 
 
987
 
(def-vl-wildelim-list vl-netdecllist :element vl-netdecl)
988
 
 
989
906
(def-vl-wildelim vl-vardecl
990
907
  :body
991
908
  (b* (((vl-vardecl x) x)
992
 
       (elem x)
993
 
       ((mv warnings vartype-prime) (vl-datatype-wildelim x.vartype elem warnings))
994
 
       ((mv warnings dims-prime)    (vl-packeddimensionlist-wildelim x.dims elem warnings))
995
 
       ((mv warnings initval-prime) (vl-maybe-expr-wildelim x.initval elem warnings))
 
909
       (ctx x)
 
910
       ((mv warnings type-prime)    (vl-datatype-wildelim x.type ctx warnings))
 
911
       ((mv warnings initval-prime) (vl-maybe-expr-wildelim x.initval ctx warnings))
 
912
       ((mv warnings delay-prime)   (vl-maybe-gatedelay-wildelim x.delay ctx warnings))
996
913
       (x-prime (change-vl-vardecl x
997
 
                                   :vartype vartype-prime
998
 
                                   :dims    dims-prime
999
 
                                   :initval initval-prime)))
 
914
                                   :type    type-prime
 
915
                                   :initval initval-prime
 
916
                                   :delay   delay-prime)))
1000
917
    (mv warnings x-prime)))
1001
918
 
1002
919
(def-vl-wildelim-list vl-vardecllist :element vl-vardecl)
1003
920
 
 
921
(def-vl-wildelim vl-paramtype
 
922
  :takes-ctx t
 
923
  :body
 
924
  (vl-paramtype-case x
 
925
    (:vl-implicitvalueparam
 
926
     (b* (((mv warnings range-prime)   (vl-maybe-range-wildelim x.range ctx warnings))
 
927
          ((mv warnings default-prime) (vl-maybe-expr-wildelim x.default ctx warnings))
 
928
          (x-prime                     (change-vl-implicitvalueparam x
 
929
                                                                     :range   range-prime
 
930
                                                                     :default default-prime)))
 
931
       (mv warnings x-prime)))
 
932
 
 
933
    (:vl-explicitvalueparam
 
934
     (b* (((mv warnings type-prime)    (vl-datatype-wildelim x.type ctx warnings))
 
935
          ((mv warnings default-prime) (vl-maybe-expr-wildelim x.default ctx warnings))
 
936
          (x-prime                     (change-vl-explicitvalueparam x
 
937
                                                                     :type    type-prime
 
938
                                                                      :default default-prime)))
 
939
       (mv warnings x-prime)))
 
940
 
 
941
    (:vl-typeparam
 
942
     (b* (((mv warnings default-prime) (vl-maybe-datatype-wildelim x.default ctx warnings))
 
943
          (x-prime                     (change-vl-typeparam x :default default-prime)))
 
944
       (mv warnings x-prime)))))
 
945
 
1004
946
(def-vl-wildelim vl-paramdecl
1005
947
  :body
1006
948
  (b* (((vl-paramdecl x) x)
1007
 
       (elem x)
1008
 
       ((mv warnings expr-prime)    (vl-expr-wildelim x.expr elem warnings))
1009
 
       ((mv warnings range-prime)   (vl-maybe-range-wildelim x.range elem warnings))
1010
 
       (x-prime (change-vl-paramdecl x
1011
 
                                     :expr  expr-prime
1012
 
                                     :range range-prime)))
 
949
       (ctx x)
 
950
       ((mv warnings type-prime)  (vl-paramtype-wildelim x.type ctx warnings))
 
951
       (x-prime                   (change-vl-paramdecl x :type type-prime)))
1013
952
    (mv warnings x-prime)))
1014
953
 
1015
954
(def-vl-wildelim-list vl-paramdecllist :element vl-paramdecl)
1024
963
(def-vl-wildelim-list vl-blockitemlist :element vl-blockitem)
1025
964
 
1026
965
(def-vl-wildelim vl-delaycontrol
1027
 
  :takes-elem t
 
966
  :takes-ctx t
1028
967
  :body (b* (((vl-delaycontrol x) x)
1029
 
             ((mv warnings value-prime) (vl-expr-wildelim x.value elem warnings))
 
968
             ((mv warnings value-prime) (vl-expr-wildelim x.value ctx warnings))
1030
969
             (x-prime (change-vl-delaycontrol x :value value-prime)))
1031
970
            (mv warnings x-prime)))
1032
971
 
1033
972
(def-vl-wildelim vl-evatom
1034
 
  :takes-elem t
 
973
  :takes-ctx t
1035
974
  :body (b* (((vl-evatom x) x)
1036
 
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr elem warnings))
 
975
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr ctx warnings))
1037
976
             (x-prime (change-vl-evatom x :expr expr-prime)))
1038
977
            (mv warnings x-prime)))
1039
978
 
1040
979
(def-vl-wildelim-list vl-evatomlist
1041
 
  :takes-elem t
 
980
  :takes-ctx t
1042
981
  :element vl-evatom)
1043
982
 
1044
983
(def-vl-wildelim vl-eventcontrol
1045
 
  :takes-elem t
 
984
  :takes-ctx t
1046
985
  :body (b* (((vl-eventcontrol x) x)
1047
 
             ((mv warnings atoms-prime) (vl-evatomlist-wildelim x.atoms elem warnings))
 
986
             ((mv warnings atoms-prime) (vl-evatomlist-wildelim x.atoms ctx warnings))
1048
987
             (x-prime (change-vl-eventcontrol x :atoms atoms-prime)))
1049
988
          (mv warnings x-prime)))
1050
989
 
1051
990
(def-vl-wildelim vl-repeateventcontrol
1052
 
  :takes-elem t
 
991
  :takes-ctx t
1053
992
  :body (b* (((vl-repeateventcontrol x) x)
1054
 
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr elem warnings))
1055
 
             ((mv warnings ctrl-prime) (vl-eventcontrol-wildelim x.ctrl elem warnings))
 
993
             ((mv warnings expr-prime) (vl-expr-wildelim x.expr ctx warnings))
 
994
             ((mv warnings ctrl-prime) (vl-eventcontrol-wildelim x.ctrl ctx warnings))
1056
995
             (x-prime (change-vl-repeateventcontrol x
1057
996
                                                    :expr expr-prime
1058
997
                                                    :ctrl ctrl-prime)))
1059
998
            (mv warnings x-prime)))
1060
999
 
1061
1000
(def-vl-wildelim vl-delayoreventcontrol
1062
 
  :takes-elem t
 
1001
  :takes-ctx t
1063
1002
  :body (case (tag x)
1064
 
          (:vl-delaycontrol (vl-delaycontrol-wildelim x elem warnings))
1065
 
          (:vl-eventcontrol (vl-eventcontrol-wildelim x elem warnings))
1066
 
          (otherwise        (vl-repeateventcontrol-wildelim x elem warnings))))
 
1003
          (:vl-delaycontrol (vl-delaycontrol-wildelim x ctx warnings))
 
1004
          (:vl-eventcontrol (vl-eventcontrol-wildelim x ctx warnings))
 
1005
          (otherwise        (vl-repeateventcontrol-wildelim x ctx warnings))))
1067
1006
 
1068
1007
(def-vl-wildelim vl-maybe-delayoreventcontrol
1069
 
  :takes-elem t
 
1008
  :takes-ctx t
1070
1009
  :inline t
1071
1010
  :body (if x
1072
 
            (vl-delayoreventcontrol-wildelim x elem warnings)
 
1011
            (vl-delayoreventcontrol-wildelim x ctx warnings)
1073
1012
          (mv warnings nil)))
1074
1013
 
1075
1014
(defthm vl-maybe-delayoreventcontrol-wildelim-under-iff
1076
 
  (iff (mv-nth 1 (vl-maybe-delayoreventcontrol-wildelim x elem warnings))
 
1015
  (iff (mv-nth 1 (vl-maybe-delayoreventcontrol-wildelim x ctx warnings))
1077
1016
       x)
1078
 
  :hints(("Goal" :in-theory (enable vl-maybe-delayoreventcontrol-wildelim))))
 
1017
  :hints(("Goal" :in-theory (enable (tau-system)
 
1018
                                    vl-maybe-delayoreventcontrol-wildelim))))
1079
1019
 
1080
1020
(defines vl-stmt-wildelim
1081
1021
 
1082
1022
  (define vl-stmt-wildelim
1083
1023
    ((x        vl-stmt-p)
1084
 
     (elem     vl-modelement-p)
 
1024
     (ctx      vl-context-p)
1085
1025
     (warnings vl-warninglist-p))
1086
1026
    :verify-guards nil
1087
1027
    :measure (vl-stmt-count x)
1088
1028
    :returns (mv (warnings vl-warninglist-p)
1089
1029
                 (new-x    vl-stmt-p))
1090
1030
    (b* ((x        (vl-stmt-fix x))
1091
 
         (elem     (vl-modelement-fix elem))
 
1031
         (ctx     (vl-context-fix ctx))
1092
1032
         (warnings (vl-warninglist-fix warnings))
1093
1033
 
1094
1034
         ((when (vl-atomicstmt-p x))
1097
1037
             (mv warnings x))
1098
1038
            (:vl-assignstmt
1099
1039
             (b* (((vl-assignstmt x) x)
1100
 
                  ((mv warnings lhs-prime) (vl-expr-wildelim x.lvalue elem warnings))
1101
 
                  ((mv warnings rhs-prime) (vl-expr-wildelim x.expr elem warnings))
1102
 
                  ((mv warnings ctrl-prime) (vl-maybe-delayoreventcontrol-wildelim x.ctrl elem warnings))
 
1040
                  ((mv warnings lhs-prime) (vl-expr-wildelim x.lvalue ctx warnings))
 
1041
                  ((mv warnings rhs-prime) (vl-expr-wildelim x.expr ctx warnings))
 
1042
                  ((mv warnings ctrl-prime) (vl-maybe-delayoreventcontrol-wildelim x.ctrl ctx warnings))
1103
1043
                  (x-prime (change-vl-assignstmt x
1104
1044
                                                 :lvalue lhs-prime
1105
1045
                                                 :expr rhs-prime
1107
1047
               (mv warnings x-prime)))
1108
1048
            (:vl-deassignstmt
1109
1049
             (b* (((vl-deassignstmt x) x)
1110
 
                  ((mv warnings lvalue-prime) (vl-expr-wildelim x.lvalue elem warnings))
 
1050
                  ((mv warnings lvalue-prime) (vl-expr-wildelim x.lvalue ctx warnings))
1111
1051
                  (x-prime (change-vl-deassignstmt x :lvalue lvalue-prime)))
1112
1052
               (mv warnings x-prime)))
1113
1053
            (:vl-enablestmt
1114
1054
             (b* (((vl-enablestmt x) x)
1115
 
                  ((mv warnings id-prime)   (vl-expr-wildelim x.id elem warnings))
1116
 
                  ((mv warnings args-prime) (vl-exprlist-wildelim x.args elem warnings))
 
1055
                  ((mv warnings id-prime)   (vl-expr-wildelim x.id ctx warnings))
 
1056
                  ((mv warnings args-prime) (vl-exprlist-wildelim x.args ctx warnings))
1117
1057
                  (x-prime (change-vl-enablestmt x
1118
1058
                                                 :id id-prime
1119
1059
                                                 :args args-prime)))
1120
1060
               (mv warnings x-prime)))
1121
1061
            (:vl-disablestmt
1122
1062
             (b* (((vl-disablestmt x) x)
1123
 
                  ((mv warnings id-prime) (vl-expr-wildelim x.id elem warnings))
 
1063
                  ((mv warnings id-prime) (vl-expr-wildelim x.id ctx warnings))
1124
1064
                  (x-prime (change-vl-disablestmt x :id id-prime)))
1125
1065
               (mv warnings x-prime)))
1126
1066
            (otherwise
1127
1067
             (b* (((vl-eventtriggerstmt x) x)
1128
 
                  ((mv warnings id-prime) (vl-expr-wildelim x.id elem warnings))
 
1068
                  ((mv warnings id-prime) (vl-expr-wildelim x.id ctx warnings))
1129
1069
                  (x-prime (change-vl-eventtriggerstmt x :id id-prime)))
1130
1070
               (mv warnings x-prime)))))
1131
1071
 
1133
1073
         (x.stmts (vl-compoundstmt->stmts x))
1134
1074
         (x.ctrl  (vl-compoundstmt->ctrl x))
1135
1075
         (x.decls (vl-compoundstmt->decls x))
1136
 
         ((mv warnings exprs-prime) (vl-exprlist-wildelim x.exprs elem warnings))
1137
 
         ((mv warnings stmts-prime) (vl-stmtlist-wildelim x.stmts elem warnings))
1138
 
         ((mv warnings ctrl-prime)  (vl-maybe-delayoreventcontrol-wildelim x.ctrl elem warnings))
 
1076
         ((mv warnings exprs-prime) (vl-exprlist-wildelim x.exprs ctx warnings))
 
1077
         ((mv warnings stmts-prime) (vl-stmtlist-wildelim x.stmts ctx warnings))
 
1078
         ((mv warnings ctrl-prime)  (vl-maybe-delayoreventcontrol-wildelim x.ctrl ctx warnings))
1139
1079
         ((mv warnings decls-prime) (vl-blockitemlist-wildelim x.decls warnings))
1140
1080
         (x-prime (change-vl-compoundstmt x
1141
1081
                                          :exprs exprs-prime
1146
1086
 
1147
1087
  (define vl-stmtlist-wildelim
1148
1088
    ((x        vl-stmtlist-p)
1149
 
     (elem     vl-modelement-p)
 
1089
     (ctx      vl-context-p)
1150
1090
     (warnings vl-warninglist-p))
1151
1091
    :measure (vl-stmtlist-count x)
1152
1092
    :returns (mv (warnings vl-warninglist-p)
1154
1094
                                (equal (len new-x) (len x)))))
1155
1095
    (b* (((when (atom x))
1156
1096
          (mv (ok) nil))
1157
 
         ((mv warnings car-prime) (vl-stmt-wildelim (car x) elem warnings))
1158
 
         ((mv warnings cdr-prime) (vl-stmtlist-wildelim (cdr x) elem warnings)))
 
1097
         ((mv warnings car-prime) (vl-stmt-wildelim (car x) ctx warnings))
 
1098
         ((mv warnings cdr-prime) (vl-stmtlist-wildelim (cdr x) ctx warnings)))
1159
1099
      (mv warnings (cons car-prime cdr-prime))))
1160
1100
  ///
1161
1101
  (verify-guards vl-stmt-wildelim)
1163
1103
 
1164
1104
(def-vl-wildelim vl-always
1165
1105
  :body (b* (((vl-always x) x)
1166
 
             (elem x)
1167
 
             ((mv warnings stmt-prime) (vl-stmt-wildelim x.stmt elem warnings))
 
1106
             (ctx x)
 
1107
             ((mv warnings stmt-prime) (vl-stmt-wildelim x.stmt ctx warnings))
1168
1108
             (x-prime (change-vl-always x :stmt stmt-prime)))
1169
1109
            (mv warnings x-prime)))
1170
1110
 
1173
1113
 
1174
1114
(def-vl-wildelim vl-initial
1175
1115
  :body (b* (((vl-initial x) x)
1176
 
             (elem x)
 
1116
             (ctx x)
1177
1117
             ((mv warnings stmt-prime)
1178
 
              (vl-stmt-wildelim x.stmt elem warnings))
 
1118
              (vl-stmt-wildelim x.stmt ctx warnings))
1179
1119
             (x-prime (change-vl-initial x :stmt stmt-prime)))
1180
1120
            (mv warnings x-prime)))
1181
1121
 
1182
1122
(def-vl-wildelim-list vl-initiallist :element vl-initial)
1183
1123
 
 
1124
(def-genblob-transform vl-genblob-wildelim ((warnings vl-warninglist-p))
 
1125
  :returns ((warnings vl-warninglist-p))
 
1126
  ;; :verify-guards nil
 
1127
  (b* (((vl-genblob x) x)
 
1128
 
 
1129
       ((mv warnings assigns)    (vl-assignlist-wildelim    x.assigns    warnings))
 
1130
       ((mv warnings modinsts)   (vl-modinstlist-wildelim   x.modinsts   warnings))
 
1131
       ((mv warnings gateinsts)  (vl-gateinstlist-wildelim  x.gateinsts  warnings))
 
1132
       ((mv warnings alwayses)   (vl-alwayslist-wildelim    x.alwayses   warnings))
 
1133
       ((mv warnings initials)   (vl-initiallist-wildelim   x.initials   warnings))
 
1134
       ((mv warnings portdecls)  (vl-portdecllist-wildelim  x.portdecls  warnings))
 
1135
       ((mv warnings paramdecls) (vl-paramdecllist-wildelim x.paramdecls warnings))
 
1136
       ((mv warnings vardecls)   (vl-vardecllist-wildelim   x.vardecls   warnings))
 
1137
 
 
1138
       ((mv warnings generates)  (vl-generates-wildelim     x.generates  warnings))
 
1139
       ((mv warnings ports)      (vl-portlist-wildelim      x.ports      warnings)))
 
1140
 
 
1141
    (mv warnings
 
1142
        (change-vl-genblob
 
1143
         x
 
1144
         :ports ports
 
1145
         :assigns assigns
 
1146
         :modinsts modinsts
 
1147
         :gateinsts gateinsts
 
1148
         :alwayses alwayses
 
1149
         :initials initials
 
1150
         :portdecls portdecls
 
1151
         :paramdecls paramdecls
 
1152
         :vardecls vardecls
 
1153
         :generates generates)))
 
1154
  :apply-to-generates vl-generates-wildelim)
 
1155
 
1184
1156
 
1185
1157
 
1186
1158
(define vl-module-wildelim ((x vl-module-p))
1190
1162
        x)
1191
1163
       ((vl-module x) x)
1192
1164
       (warnings  x.warnings)
1193
 
       ((mv warnings assigns)    (vl-assignlist-wildelim    x.assigns    warnings))
1194
 
       ((mv warnings modinsts)   (vl-modinstlist-wildelim   x.modinsts   warnings))
1195
 
       ((mv warnings gateinsts)  (vl-gateinstlist-wildelim  x.gateinsts  warnings))
1196
 
       ((mv warnings alwayses)   (vl-alwayslist-wildelim    x.alwayses   warnings))
1197
 
       ((mv warnings initials)   (vl-initiallist-wildelim   x.initials   warnings))
1198
 
       ((mv warnings ports)      (vl-portlist-wildelim      x.ports      warnings))
1199
 
       ((mv warnings portdecls)  (vl-portdecllist-wildelim  x.portdecls  warnings))
1200
 
       ((mv warnings paramdecls) (vl-paramdecllist-wildelim x.paramdecls warnings))
1201
 
       ((mv warnings netdecls)   (vl-netdecllist-wildelim   x.netdecls   warnings))
1202
 
       ((mv warnings vardecls)   (vl-vardecllist-wildelim   x.vardecls   warnings)))
1203
 
    (change-vl-module x
1204
 
                      :assigns assigns
1205
 
                      :modinsts modinsts
1206
 
                      :gateinsts gateinsts
1207
 
                      :alwayses alwayses
1208
 
                      :initials initials
1209
 
                      :ports ports
1210
 
                      :portdecls portdecls
1211
 
                      :paramdecls paramdecls
1212
 
                      :netdecls netdecls
1213
 
                      :vardecls vardecls
1214
 
                      :warnings warnings)))
 
1165
       (genblob (vl-module->genblob x))
 
1166
       ((mv warnings new-genblob)
 
1167
        (vl-genblob-wildelim genblob warnings))
 
1168
       (mod (change-vl-module x :warnings warnings)))
 
1169
    (vl-genblob->module new-genblob mod)))
1215
1170
 
1216
1171
(defprojection vl-modulelist-wildelim ((x vl-modulelist-p))
1217
1172
  :returns (new-x vl-modulelist-p)