← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/transforms/always/nedgeflop.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/always/nedgeflop.lisp
83
83
  :returns (mv (exprs     vl-exprlist-p :hyp :fguard)
84
84
               (ports     vl-portlist-p :hyp :fguard)
85
85
               (portdecls vl-portdecllist-p :hyp :fguard)
86
 
               (netdecls  vl-netdecllist-p :hyp :fguard))
 
86
               (vardecls  vl-vardecllist-p :hyp :fguard))
87
87
  :short "Helper function for creating lists of primitive port declarations."
88
88
  :measure (nfix (- (nfix n) (nfix i)))
89
89
  (b* (((when (mbe :logic (zp (- (lnfix n) (lnfix i)))
90
90
                   :exec (eql i n)))
91
91
        (mv nil nil nil nil))
92
92
       (name1 (hons-copy (cat prefix (natstr i))))
93
 
       ((mv expr1 port1 portdecl1 netdecl1)
 
93
       ((mv expr1 port1 portdecl1 vardecl1)
94
94
        (vl-primitive-mkport name1 dir))
95
 
       ((mv exprs2 ports2 portdecls2 netdecls2)
 
95
       ((mv exprs2 ports2 portdecls2 vardecls2)
96
96
        (vl-primitive-mkports prefix (+ 1 (lnfix i)) n
97
97
                              :dir dir :loc loc)))
98
98
    (mv (cons expr1 exprs2)
99
99
        (cons port1 ports2)
100
100
        (cons portdecl1 portdecls2)
101
 
        (cons netdecl1 netdecls2)))
 
101
        (cons vardecl1 vardecls2)))
102
102
  ///
103
103
  (defmvtypes vl-primitive-mkports-fn
104
104
    (true-listp true-listp true-listp true-listp))
105
105
 
106
106
  (defthm len-of-vl-primitive-mkports
107
 
    (b* (((mv exprs ports portdecls netdecls)
 
107
    (b* (((mv exprs ports portdecls vardecls)
108
108
          (vl-primitive-mkports prefix i n
109
109
                                :dir dir
110
110
                                :loc loc))
112
112
      (and (equal (len exprs) len)
113
113
           (equal (len ports) len)
114
114
           (equal (len portdecls) len)
115
 
           (equal (len netdecls) len))))
 
115
           (equal (len vardecls) len))))
116
116
 
117
117
  (defthm vl-primitive-mkports-under-iff
118
 
    (b* (((mv exprs ports portdecls netdecls)
 
118
    (b* (((mv exprs ports portdecls vardecls)
119
119
          (vl-primitive-mkports prefix i n
120
120
                                :dir dir
121
121
                                :loc loc))
123
123
      (and (iff exprs     (posp len))
124
124
           (iff ports     (posp len))
125
125
           (iff portdecls (posp len))
126
 
           (iff netdecls  (posp len))))))
 
126
           (iff vardecls  (posp len))))))
127
127
 
128
128
(define vl-nedgeflop-posedge-clks
129
129
  :short "Build the Verilog sensitivity list for a primitive n-edge flop."
279
279
  (b* ((name (cat "VL_1_BIT_" (natstr n) "_EDGE_FLOP"))
280
280
 
281
281
       ;; output q;
282
 
       ((mv q-expr q-port q-portdecl ?q-netdecl)
 
282
       ((mv q-expr q-port q-portdecl q-vardecl)
283
283
        (vl-primitive-mkport "q" :vl-output))
284
284
 
285
285
       ;; reg q;
286
 
       (q-vardecl (make-vl-vardecl :vartype (make-vl-coretype :name :vl-reg)
287
 
                                   :name "q"
288
 
                                   :loc *vl-fakeloc*))
 
286
       (q-portdecl (change-vl-portdecl q-portdecl :type *vl-plain-old-reg-type*))
 
287
       (q-vardecl  (change-vl-vardecl  q-vardecl  :type *vl-plain-old-reg-type*))
289
288
 
290
289
       ;; input d0, d1, ..., d{n-1};
291
 
       ((mv d-exprs d-ports d-portdecls d-netdecls)
 
290
       ((mv d-exprs d-ports d-portdecls d-vardecls)
292
291
        (vl-primitive-mkports "d" 0 n :dir :vl-input))
293
292
 
294
293
       ;; input clk0, clk1, ..., clk{n-1};
295
 
       ((mv clk-exprs clk-ports clk-portdecls clk-netdecls)
 
294
       ((mv clk-exprs clk-ports clk-portdecls clk-vardecls)
296
295
        (vl-primitive-mkports "clk" 0 n :dir :vl-input))
297
296
       ;; always @(posedge clk0 or posedge clk1 or ...)
298
297
       ;;   if (clk0) q <= d0;
305
304
                  :origname  name
306
305
                  :ports     (cons q-port (append d-ports clk-ports))
307
306
                  :portdecls (cons q-portdecl (append d-portdecls clk-portdecls))
308
 
                  :netdecls  (append d-netdecls clk-netdecls)
309
 
                  :vardecls  (list q-vardecl)
 
307
                  :vardecls  (cons q-vardecl (append d-vardecls clk-vardecls))
310
308
                  :alwayses  (list always)
311
309
                  :minloc    *vl-fakeloc*
312
310
                  :maxloc    *vl-fakeloc*
380
378
 
381
379
||#
382
380
 
 
381
 
 
382
 
383
383
(defprojection vl-make-same-bitselect-from-each (x index)
384
384
  (vl-make-bitselect x index)
385
385
  :guard (and (vl-exprlist-p x)
388
388
  (defthm vl-exprlist-p-of-vl-make-same-bitselect-from-each
389
389
    (implies (force (vl-exprlist-p x))
390
390
             (vl-exprlist-p (vl-make-same-bitselect-from-each x index))))
 
391
  (local (in-theory (enable repeat)))
391
392
  (defthm vl-exprlist->finalwidths-of-vl-make-same-bitselect-from-each
392
393
    (equal (vl-exprlist->finalwidths (vl-make-same-bitselect-from-each x index))
393
394
           (replicate (len x) 1)))
427
428
       (name (cat "VL_" (natstr width) "_BIT_" (natstr nedges) "_EDGE_FLOP"))
428
429
 
429
430
       ;; output [width-1:0] q;
430
 
       ((mv q-expr q-port q-portdecl ?q-netdecl)
 
431
       ((mv q-expr q-port q-portdecl q-vardecl)
431
432
        (vl-occform-mkport "q" :vl-output width))
432
433
 
433
434
       ;; Note: no reg declaration for q, because the actual regs will live in
434
435
       ;; the submodule instances.
435
436
 
436
437
       ;; input [width-1:0] d0, d1, ..., d{n-1};
437
 
       ((mv d-exprs d-ports d-portdecls d-netdecls)
 
438
       ((mv d-exprs d-ports d-portdecls d-vardecls)
438
439
        (vl-occform-mkports "d" 0 nedges :dir :vl-input :width width))
439
440
 
440
441
       ;; input clk0, clk1, ..., clk{n-1};
441
 
       ((mv clk-exprs clk-ports clk-portdecls clk-netdecls)
 
442
       ((mv clk-exprs clk-ports clk-portdecls clk-vardecls)
442
443
        (vl-occform-mkports "clk" 0 nedges :dir :vl-input :width 1))
443
444
 
444
445
       (primitive (vl-make-1-bit-n-edge-flop nedges))
449
450
           :origname  name
450
451
           :ports     (cons q-port (append d-ports clk-ports))
451
452
           :portdecls (cons q-portdecl (append d-portdecls clk-portdecls))
452
 
           :netdecls  (cons q-netdecl (append d-netdecls clk-netdecls))
 
453
           :vardecls  (cons q-vardecl (append d-vardecls clk-vardecls))
453
454
           :modinsts  modinsts
454
455
           :minloc    *vl-fakeloc*
455
456
           :maxloc    *vl-fakeloc*)
625
626
                 (cat "VL_" (natstr width) "_BIT_" (natstr nedges) "_EDGE_FLOP")
626
627
               (cat "VL_" (natstr width) "_BIT_" (natstr nedges) "_EDGE_" (natstr delay) "_TICK_FLOP")))
627
628
 
628
 
       ((mv qexpr qport qportdecl qnetdecl) (vl-occform-mkport "q" :vl-output width))
629
 
       ((mv dexprs dports dportdecls dnetdecls) (vl-occform-mkports "d" 0 nedges :dir :vl-input :width width))
630
 
       ((mv clkexprs clkports clkportdecls clknetdecls) (vl-occform-mkports "clk" 0 nedges :dir :vl-input :width 1))
 
629
       ((mv qexpr qport qportdecl qvardecl) (vl-occform-mkport "q" :vl-output width))
 
630
       ((mv dexprs dports dportdecls dvardecls) (vl-occform-mkports "d" 0 nedges :dir :vl-input :width width))
 
631
       ((mv clkexprs clkports clkportdecls clkvardecls) (vl-occform-mkports "clk" 0 nedges :dir :vl-input :width 1))
631
632
 
632
633
       ;; note qregdecls are netdecls not regdecls
633
634
       ((mv qregexpr qregdecls qregassigns)
694
695
                            :origname name
695
696
                            :ports (cons qport (append dports clkports))
696
697
                            :portdecls (cons qportdecl (append dportdecls clkportdecls))
697
 
                            :netdecls `(,qnetdecl
698
 
                                        ,@dnetdecls
699
 
                                        ,@clknetdecls
 
698
                            :vardecls `(,qvardecl
 
699
                                        ,@dvardecls
 
700
                                        ,@clkvardecls
700
701
                                        ,@clkdeldecls
701
702
                                        ,@ddeldecls
702
703
                                        ,@qregdecls