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

« back to all changes in this revision

Viewing changes to books/centaur/vl/transforms/occform/select.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:
67
67
 
68
68
  (b* ((name (hons-copy "VL_1_BIT_DYNAMIC_BITSELECT"))
69
69
 
70
 
       ((mv out-expr out-port out-portdecl out-netdecl) (vl-primitive-mkport "out" :vl-output))
71
 
       ((mv in-expr in-port in-portdecl in-netdecl)     (vl-primitive-mkport "in"  :vl-input))
72
 
       ((mv idx-expr idx-port idx-portdecl idx-netdecl) (vl-primitive-mkport "idx" :vl-input))
 
70
       ((mv out-expr out-port out-portdecl out-vardecl) (vl-primitive-mkport "out" :vl-output))
 
71
       ((mv in-expr in-port in-portdecl in-vardecl)     (vl-primitive-mkport "in"  :vl-input))
 
72
       ((mv idx-expr idx-port idx-portdecl idx-vardecl) (vl-primitive-mkport "idx" :vl-input))
73
73
 
74
 
       ((mv ~idx-expr ~idx-netdecl) (vl-primitive-mkwire "idx_bar"))
75
 
       ((mv a-expr a-netdecl)       (vl-primitive-mkwire "a"))
76
 
       ((mv b-expr b-netdecl)       (vl-primitive-mkwire "b"))
 
74
       ((mv ~idx-expr ~idx-vardecl) (vl-primitive-mkwire "idx_bar"))
 
75
       ((mv a-expr a-vardecl)       (vl-primitive-mkwire "a"))
 
76
       ((mv b-expr b-vardecl)       (vl-primitive-mkwire "b"))
77
77
 
78
78
       (~idx-inst (vl-simple-inst *vl-1-bit-not* "mk_idx_bar" ~idx-expr idx-expr))
79
79
       (a-inst    (vl-simple-inst *vl-1-bit-and* "mk_a"       a-expr    ~idx-expr in-expr))
85
85
                     :origname  name
86
86
                     :ports     (list out-port in-port idx-port)
87
87
                     :portdecls (list out-portdecl in-portdecl idx-portdecl)
88
 
                     :netdecls  (list out-netdecl in-netdecl idx-netdecl ~idx-netdecl a-netdecl b-netdecl)
 
88
                     :vardecls  (list out-vardecl in-vardecl idx-vardecl ~idx-vardecl a-vardecl b-vardecl)
89
89
                     :modinsts  (list ~idx-inst a-inst b-inst out-inst)
90
90
                     :minloc    *vl-fakeloc*
91
91
                     :maxloc    *vl-fakeloc*))))
141
141
 
142
142
  (b* ((name (hons-copy "VL_2_BIT_DYNAMIC_BITSELECT"))
143
143
 
144
 
       ((mv out-expr out-port out-portdecl out-netdecl) (vl-primitive-mkport "out" :vl-output))
145
 
       ((mv in-expr in-port in-portdecl in-netdecl)     (vl-occform-mkport   "in"  :vl-input 2))
146
 
       ((mv idx-expr idx-port idx-portdecl idx-netdecl) (vl-primitive-mkport "idx" :vl-input))
 
144
       ((mv out-expr out-port out-portdecl out-vardecl) (vl-primitive-mkport "out" :vl-output))
 
145
       ((mv in-expr in-port in-portdecl in-vardecl)     (vl-occform-mkport   "in"  :vl-input 2))
 
146
       ((mv idx-expr idx-port idx-portdecl idx-vardecl) (vl-primitive-mkport "idx" :vl-input))
147
147
 
148
 
       ((mv ~idx-expr ~idx-netdecl)   (vl-primitive-mkwire "idx_bar"))
149
 
       ((mv idx_x-expr idx_x-netdecl) (vl-primitive-mkwire "idx_x"))
150
 
       ((mv a-expr a-netdecl)         (vl-primitive-mkwire "a"))
151
 
       ((mv b-expr b-netdecl)         (vl-primitive-mkwire "b"))
152
 
       ((mv main-expr main-netdecl)   (vl-primitive-mkwire "main"))
 
148
       ((mv ~idx-expr ~idx-vardecl)   (vl-primitive-mkwire "idx_bar"))
 
149
       ((mv idx_x-expr idx_x-vardecl) (vl-primitive-mkwire "idx_x"))
 
150
       ((mv a-expr a-vardecl)         (vl-primitive-mkwire "a"))
 
151
       ((mv b-expr b-vardecl)         (vl-primitive-mkwire "b"))
 
152
       ((mv main-expr main-vardecl)   (vl-primitive-mkwire "main"))
153
153
 
154
154
       (in[0]-expr  (vl-make-bitselect in-expr 0))
155
155
       (in[1]-expr  (vl-make-bitselect in-expr 1))
172
172
                     :origname  name
173
173
                     :ports     (list out-port in-port idx-port)
174
174
                     :portdecls (list out-portdecl in-portdecl idx-portdecl)
175
 
                     :netdecls  (list out-netdecl in-netdecl idx-netdecl
176
 
                                      ~idx-netdecl a-netdecl b-netdecl main-netdecl
177
 
                                      idx_x-netdecl)
 
175
                     :vardecls  (list out-vardecl in-vardecl idx-vardecl
 
176
                                      ~idx-vardecl a-vardecl b-vardecl main-vardecl
 
177
                                      idx_x-vardecl)
178
178
                     :modinsts (list ~idx-inst a-inst b-inst main-inst idx_x-inst out-inst)
179
179
                     :minloc    *vl-fakeloc*
180
180
                     :maxloc    *vl-fakeloc*))))
243
243
       (submods (vl-make-2^n-bit-dynamic-bitselect (- n 1)))
244
244
       (name (hons-copy (cat "VL_" (natstr m) "_BIT_DYNAMIC_BITSELECT")))
245
245
 
246
 
       ((mv out-expr out-port out-portdecl out-netdecl) (vl-primitive-mkport "out" :vl-output))
247
 
       ((mv in-expr in-port in-portdecl in-netdecl)     (vl-occform-mkport "in" :vl-input m))
248
 
       ((mv idx-expr idx-port idx-portdecl idx-netdecl) (vl-occform-mkport "idx" :vl-input n))
 
246
       ((mv out-expr out-port out-portdecl out-vardecl) (vl-primitive-mkport "out" :vl-output))
 
247
       ((mv in-expr in-port in-portdecl in-vardecl)     (vl-occform-mkport "in" :vl-input m))
 
248
       ((mv idx-expr idx-port idx-portdecl idx-vardecl) (vl-occform-mkport "idx" :vl-input n))
249
249
 
250
 
       ((mv high-expr high-netdecl)   (vl-primitive-mkwire "high"))
251
 
       ((mv low-expr low-netdecl)     (vl-primitive-mkwire "low"))
252
 
       ((mv ~idx-expr ~idx-netdecl)   (vl-primitive-mkwire "idx_bar"))
253
 
       ((mv a-expr a-netdecl)         (vl-primitive-mkwire "a"))
254
 
       ((mv b-expr b-netdecl)         (vl-primitive-mkwire "b"))
255
 
       ((mv main-expr main-netdecl)   (vl-primitive-mkwire "main"))
256
 
       ((mv idx_x-expr idx_x-netdecl) (vl-primitive-mkwire "idx_x"))
 
250
       ((mv high-expr high-vardecl)   (vl-primitive-mkwire "high"))
 
251
       ((mv low-expr low-vardecl)     (vl-primitive-mkwire "low"))
 
252
       ((mv ~idx-expr ~idx-vardecl)   (vl-primitive-mkwire "idx_bar"))
 
253
       ((mv a-expr a-vardecl)         (vl-primitive-mkwire "a"))
 
254
       ((mv b-expr b-vardecl)         (vl-primitive-mkwire "b"))
 
255
       ((mv main-expr main-vardecl)   (vl-primitive-mkwire "main"))
 
256
       ((mv idx_x-expr idx_x-vardecl) (vl-primitive-mkwire "idx_x"))
257
257
 
258
258
       (|in[m-1]:k|  (vl-make-partselect in-expr (- m 1) k))
259
259
       (|in[k-1:0]|  (vl-make-partselect in-expr (- k 1) 0))
283
283
                           :origname  name
284
284
                           :ports     (list out-port in-port idx-port)
285
285
                           :portdecls (list out-portdecl in-portdecl idx-portdecl)
286
 
                           :netdecls  (list out-netdecl in-netdecl idx-netdecl high-netdecl low-netdecl
287
 
                                            ~idx-netdecl a-netdecl b-netdecl main-netdecl idx_x-netdecl)
 
286
                           :vardecls  (list out-vardecl in-vardecl idx-vardecl high-vardecl low-vardecl
 
287
                                            ~idx-vardecl a-vardecl b-vardecl main-vardecl idx_x-vardecl)
288
288
                           :modinsts  (list high-inst low-inst ~idx-inst a-inst b-inst main-inst idx_x-inst out-inst)
289
289
                           :minloc    *vl-fakeloc*
290
290
                           :maxloc    *vl-fakeloc*)
352
352
 
353
353
       (name (hons-copy (cat "VL_" (natstr n) "_BIT_DYNAMIC_BITSELECT")))
354
354
 
355
 
       ((mv out-expr out-port out-portdecl out-netdecl) (vl-primitive-mkport "out" :vl-output))
356
 
       ((mv in-expr in-port in-portdecl in-netdecl)     (vl-occform-mkport "in" :vl-input n))
357
 
       ((mv idx-expr idx-port idx-portdecl idx-netdecl) (vl-occform-mkport "idx" :vl-input bitlength))
 
355
       ((mv out-expr out-port out-portdecl out-vardecl) (vl-primitive-mkport "out" :vl-output))
 
356
       ((mv in-expr in-port in-portdecl in-vardecl)     (vl-occform-mkport "in" :vl-input n))
 
357
       ((mv idx-expr idx-port idx-portdecl idx-vardecl) (vl-occform-mkport "idx" :vl-input bitlength))
358
358
 
359
359
       ;; pad-expr = { (2^bitlen-n)'bxxx...xxx, in }
360
360
       (padlen        (- 2^bitlength n))
373
373
                          :origname  name
374
374
                          :ports     (list out-port in-port idx-port)
375
375
                          :portdecls (list out-portdecl in-portdecl idx-portdecl)
376
 
                          :netdecls  (list out-netdecl in-netdecl idx-netdecl)
 
376
                          :vardecls  (list out-vardecl in-vardecl idx-vardecl)
377
377
                          :modinsts  (list inst)
378
378
                          :minloc    *vl-fakeloc*
379
379
                          :maxloc    *vl-fakeloc*)
423
423
                ((unless idx) ;; Should never happen
424
424
                 (raise "coremod has no index port?")
425
425
                 m)
426
 
                (range    (vl-portdecl->range idx))
 
426
                (type    (vl-portdecl->type idx))
 
427
                ((unless (eq (vl-datatype-kind type) :vl-coretype))
 
428
                 (raise "coremod port isn't a coretype?")
 
429
                 m)
 
430
                ((vl-coretype type))
 
431
                ((unless (and (atom type.udims)
 
432
                              (or (atom type.pdims)
 
433
                                  (and (atom (cdr type.pdims))
 
434
                                       (not (eq (car type.pdims) :vl-unsized-dimension))))))
 
435
                 (raise "coremod index unexpected array dims")
 
436
                 m)
 
437
                (range   (and (consp type.pdims) (car type.pdims)))
427
438
                ((unless (vl-maybe-range-resolved-p range)) ;; Should never happen
428
439
                 (raise "coremod index range not resolved?")
429
440
                 m))
437
448
        ;; Else, we need a new module.
438
449
        (name (cat "VL_" (natstr n) "_BIT_DYNAMIC_BITSELECT_" (natstr m)))
439
450
 
440
 
        ((mv out-expr out-port out-portdecl out-netdecl) (vl-primitive-mkport "out" :vl-output))
441
 
        ((mv in-expr in-port in-portdecl in-netdecl)     (vl-occform-mkport "in" :vl-input n))
442
 
        ((mv idx-expr idx-port idx-portdecl idx-netdecl) (vl-occform-mkport "idx" :vl-input m))
 
451
        ((mv out-expr out-port out-portdecl out-vardecl) (vl-primitive-mkport "out" :vl-output))
 
452
        ((mv in-expr in-port in-portdecl in-vardecl)     (vl-occform-mkport "in" :vl-input n))
 
453
        ((mv idx-expr idx-port idx-portdecl idx-vardecl) (vl-occform-mkport "idx" :vl-input m))
443
454
 
444
455
        ((when (< k m))
445
456
         ;; Case 1.  Our idx port is larger than the idx port on the core
451
462
 
452
463
              ;; wire main = in[lowbits];
453
464
              ;; VL_N_BIT_DYNAMIC_BITSELECT core (main, in, lowbits);
454
 
              ((mv main-expr main-netdecl) (vl-primitive-mkwire "main"))
 
465
              ((mv main-expr main-vardecl) (vl-primitive-mkwire "main"))
455
466
              (core-inst (vl-simple-inst (car coremods) "core" main-expr in-expr lowbits))
456
467
 
457
468
              ;; wire any_extra = |highbits;
458
469
              ((cons extra-mod extra-support) (vl-make-n-bit-reduction-op :vl-unary-bitor (- m k)))
459
 
              ((mv extra-expr extra-netdecl)  (vl-primitive-mkwire "any_extra"))
 
470
              ((mv extra-expr extra-vardecl)  (vl-primitive-mkwire "any_extra"))
460
471
              (extra-inst (vl-simple-inst extra-mod "mk_any_extra" extra-expr highbits))
461
472
 
462
473
              ;; this is effectively out = any_extra ? 1'bx : main;
466
477
              ;; and(a, no_extra, main);
467
478
              ;; and(b, any_extra, 1'bx);
468
479
              ;; or(out, a, b);
469
 
              ((mv noextra-expr noextra-netdecl) (vl-primitive-mkwire "no_extra"))
470
 
              ((mv a-expr a-netdecl)             (vl-primitive-mkwire "a"))
471
 
              ((mv b-expr b-netdecl)             (vl-primitive-mkwire "b"))
 
480
              ((mv noextra-expr noextra-vardecl) (vl-primitive-mkwire "no_extra"))
 
481
              ((mv a-expr a-vardecl)             (vl-primitive-mkwire "a"))
 
482
              ((mv b-expr b-vardecl)             (vl-primitive-mkwire "b"))
472
483
              (noextra-inst (vl-simple-inst *vl-1-bit-not* "mk_no_extra" noextra-expr extra-expr))
473
484
              (a-inst       (vl-simple-inst *vl-1-bit-and* "mk_a"        a-expr       noextra-expr main-expr))
474
485
              (b-inst       (vl-simple-inst *vl-1-bit-and* "mk_b"        b-expr       extra-expr   |*sized-1'bx*|))
478
489
                                   :origname  name
479
490
                                   :ports     (list out-port in-port idx-port)
480
491
                                   :portdecls (list out-portdecl in-portdecl idx-portdecl)
481
 
                                   :netdecls  (list out-netdecl in-netdecl idx-netdecl main-netdecl extra-netdecl
482
 
                                                    noextra-netdecl a-netdecl b-netdecl)
 
492
                                   :vardecls  (list out-vardecl in-vardecl idx-vardecl main-vardecl extra-vardecl
 
493
                                                    noextra-vardecl a-vardecl b-vardecl)
483
494
                                   :modinsts  (list core-inst extra-inst noextra-inst a-inst b-inst out-inst)
484
495
                                   :minloc    *vl-fakeloc*
485
496
                                   :maxloc    *vl-fakeloc*)))
503
514
                           :origname  name
504
515
                           :ports     (list out-port in-port idx-port)
505
516
                           :portdecls (list out-portdecl in-portdecl idx-portdecl)
506
 
                           :netdecls  (list out-netdecl in-netdecl idx-netdecl)
 
517
                           :vardecls  (list out-vardecl in-vardecl idx-vardecl)
507
518
                           :modinsts  (list core-inst)
508
519
                           :minloc    *vl-fakeloc*
509
520
                           :maxloc    *vl-fakeloc*)