← 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/combinational.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/combinational.lisp
573
573
        (mv nil (ok)))
574
574
 
575
575
       (lvalues (mergesort (vl-idexprlist->names (vl-stmt-cblock-lvalexprs body))))
576
 
       ((unless (vl-cblock-pathcheck lvalues body))
577
 
        ;; Some reg doesn't get updated in some path, not a combinational
578
 
        ;; block, maybe a latch or something.
 
576
       (paths-okp (vl-cblock-pathcheck lvalues body))
 
577
 
 
578
       ((when (and (not paths-okp)
 
579
                   (not (eq type :vl-always-comb))))
 
580
        ;; Some reg doesn't get updated in some path, and we don't know for
 
581
        ;; sure that this is supposed to be a combinational block.  This
 
582
        ;; might be a latch.  It's not our job to synthesize it.  Just fail,
 
583
        ;; no error, no warning.  BOZO for better debugging it might be good
 
584
        ;; to have a warning here anyway...
579
585
        (mv nil (ok)))
580
586
 
 
587
       (warnings
 
588
        (if (and (not paths-okp)
 
589
                 (eq type :vl-always-comb))
 
590
            (warn :type :vl-tricky-always-comb
 
591
                  :msg "~a0: always block does not obviously write to all of ~
 
592
                        its registers in every if/else branch."
 
593
                  :args (list always))
 
594
          (ok)))
 
595
 
581
596
       ;; Otherwise this pretty strongly seems to be intended to be a
582
597
       ;; combinational always block.  At this point it's probably fine to
583
598
       ;; start issuing warnings.
648
663
  :short "Convert a combinational always block into assignments."
649
664
  :long "<p>Basic examples of what we're trying to do here:</p>
650
665
@({
651
 
    always @(*)            ---->   assign lhs = condition1 ? expr1
652
 
       if (condition1)                        : condition2 ? expr2
653
 
          lhs = expr1;                        : expr3
 
666
    always @(*)            ---->   assign lhs = condition1 ? {expr1}
 
667
       if (condition1)                        : condition2 ? {expr2}
 
668
          lhs = expr1;                        : {expr3}
654
669
       else if (condition2)
655
670
          lhs = expr2;
656
671
       else
657
672
          lhs = expr3;
658
673
 
659
 
    always @(*)            ---->   assign lhs = condition ? expr2 : expr1
 
674
    always @(*)            ---->   assign lhs = condition ? {expr2} : {expr1}
660
675
       lhs = expr1;
661
676
       if (condition)
662
677
          lhs = expr2;
671
686
 
672
687
<p>To avoid this, we locally use the @(see stmttemps) transform before trying
673
688
to carry out this expression building.  This should ensure that all lhses/rhses
674
 
are well-typed and have compatible widths.</p>")
 
689
are well-typed and have compatible widths.  The excessive use of concatenations
 
690
above ensures that everything is unsigned, to avoid creating badly typed
 
691
@('?:') expressions.</p>
 
692
 
 
693
<p>Slight twist.  If we know that this is supposed to be a combinational always
 
694
block because it's written with @('always_comb'), then we allow the lhs to not
 
695
be written in every branch.  In this case a Verilog simulator may not trigger
 
696
any update of the variable, essentially treating it like a latch.  However, it
 
697
seems quite likely that a synthesis tool will not infer a latch.  To try to
 
698
avoid making mistakes here, we want to make sure to drive the variable to Xes
 
699
in this case.</p>
 
700
 
 
701
<p>To drive the variable to Xes, a simple thing to do is, e.g.,</p>
 
702
 
 
703
@({
 
704
    always_comb           --->  always_comb
 
705
       if (condition)              lhs = XXXX
 
706
          lhs = expr;              if (condition)
 
707
       if (condition2)                lhs = expr;
 
708
          lhs = expr2;             if (condition2)
 
709
                                      lhs = expr2;
 
710
})
 
711
 
 
712
<p>This is safe even if all the branches are covered (in which case we're
 
713
simply setting the variable to X and then to its real value).</p>")
675
714
 
676
715
(define vl-atomicstmt-cblock-varexpr
677
716
  :short "Update our current expression for @('varname') to account for a new
679
718
  ((varname  stringp          "Variable we're considering.")
680
719
   (x        (and (vl-stmt-p x)
681
720
                  (vl-atomicstmt-p x))  "Statement that we're now encountering.")
682
 
   (curr     vl-maybe-expr-p  "Expression we've built for varname up until now."))
 
721
   (curr     vl-expr-p
 
722
             "Expression we've built for varname up until now.  (Initially an
 
723
              appropriately sized X.)"))
683
724
  :guard (vl-atomicstmt-cblock-p x)
684
 
  :returns (expr? (and (vl-maybe-expr-p expr?)
685
 
                       (implies curr expr?))
 
725
  :returns (expr? vl-expr-p
686
726
                  :hyp :fguard
687
727
                  "New expression to assign to varname, after taking this
688
728
                   statement into account.")
691
731
     ;; Null statement has no effect
692
732
     curr)
693
733
    (:vl-assignstmt
694
 
     (if (equal varname (vl-idexpr->name (vl-assignstmt->lvalue x)))
695
 
         ;; Assign a new expression to this var
696
 
         (vl-assignstmt->expr x)
697
 
       ;; Assignment to some other var doesn't affect var.
698
 
       curr))
 
734
     (b* (((unless (equal varname (vl-idexpr->name (vl-assignstmt->lvalue x))))
 
735
           ;; Assignment to some other var doesn't affect var.
 
736
           curr)
 
737
          ;; Assign a new expression to this var
 
738
          (expr       (vl-assignstmt->expr x))
 
739
          (finalwidth (vl-expr->finalwidth expr))
 
740
          (- (or (posp finalwidth)
 
741
                 ;; Should not happen because of stmttemps
 
742
                 (raise "No size on expression.")))
 
743
          (wrapper (make-vl-nonatom :op :vl-concat
 
744
                                    :args (list expr)
 
745
                                    :finalwidth finalwidth
 
746
                                    :finaltype :vl-unsigned)))
 
747
       wrapper))
699
748
    (otherwise
700
749
     curr))
701
750
  :prepwork
713
762
    :short "Construct the expression for a single variable."
714
763
    ((varname  stringp         "Variable we're considering.")
715
764
     (x        vl-stmt-p       "Statement we're descending through.")
716
 
     (curr     vl-maybe-expr-p "Expression we've built up for varname so far, if any."))
 
765
     (curr     vl-expr-p       "Expression we've built up for varname so far."))
717
766
    :guard (vl-stmt-cblock-p x)
718
767
    :verify-guards nil
719
 
    :returns (expr? (and (implies curr expr?)
720
 
                         (vl-maybe-expr-p expr?))
 
768
    :returns (expr? vl-expr-p
721
769
                    :hyp :fguard
722
770
                    "New expression for varname, if any")
723
771
    :measure (vl-stmt-count x)
741
789
                ;;   var = curr
742
790
                ;;   if (condition) [nothing] else var = false;
743
791
                (vl-safe-qmark-expr x.condition curr false-expr)))
744
 
            ;; Possibility 1: this is something like:
 
792
            ;; Since we are initializing all variables to X, the only reason we 
 
793
            ;; can be here is that we have something like:
745
794
            ;;    var = curr
746
795
            ;;    if (condition) othervar = blah;
747
 
            ;; We don't care, just keep our current binding for var.
748
 
            ;;
749
 
            ;; Possibility 2: this is something like:
750
 
            ;;    begin
751
 
            ;;      if (condition) var = blah;
752
 
            ;;      var = blah2;
753
 
            ;;    end
754
 
            ;; and we don't even have a binding for var yet.  This is subtle
755
 
            ;; but fine.  We don't care that this IF statement binds VAR, because
756
 
            ;; we know that VAR is ultimately bound on every path, so something
757
 
            ;; later has to overwrite it.
 
796
            ;; and we're encountering the IF.  We don't care because this if
 
797
            ;; doesn't have anything to do with var.
758
798
            curr))
759
799
 
760
800
         ((when (vl-blockstmt-p x))
767
807
  (define vl-stmtlist-cblock-varexpr
768
808
    ((varname  stringp         "Variable we're considering.")
769
809
     (x        vl-stmtlist-p   "Statement we're descending through.")
770
 
     (curr     vl-maybe-expr-p "Expression we've built up for varname so far, if any."))
 
810
     (curr     vl-expr-p       "Expression we've built up for varname so far."))
771
811
    :guard (vl-stmtlist-cblock-p x)
772
812
    :returns (expr? (and (implies curr expr?)
773
813
                         (vl-maybe-expr-p expr?))
782
822
  ///
783
823
  (verify-guards vl-stmt-cblock-varexpr))
784
824
 
785
 
(define vl-cblock-make-assign ((name   stringp)
 
825
(define vl-cblock-make-assign ((name  stringp)
786
826
                               (vars  vl-vardecllist-p)
787
827
                               (body  vl-stmt-p)
788
828
                               (ctx   vl-always-p))
789
829
  :returns (assigns vl-assignlist-p :hyp :fguard)
790
830
  :guard (vl-stmt-cblock-p body)
791
 
  (b* ((expr (vl-stmt-cblock-varexpr name body nil))
792
 
       ((unless expr)
793
 
        (raise "Failed to construct var expr for ~x0??" name))
794
 
       (decl (vl-find-vardecl name vars))
 
831
  (b* ((decl (vl-find-vardecl name vars))
795
832
       ((unless decl)
796
833
        (raise "Failed to find reg decl for ~x0??" name))
797
 
       ((vl-vardecl decl) decl)
798
834
       ((unless (and (vl-simplereg-p decl)
799
835
                     (vl-maybe-range-resolved-p (vl-simplereg->range decl))))
800
836
        (raise "Variable decl too hard for ~x0??" name))
801
837
       (size (vl-maybe-range-size (vl-simplereg->range decl)))
802
838
       (type (if (vl-simplereg->signedp decl) :vl-signed :vl-unsigned))
 
839
       (initial-x
 
840
        ;; Create an appropriately-sized X to initialize the variable with.
 
841
        ;; This variable will only matter if some branches of the IF do not
 
842
        ;; assign to this variable.  This is unsigned to agree with the
 
843
        ;; concatenations around the expressions above.
 
844
        (make-vl-atom :guts (make-vl-weirdint :origwidth size
 
845
                                              :origtype :vl-unsigned
 
846
                                              :bits (repeat size :vl-xval)
 
847
                                              :wasunsized nil)
 
848
                      :finalwidth size
 
849
                      :finaltype :vl-unsigned))
 
850
       (expr (vl-stmt-cblock-varexpr name body initial-x))
803
851
       (lhs  (vl-idexpr name size type))
804
852
       (assign (make-vl-assign :lvalue lhs
805
853
                               :expr expr
878
926
       ((mv delta cvtregs2) (vl-cblocks-synth (cdr x) vars delta)))
879
927
    (mv delta (append cvtregs1 cvtregs2))))
880
928
 
881
 
 
882
929
(define vl-module-combinational-elim ((x vl-module-p))
883
930
  :returns (new-x vl-module-p :hyp :fguard)
884
931
  (b* (((vl-module x) x)
907
954
 
908
955
       ;; Found blocks to convert.  Convert them into assigns.
909
956
       (delta (vl-starting-delta x))
910
 
       (delta (change-vl-delta delta
911
 
                               :netdecls x.netdecls
912
 
                               :assigns x.assigns))
 
957
       (delta (change-vl-delta delta :assigns x.assigns))
913
958
       ((mv delta cvtregs) (vl-cblocks-synth cblocks x.vardecls delta))
914
 
       ;; The delta may have assigns, netdecls, and warnings for us.
 
959
       ;; The delta may have assigns, new vardecls, and new warnings for us.
915
960
       ((vl-delta delta) delta)
916
961
 
917
 
       (non-regs (difference (mergesort cvtregs)
918
 
                             (mergesort (vl-vardecllist->names x.vardecls))))
919
 
       ((when non-regs)
920
 
        ;; Should be impossible
921
 
        (raise "Trying to convert non-registers: ~x0.~%" non-regs)
 
962
       ((mv fixed-vardecls fixed-portdecls)
 
963
        (vl-convert-regs cvtregs x.vardecls x.portdecls))
 
964
 
 
965
       (final-vardecls (append-without-guard
 
966
                        fixed-vardecls
 
967
                        delta.vardecls))
 
968
 
 
969
       ;; Extra sanity check: final vardecls had better all be unique
 
970
       ((unless (uniquep (vl-vardecllist->names final-vardecls)))
 
971
        (raise "Name clash when converting combinational blocks!  ~x0."
 
972
               (duplicated-members (vl-vardecllist->names final-vardecls)))
922
973
        x)
923
974
 
924
 
       ((mv vardecls-to-convert new-vardecls)
925
 
        (vl-filter-vardecls cvtregs x.vardecls))
926
 
 
927
 
       (new-netdecls (append (vl-always-convert-regs vardecls-to-convert)
928
 
                             delta.netdecls))
929
975
       (new-x (change-vl-module x
930
976
                                :alwayses others
931
 
                                :netdecls new-netdecls
932
 
                                :vardecls new-vardecls
 
977
                                :vardecls final-vardecls
 
978
                                :portdecls fixed-portdecls
933
979
                                :assigns  delta.assigns
934
980
                                :warnings delta.warnings)))
935
981
    new-x))