← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/toe/toe-wirealist.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/toe/toe-wirealist.lisp
31
31
(in-package "VL")
32
32
(include-book "toe-emodwire")
33
33
(include-book "../mlib/range-tools")
 
34
(include-book "std/typed-lists/cons-listp" :dir :system)
34
35
(local (include-book "../util/arithmetic"))
35
36
(local (include-book "../util/intersectp-equal"))
36
37
 
615
616
    |w[msb:lsb]|))
616
617
 
617
618
 
618
 
(define vl-netdecl-msb-emodwires
619
 
  :parents (vl-wirealist-p)
620
 
  :short "Compute the @(see vl-emodwire-p)s for a net declaration, in MSB-first order."
621
 
  ((x        vl-netdecl-p)
622
 
   (warnings vl-warninglist-p))
623
 
  :returns (mv (successp booleanp :rule-classes :type-prescription)
624
 
               (warnings vl-warninglist-p)
625
 
               (emodwires vl-emodwirelist-p))
626
 
  (b* (((vl-netdecl x) x)
627
 
       ((when x.arrdims)
628
 
        (mv nil
629
 
            (fatal :type :vl-bad-netdecl
630
 
                   :msg "~a0 has array dimensions, which are not supported."
631
 
                   :args (list x))
632
 
            nil))
633
 
 
634
 
       ((when (not (vl-maybe-range-resolved-p x.range)))
635
 
        (mv nil
636
 
            (fatal :type :vl-bad-netdecl
637
 
                   :msg "~a0 has unresolved range ~a1."
638
 
                   :args (list x x.range))
639
 
            nil))
640
 
 
641
 
       ((when (not x.range))
642
 
        (mv t (ok) (list (vl-plain-wire-name x.name))))
643
 
 
644
 
       (msb          (vl-resolved->val (vl-range->msb x.range)))
645
 
       (lsb          (vl-resolved->val (vl-range->lsb x.range)))
646
 
       (|w[msb:lsb]| (vl-emodwires-from-msb-to-lsb x.name msb lsb)))
647
 
    (mv t (ok) |w[msb:lsb]|))
648
 
  ///
649
 
  (local (in-theory (enable vl-netdecl-msb-emodwires)))
650
 
 
651
 
  (defthm true-listp-of-vl-netdecl-msb-emodwires
652
 
    (true-listp (mv-nth 2 (vl-netdecl-msb-emodwires x warnings)))
653
 
    :rule-classes :type-prescription)
654
 
 
655
 
  (defthm basenames-of-vl-netdecl-msb-emodwires
656
 
    (implies (vl-netdecl-p x)
657
 
             (let ((wires (mv-nth 2 (vl-netdecl-msb-emodwires x warnings))))
658
 
               (equal (vl-emodwirelist->basenames wires)
659
 
                      (replicate (len wires) (vl-netdecl->name x)))))
660
 
    :hints(("Goal" :in-theory (enable vl-plain-wire-name))))
661
 
 
662
 
  (defthm unique-indicies-of-vl-netdecl-msb-emodwires
663
 
    (no-duplicatesp-equal
664
 
     (vl-emodwirelist->indices
665
 
      (mv-nth 2 (vl-netdecl-msb-emodwires x warnings))))))
666
 
 
667
 
 
668
 
(define vl-netdecllist-to-wirealist
669
 
  :parents (vl-wirealist-p)
670
 
  :short "Generate a (fast) wirealist from a @(see vl-netdecllist-p)."
671
 
  ((x        vl-netdecllist-p)
672
 
   (warnings vl-warninglist-p))
673
 
  :returns (mv (successp booleanp :rule-classes :type-prescription
674
 
                         "Whether <em>all</em> nets were successfully converted
675
 
                          into wire-alist entries.")
676
 
               (warnings vl-warninglist-p)
677
 
               (walist   vl-wirealist-p))
678
 
  :long "<p>Even if @('successp') is @('nil'), we will produce at least a
679
 
partial wire alist for this module which is as complete as possible.  Any
680
 
failure will result in at least one fatal warning.</p>"
681
 
 
682
 
  (b* (((when (atom x))
683
 
        (mv t (ok) nil))
684
 
       ((mv successp1 warnings wires1)
685
 
        (vl-netdecl-msb-emodwires (car x) warnings))
686
 
       ((mv successp2 warnings walist)
687
 
        (vl-netdecllist-to-wirealist (cdr x) warnings))
688
 
       (successp (and successp1 successp2))
689
 
       (walist   (if successp1
690
 
                     (hons-acons (vl-netdecl->name (car x)) wires1 walist)
691
 
                   walist)))
692
 
    (mv successp warnings walist))
693
 
  ///
694
 
  (defthm subsetp-equal-of-strip-cars-of-vl-netdecllist-to-wirealist
695
 
    (subsetp-equal (strip-cars (mv-nth 2 (vl-netdecllist-to-wirealist x warnings)))
696
 
                   (vl-netdecllist->names x))))
697
 
 
698
619
(define vl-vardecl-msb-emodwires
699
620
  :parents (vl-wirealist-p)
700
 
  :short "Same as @(see vl-netdecl-msb-emodwires), but for variables."
 
621
  :short "Compute the @(see vl-emodwire-p)s for a variable declaration, in MSB-first order."
701
622
  ((x        vl-vardecl-p)
702
623
   (warnings vl-warninglist-p))
703
624
  :returns (mv (successp  booleanp :rule-classes :type-prescription)
704
625
               (warnings  vl-warninglist-p)
705
626
               (emodwires vl-emodwirelist-p))
706
627
  (b* (((vl-vardecl x) x)
707
 
       ((unless (vl-simplereg-p x))
 
628
 
 
629
       ((unless (vl-simplevar-p x))
708
630
        (mv nil
709
631
            (fatal :type :vl-bad-vardecl
710
 
                   :msg "~a0 is not yet supported: we only handle simple reg/logic ~
711
 
                         wires with at most a single range."
 
632
                   :msg "~a0 is not yet supported: we only handle simple ~
 
633
                         wires and reg/logic variables  with at most a single ~
 
634
                         range."
712
635
                   :args (list x))
713
636
            nil))
714
 
       (range (vl-simplereg->range x))
 
637
 
 
638
       (range (vl-simplevar->range x))
715
639
       ((unless (vl-maybe-range-resolved-p range))
716
640
        (mv nil
717
641
            (fatal :type :vl-bad-vardecl
718
642
                   :msg "~a0 has unresolved range ~a1."
719
643
                   :args (list x range))
720
644
            nil))
 
645
 
721
646
       ((unless range)
722
647
        (mv t (ok) (list (vl-plain-wire-name x.name))))
 
648
 
723
649
       (msb          (vl-resolved->val (vl-range->msb range)))
724
650
       (lsb          (vl-resolved->val (vl-range->lsb range)))
725
651
       (|w[msb:lsb]| (vl-emodwires-from-msb-to-lsb x.name msb lsb)))
742
668
      (mv-nth 2 (vl-vardecl-msb-emodwires x warnings))))))
743
669
 
744
670
 
745
 
(defsection vl-vardecllist-to-wirealist
 
671
(define vl-vardecllist-to-wirealist
746
672
  :parents (vl-wirealist-p)
747
 
  :short "Same as @(see vl-netdecllist-to-wirealist), but for variables."
748
 
 
749
 
  (defund vl-vardecllist-to-wirealist (x warnings)
750
 
    (declare (xargs :guard (and (vl-vardecllist-p x)
751
 
                                (vl-warninglist-p warnings))))
752
 
    (if (atom x)
753
 
        (mv t warnings nil)
754
 
      (b* (((mv successp1 warnings wires1)
755
 
            (vl-vardecl-msb-emodwires (car x) warnings))
756
 
           ((mv successp2 warnings walist)
757
 
            (vl-vardecllist-to-wirealist (cdr x) warnings))
758
 
           (successp (and successp1 successp2))
759
 
           (walist   (if successp1
760
 
                         (hons-acons (vl-vardecl->name (car x)) wires1 walist)
761
 
                       walist)))
762
 
        (mv successp warnings walist))))
763
 
 
764
 
  (local (in-theory (enable vl-vardecllist-to-wirealist)))
765
 
 
766
 
  (defthm vl-warninglist-p-of-vl-vardecllist-to-wirealist
767
 
    (implies (force (vl-warninglist-p warnings))
768
 
             (vl-warninglist-p (mv-nth 1 (vl-vardecllist-to-wirealist x warnings)))))
769
 
 
770
 
  (defthm vl-wirealist-p-of-vl-vardecllist-to-wirealist
771
 
    (implies (force (vl-vardecllist-p x))
772
 
             (vl-wirealist-p (mv-nth 2 (vl-vardecllist-to-wirealist x warnings)))))
773
 
 
 
673
  :short "Generate a (fast) wirealist from a @(see vl-vardecllist-p)."
 
674
  ((x        vl-vardecllist-p)
 
675
   (warnings vl-warninglist-p))
 
676
  :returns (mv (successp booleanp :rule-classes :type-prescription)
 
677
               (warnings vl-warninglist-p)
 
678
               (wire-alist vl-wirealist-p))
 
679
  (b* (((when (atom x))
 
680
        (mv t (ok) nil))
 
681
       ((mv successp1 warnings wires1)
 
682
        (vl-vardecl-msb-emodwires (car x) warnings))
 
683
       ((mv successp2 warnings walist)
 
684
        (vl-vardecllist-to-wirealist (cdr x) warnings))
 
685
       (successp (and successp1 successp2))
 
686
       (walist   (if successp1
 
687
                     (hons-acons (vl-vardecl->name (car x)) wires1 walist)
 
688
                   walist)))
 
689
    (mv successp warnings walist))
 
690
  ///
774
691
  (defthm subsetp-equal-of-strip-cars-of-vl-vardecllist-to-wirealist
775
692
    (subsetp-equal (strip-cars (mv-nth 2 (vl-vardecllist-to-wirealist x warnings)))
776
693
                   (vl-vardecllist->names x))))
777
694
 
778
 
 
779
 
(defsection vl-module-wirealist
 
695
(define vl-module-wirealist
780
696
  :parents (vl-wirealist-p)
781
697
  :short "Safely generate the (fast) wirealist for a module."
782
 
 
783
 
  :long "<p><b>Signature:</b> @(call vl-module-wirealist) returns @('(mv
784
 
successp warnings walist)').</p>
785
 
 
786
 
<p>Note: this function is memoized and generates fast alists.  You should be
787
 
sure to clear its memo table so that these fast alists can be garbage
 
698
  ((x        vl-module-p)
 
699
   (warnings vl-warninglist-p))
 
700
  :returns (mv (successp booleanp :rule-classes :type-prescription)
 
701
               (warnings vl-warninglist-p)
 
702
               (wire-alist vl-wirealist-p))
 
703
  :long "<p>Note: this function is memoized and generates fast alists.  You
 
704
should be sure to clear its memo table so that these fast alists can be garbage
788
705
collected.</p>
789
706
 
790
707
<p>This function can fail, setting @('successp') to @('nil') and adding fatal
812
729
 
813
730
@(thm no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist)"
814
731
 
815
 
  (defund vl-module-wirealist (x warnings)
816
 
    (declare (xargs :guard (and (vl-module-p x)
817
 
                                (vl-warninglist-p warnings))))
818
732
    (b* (((vl-module x) x)
819
733
 
820
734
; Name uniqueness check.
867
781
; versions of the Hons code, you may wish to revisit it!
868
782
 
869
783
         ((unless (mbe :logic
870
 
                       (uniquep (append (vl-netdecllist->names x.netdecls)
871
 
                                        (vl-vardecllist->names x.vardecls)))
 
784
                       (uniquep (vl-vardecllist->names x.vardecls))
872
785
                       :exec
873
 
                       (let* ((names (vl-netdecllist->names-exec x.netdecls nil))
874
 
                              (names (vl-vardecllist->names-exec x.vardecls names)))
875
 
                         (uniquep names))))
 
786
                       (uniquep (vl-vardecllist->names-exec x.vardecls nil))))
876
787
          (mv nil
877
 
              (cons (make-vl-warning :type :vl-namespace-error
878
 
                                     :msg "~m0 illegally redefines ~&1."
879
 
                                     :args (list x.name
880
 
                                                 (duplicated-members
881
 
                                                  (append (vl-netdecllist->names x.netdecls)
882
 
                                                          (vl-vardecllist->names x.vardecls))))
883
 
                                     :fatalp t
884
 
                                     :fn 'vl-modwire-alist)
885
 
                    warnings)
886
 
              nil))
887
 
 
888
 
         ((mv successp1 warnings net-walist)
889
 
          (vl-netdecllist-to-wirealist x.netdecls warnings))
890
 
         ((mv successp2 warnings reg-walist)
891
 
          (vl-vardecllist-to-wirealist x.vardecls warnings))
892
 
 
893
 
         ;; In practice this hons-shrink-alist shouldn't really be more
894
 
         ;; expensive than having used an accumulator, because most modules
895
 
         ;; have very few registers.
896
 
         (walist   (hons-shrink-alist reg-walist net-walist))
897
 
 
898
 
         ;; Walist stole the hash table for net-walist, but we still need
899
 
         ;; to free the reg-walist.
900
 
         (- (fast-alist-free reg-walist))
901
 
         (successp (and successp1 successp2)))
902
 
      (mv successp warnings walist)))
903
 
 
904
 
  (local (in-theory (enable vl-module-wirealist)))
905
 
 
906
 
  (defthm vl-warninglist-p-of-vl-module-wirealist
907
 
    (implies (force (vl-warninglist-p warnings))
908
 
             (vl-warninglist-p (mv-nth 1 (vl-module-wirealist x warnings)))))
909
 
 
910
 
  (defthm vl-wirealist-p-of-vl-module-wirealist
911
 
    (implies (force (vl-module-p x))
912
 
             (vl-wirealist-p (mv-nth 2 (vl-module-wirealist x warnings)))))
913
 
 
914
 
  (memoize 'vl-module-wirealist))
915
 
 
916
 
 
917
 
(defsection no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist
918
 
 
919
 
  (defthm equal-of-cons-rewrite
920
 
    (equal (equal (cons a b) x)
921
 
           (and (consp x)
922
 
                (equal (car x) a)
923
 
                (equal (cdr x) b))))
924
 
 
925
 
  (local (defthm append-alist-vals-removal
926
 
           (equal (append-alist-vals x)
927
 
                  (flatten (strip-cdrs x)))
928
 
           :hints(("Goal" :induct (len x)))))
929
 
 
930
 
  (local
931
 
   (defsection vardecls
932
 
 
933
 
     (defthm rcars
934
 
       (implies (no-duplicatesp-equal (vl-vardecllist->names x))
935
 
                (no-duplicatesp-equal
936
 
                 (strip-cars (mv-nth 2 (vl-vardecllist-to-wirealist x warnings)))))
937
 
       :hints(("Goal" :in-theory (enable vl-vardecllist-to-wirealist))))
938
 
 
939
 
     (local
940
 
      (defthm r0
941
 
        (implies (and (not (member-equal (vl-vardecl->name a)
942
 
                                         (vl-vardecllist->names x)))
943
 
                      ;(force (vl-vardecl-p a))
944
 
                      (consp x)
945
 
                      )
946
 
                 (not (equal (vl-vardecl->name a)
947
 
                             (vl-vardecl->name (first x)))))))
948
 
 
949
 
     (local
950
 
      (defthm r1
951
 
        (implies (and (force (not (equal (vl-vardecl->name a)
952
 
                                         (vl-vardecl->name b))))
953
 
                      (force (vl-vardecl-p a))
954
 
                      (force (vl-vardecl-p b)))
955
 
                 (not (intersectp-equal
956
 
                       (mv-nth 2 (vl-vardecl-msb-emodwires a warnings1))
957
 
                       (mv-nth 2 (vl-vardecl-msb-emodwires b warnings2)))))
958
 
        :hints(("Goal"
959
 
                :use ((:instance empty-intersect-of-vl-emodwires-by-basename
960
 
                                 (xname (vl-vardecl->name a))
961
 
                                 (yname (vl-vardecl->name b))
962
 
                                 (x (mv-nth 2 (vl-vardecl-msb-emodwires a warnings1)))
963
 
                                 (y (mv-nth 2 (vl-vardecl-msb-emodwires b warnings2)))))))))
964
 
 
965
 
     (local
966
 
      (defthm r2
967
 
        (let ((r-wires          (mv-nth 2 (vl-vardecl-msb-emodwires r warnings1)))
968
 
              (other-wire-lists (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist others warnings2)))))
969
 
          (implies (and (force (not (member-equal (vl-vardecl->name r)
970
 
                                                  (vl-vardecllist->names others))))
971
 
                        (force (vl-vardecl-p r))
972
 
                        (force (vl-vardecllist-p others)))
973
 
                   (empty-intersect-with-each-p r-wires
974
 
                                                other-wire-lists)))
975
 
        :hints(("Goal"
976
 
                :induct (vl-vardecllist-to-wirealist others warnings2)
977
 
                :in-theory (enable vl-vardecllist-to-wirealist)))))
978
 
 
979
 
     (defthm rcdrs
980
 
       (implies (and (no-duplicatesp-equal (vl-vardecllist->names x))
981
 
                     (force (vl-vardecllist-p x)))
982
 
                (no-duplicatesp-equal
983
 
                 (flatten (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist x warnings))))))
984
 
       :hints(("Goal"
985
 
               :in-theory (enable vl-vardecllist-to-wirealist)
986
 
               :induct (vl-vardecllist-to-wirealist x warnings))))))
987
 
 
988
 
 
989
 
  ;; Lemmas for netdecls... same as vardecls.
990
 
 
991
 
  (local
992
 
   (defsection netdecls
993
 
 
994
 
     (defthm ncars
995
 
       (implies (no-duplicatesp-equal (vl-netdecllist->names x))
996
 
                (no-duplicatesp-equal
997
 
                 (strip-cars (mv-nth 2 (vl-netdecllist-to-wirealist x warnings)))))
998
 
       :hints(("Goal" :in-theory (enable vl-netdecllist-to-wirealist))))
999
 
 
1000
 
     (local
1001
 
      (defthm n0
1002
 
        (implies (and (not (member-equal (vl-netdecl->name a)
1003
 
                                         (vl-netdecllist->names x)))
1004
 
                      ;; (force (vl-netdecl-p a))
1005
 
                      (force (consp x))
1006
 
                      )
1007
 
                 (not (equal (vl-netdecl->name a)
1008
 
                             (vl-netdecl->name (first x)))))))
1009
 
 
1010
 
     (local
1011
 
      (defthm n1
1012
 
        (implies (and (force (not (equal (vl-netdecl->name a)
1013
 
                                         (vl-netdecl->name b))))
1014
 
                      (force (vl-netdecl-p a))
1015
 
                      (force (vl-netdecl-p b)))
1016
 
                 (not (intersectp-equal
1017
 
                       (mv-nth 2 (vl-netdecl-msb-emodwires a warnings1))
1018
 
                       (mv-nth 2 (vl-netdecl-msb-emodwires b warnings2)))))
1019
 
        :hints(("Goal"
1020
 
                :use ((:instance empty-intersect-of-vl-emodwires-by-basename
1021
 
                                 (xname (vl-netdecl->name a))
1022
 
                                 (yname (vl-netdecl->name b))
1023
 
                                 (x (mv-nth 2 (vl-netdecl-msb-emodwires a warnings1)))
1024
 
                                 (y (mv-nth 2 (vl-netdecl-msb-emodwires b warnings2)))))))))
1025
 
 
1026
 
     (local
1027
 
      (defthm n2
1028
 
        (let ((r-wires          (mv-nth 2 (vl-netdecl-msb-emodwires r warnings1)))
1029
 
              (other-wire-lists (strip-cdrs (mv-nth 2 (vl-netdecllist-to-wirealist others warnings2)))))
1030
 
          (implies (and (force (not (member-equal (vl-netdecl->name r)
1031
 
                                                  (vl-netdecllist->names others))))
1032
 
                        (force (vl-netdecl-p r))
1033
 
                        (force (vl-netdecllist-p others)))
1034
 
                   (empty-intersect-with-each-p r-wires
1035
 
                                                other-wire-lists)))
1036
 
        :hints(("Goal"
1037
 
                :induct (vl-netdecllist-to-wirealist others warnings2)
1038
 
                :in-theory (enable vl-netdecllist-to-wirealist)))))
1039
 
 
1040
 
     (defthm ncdrs
1041
 
       (implies (and (no-duplicatesp-equal (vl-netdecllist->names x))
1042
 
                     (force (vl-netdecllist-p x)))
1043
 
                (no-duplicatesp-equal
1044
 
                 (flatten (strip-cdrs (mv-nth 2 (vl-netdecllist-to-wirealist x warnings))))))
1045
 
       :hints(("Goal"
1046
 
               :in-theory (enable vl-netdecllist-to-wirealist)
1047
 
               :induct (vl-netdecllist-to-wirealist x warnings))))))
1048
 
 
1049
 
 
1050
 
  (local
1051
 
   (defsection var/netdecls
1052
 
 
1053
 
; One more lemma to show there aren't any duplicates between the separate
1054
 
; var/net declarations.
1055
 
 
1056
 
     (local
1057
 
      (defthm rn-0
1058
 
        (let ((wires (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist x warnings)))))
1059
 
          (implies (force (vl-vardecllist-p x))
1060
 
                   (subsetp-equal (vl-emodwirelist->basenames (flatten wires))
1061
 
                                  (vl-vardecllist->names x))))
1062
 
        :hints(("Goal"
1063
 
                :induct (vl-vardecllist-to-wirealist x warnings)
1064
 
                :in-theory (enable vl-vardecllist-to-wirealist))
1065
 
               (set-reasoning))))
1066
 
 
1067
 
     (local
1068
 
      (defthm rn-1
1069
 
        (let ((wires (strip-cdrs (mv-nth 2 (vl-netdecllist-to-wirealist x warnings)))))
1070
 
          (implies (force (vl-netdecllist-p x))
1071
 
                   (subsetp-equal (vl-emodwirelist->basenames (flatten wires))
1072
 
                                  (vl-netdecllist->names x))))
1073
 
        :hints(("Goal"
1074
 
                :induct (vl-netdecllist-to-wirealist x warnings)
1075
 
                :in-theory (enable vl-netdecllist-to-wirealist))
1076
 
               (set-reasoning))))
1077
 
 
1078
 
     (local
1079
 
      (defthm rn-2
1080
 
        (let ((nwires (strip-cdrs (mv-nth 2 (vl-netdecllist-to-wirealist nets warnings1))))
1081
 
              (rwires (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist vars warnings2)))))
1082
 
          (implies (and (force (not (intersectp-equal
1083
 
                                     (vl-vardecllist->names vars)
1084
 
                                     (vl-netdecllist->names nets))))
1085
 
                        (force (vl-netdecllist-p nets))
1086
 
                        (force (vl-vardecllist-p vars)))
1087
 
                   (not (intersectp-equal
1088
 
                         (vl-emodwirelist->basenames (flatten nwires))
1089
 
                         (vl-emodwirelist->basenames (flatten rwires))))))))
1090
 
 
1091
 
     (local
1092
 
      (defthm crock
1093
 
        (implies (not (intersectp-equal (vl-emodwirelist->basenames x)
1094
 
                                        (vl-emodwirelist->basenames y)))
1095
 
                 (not (intersectp-equal x y)))
1096
 
        :hints(("Goal" :induct (len x)))))
1097
 
 
1098
 
     (defthm var/netdecls
1099
 
       (let ((nwires (strip-cdrs (mv-nth 2 (vl-netdecllist-to-wirealist nets warnings1))))
1100
 
             (rwires (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist vars warnings2)))))
1101
 
         (implies (and (force (not (intersectp-equal
1102
 
                                    (vl-vardecllist->names vars)
1103
 
                                    (vl-netdecllist->names nets))))
1104
 
                       (force (vl-netdecllist-p nets))
1105
 
                       (force (vl-vardecllist-p vars)))
1106
 
                  (not (intersectp-equal (flatten nwires)
1107
 
                                         (flatten rwires))))))))
1108
 
 
1109
 
 
1110
 
; These decompose the main goal so that our lemmas apply:
1111
 
 
1112
 
  (local (defthm hons-assoc-equal-under-iff
1113
 
           (implies (cons-listp x)
1114
 
                    (iff (hons-assoc-equal a x)
1115
 
                         (member-equal a (strip-cars x))))
1116
 
           :hints(("Goal" :in-theory (enable hons-assoc-equal
1117
 
                                             strip-cars)))))
1118
 
 
1119
 
  (local (defthm unique-hons-shrink-alist-is-revappend
1120
 
           ;; Forcing this in general would be terrible, but for this proof
1121
 
           ;; it's what we want to do.
1122
 
           (implies (and (force (no-duplicatesp-equal (strip-cars x)))
1123
 
                         (force (not (intersectp-equal (strip-cars x) (strip-cars y))))
1124
 
                         (force (cons-listp x))
1125
 
                         (force (cons-listp y)))
1126
 
                    (equal (hons-shrink-alist x y)
1127
 
                           (revappend x y)))
1128
 
           :hints(("Goal" :in-theory (enable hons-shrink-alist)))))
1129
 
 
1130
 
  (local (in-theory (enable vl-module-wirealist)))
1131
 
 
1132
 
  (defthm no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist
1133
 
    (implies (vl-module-p x)
1134
 
             (let ((walist (mv-nth 2 (vl-module-wirealist x warnings))))
1135
 
               (no-duplicatesp-equal (append-alist-vals walist))))))
1136
 
 
1137
 
 
1138
 
 
1139
 
(defsection vl-msb-constint-bitlist
 
788
              (fatal :type :vl-namespace-error
 
789
                     :msg "~m0 illegally redefines ~&1."
 
790
                     :args (list x.name
 
791
                                 (duplicated-members (vl-vardecllist->names x.vardecls))))
 
792
              nil)))
 
793
 
 
794
      (vl-vardecllist-to-wirealist x.vardecls warnings))
 
795
 
 
796
    ///
 
797
    (memoize 'vl-module-wirealist)
 
798
 
 
799
    ;; Wow, this proof is way simpler now that vardecls/netdecls are merged.
 
800
 
 
801
    (local (defthm append-alist-vals-removal
 
802
             (equal (append-alist-vals x)
 
803
                    (flatten (strip-cdrs x)))
 
804
             :hints(("Goal" :induct (len x)))))
 
805
 
 
806
    (local (defthm rcars
 
807
             (implies (no-duplicatesp-equal (vl-vardecllist->names x))
 
808
                      (no-duplicatesp-equal
 
809
                       (strip-cars (mv-nth 2 (vl-vardecllist-to-wirealist x warnings)))))
 
810
             :hints(("Goal" :in-theory (enable vl-vardecllist-to-wirealist)))))
 
811
 
 
812
    (local
 
813
     (defthm r0
 
814
       (implies (and (not (member-equal (vl-vardecl->name a)
 
815
                                        (vl-vardecllist->names x)))
 
816
                     (consp x))
 
817
                (not (equal (vl-vardecl->name a)
 
818
                            (vl-vardecl->name (first x)))))))
 
819
 
 
820
    (local
 
821
     (defthm r1
 
822
       (implies (and (force (not (equal (vl-vardecl->name a)
 
823
                                        (vl-vardecl->name b))))
 
824
                     (force (vl-vardecl-p a))
 
825
                     (force (vl-vardecl-p b)))
 
826
                (not (intersectp-equal
 
827
                      (mv-nth 2 (vl-vardecl-msb-emodwires a warnings1))
 
828
                      (mv-nth 2 (vl-vardecl-msb-emodwires b warnings2)))))
 
829
       :hints(("Goal"
 
830
               :use ((:instance empty-intersect-of-vl-emodwires-by-basename
 
831
                      (xname (vl-vardecl->name a))
 
832
                      (yname (vl-vardecl->name b))
 
833
                      (x (mv-nth 2 (vl-vardecl-msb-emodwires a warnings1)))
 
834
                      (y (mv-nth 2 (vl-vardecl-msb-emodwires b warnings2)))))))))
 
835
 
 
836
    (local
 
837
     (defthm r2
 
838
       (let ((r-wires          (mv-nth 2 (vl-vardecl-msb-emodwires r warnings1)))
 
839
             (other-wire-lists (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist others warnings2)))))
 
840
         (implies (and (force (not (member-equal (vl-vardecl->name r)
 
841
                                                 (vl-vardecllist->names others))))
 
842
                       (force (vl-vardecl-p r))
 
843
                       (force (vl-vardecllist-p others)))
 
844
                  (empty-intersect-with-each-p r-wires
 
845
                                               other-wire-lists)))
 
846
       :hints(("Goal"
 
847
               :induct (vl-vardecllist-to-wirealist others warnings2)
 
848
               :in-theory (enable vl-vardecllist-to-wirealist)))))
 
849
 
 
850
    (local (defthm rcdrs
 
851
             (implies (and (no-duplicatesp-equal (vl-vardecllist->names x))
 
852
                           (force (vl-vardecllist-p x)))
 
853
                      (no-duplicatesp-equal
 
854
                       (flatten (strip-cdrs (mv-nth 2 (vl-vardecllist-to-wirealist x warnings))))))
 
855
             :hints(("Goal"
 
856
                     :in-theory (enable vl-vardecllist-to-wirealist)
 
857
                     :induct (vl-vardecllist-to-wirealist x warnings)))))
 
858
 
 
859
    (defthm no-duplicatesp-equal-of-append-alist-vals-of-vl-module-wirealist
 
860
      (let ((walist (mv-nth 2 (vl-module-wirealist x warnings))))
 
861
        (no-duplicatesp-equal (append-alist-vals walist)))))
 
862
 
 
863
 
 
864
 
 
865
 
 
866
(define vl-msb-constint-bitlist-aux ((value natp) acc)
 
867
  :parents (vl-msb-constint-bitlist)
 
868
  :short "Produce an MSB-ordered list of the bits for some value."
 
869
  :prepwork ((local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system)))
 
870
  :measure (nfix value)
 
871
  (b* (((when (zp value))
 
872
        acc)
 
873
       (floor2 (mbe :logic (floor value 2)
 
874
                    :exec (ash value -1)))
 
875
       (mod2   (mbe :logic (mod value 2)
 
876
                    :exec (rem value 2)))
 
877
       (bit    (if (eql mod2 0)
 
878
                   'acl2::f
 
879
                 'acl2::t)))
 
880
    (vl-msb-constint-bitlist-aux floor2 (cons bit acc)))
 
881
  ///
 
882
  (defthm true-listp-of-vl-msb-constint-bitlist-aux
 
883
    (implies (true-listp acc)
 
884
             (true-listp (vl-msb-constint-bitlist-aux value acc)))
 
885
    :rule-classes :type-prescription)
 
886
 
 
887
  (defthm vl-emodwirelist-p-of-vl-msb-constint-bitlist-aux
 
888
    (implies (vl-emodwirelist-p acc)
 
889
             (vl-emodwirelist-p (vl-msb-constint-bitlist-aux value acc)))))
 
890
 
 
891
(define vl-msb-constint-bitlist
1140
892
  :parents (vl-msb-expr-bitlist)
1141
893
  :short "Produce the @(see vl-emodwire-p)s for a @(see vl-constint-p)."
1142
894
 
1143
 
  :long "<p><b>Signature:</b> @(call vl-msb-constint-bitlist) returns @('(mv
1144
 
successp warnings bits)').</p>
 
895
  ((x vl-expr-p)
 
896
   (warnings vl-warninglist-p))
 
897
  :guard (and (vl-atom-p x)
 
898
              (vl-constint-p (vl-atom->guts x)))
 
899
  :returns (mv (successp booleanp :rule-classes :type-prescription)
 
900
               (warnings vl-warninglist-p)
 
901
               (bits     vl-emodwirelist-p))
1145
902
 
1146
 
<p>In @('defm') commands, the symbols @('ACL2::t') and @('ACL2::f') are
 
903
  :long "<p>In E modules, the symbols @('ACL2::t') and @('ACL2::f') are
1147
904
interpreted as literal 1 and 0 bits.</p>
1148
905
 
1149
906
<p>We are given an atomic, constant integer expression.  This expression has
1150
907
some width and value.  We return a <i>width</i>-long list of symbols
1151
908
@('ACL2::T') or @('ACL2::F') that represent this <i>value</i>.</p>"
1152
909
 
1153
 
  (local (include-book "arithmetic-3/floor-mod/floor-mod" :dir :system))
1154
 
 
1155
 
  (defund vl-msb-constint-bitlist-aux (value acc)
1156
 
    "Produce an MSB-ordered list of the bits for some value."
1157
 
    (declare (xargs :guard (natp value)
1158
 
                    :measure (nfix value)))
1159
 
    (if (mbe :logic (zp value)
1160
 
             :exec (= value 0))
1161
 
        acc
1162
 
      (let* ((floor2 (mbe :logic (floor value 2)
1163
 
                          :exec (ash value -1)))
1164
 
             (mod2   (mbe :logic (mod value 2)
1165
 
                          :exec (rem value 2)))
1166
 
             (bit    (if (= mod2 0)
1167
 
                         'acl2::f
1168
 
                       'acl2::t)))
1169
 
        (vl-msb-constint-bitlist-aux floor2
1170
 
                                     (cons bit acc)))))
1171
 
 
1172
 
  (defthm true-listp-of-vl-msb-constint-bitlist-aux
1173
 
    (implies (true-listp acc)
1174
 
             (true-listp (vl-msb-constint-bitlist-aux value acc)))
1175
 
    :rule-classes :type-prescription
1176
 
    :hints(("Goal" :in-theory (enable vl-msb-constint-bitlist-aux))))
1177
 
 
1178
 
  (defthm vl-emodwirelist-p-of-vl-msb-constint-bitlist-aux
1179
 
    (implies (vl-emodwirelist-p acc)
1180
 
             (vl-emodwirelist-p (vl-msb-constint-bitlist-aux value acc)))
1181
 
    :hints(("Goal" :in-theory (enable vl-msb-constint-bitlist-aux))))
1182
 
 
1183
 
 
1184
 
  (defund vl-msb-constint-bitlist (x warnings)
1185
 
    (declare (xargs :guard (and (vl-expr-p x)
1186
 
                                (vl-atom-p x)
1187
 
                                (vl-constint-p (vl-atom->guts x))
1188
 
                                (vl-warninglist-p warnings))))
1189
 
    (b* ((width (vl-atom->finalwidth x))
1190
 
         (guts  (vl-atom->guts x))
1191
 
         (value (vl-constint->value guts))
1192
 
 
1193
 
         ((unless width)
1194
 
          (b* ((w (make-vl-warning
1195
 
                   :type :vl-programming-error
1196
 
                   :msg "Cannot generate wires for ~a0 because it does not have ~
1197
 
                         a finalwidth."
1198
 
                   :args (list x)
1199
 
                   :fatalp t
1200
 
                   :fn 'vl-msb-constint-bitlist)))
1201
 
            (mv nil (cons w warnings) nil)))
1202
 
 
1203
 
         (bits (vl-msb-constint-bitlist-aux value nil))
1204
 
         (blen (length bits))
1205
 
 
1206
 
         ((when (equal blen width))
1207
 
          ;; Already the right width.  No need to pad.
1208
 
          (mv t warnings bits))
1209
 
 
1210
 
         ((when (< blen width))
1211
 
          ;; Sometimes we need to pad with extra F bits to get to the
1212
 
          ;; appropriate width.
1213
 
          (mv t warnings
1214
 
              (make-list-ac (- width blen) 'acl2::f bits)))
1215
 
 
1216
 
         ;; Else, more bits than the width permits?  This shouldn't ever happen
1217
 
         ;; if our sizing code is right.
1218
 
         (w (make-vl-warning :type :vl-programming-error
1219
 
                             :msg "Produced too many wires for ~a0. ~
1220
 
                                   Finalwidth: ~x1.  ~x2 Bits: ~x3."
1221
 
                             :args (list x (vl-atom->finalwidth x) blen bits)
1222
 
                             :fatalp t
1223
 
                             :fn 'vl-msb-constint-bitlist)))
1224
 
 
1225
 
      (mv nil (cons w warnings) nil)))
 
910
  (b* ((width (vl-atom->finalwidth x))
 
911
       (guts  (vl-atom->guts x))
 
912
       (value (vl-constint->value guts))
 
913
 
 
914
       ((unless width)
 
915
        (mv nil
 
916
            (fatal :type :vl-programming-error
 
917
                   :msg "Cannot generate wires for ~a0 because it does not ~
 
918
                         have a finalwidth."
 
919
                   :args (list x))
 
920
            nil))
 
921
 
 
922
       (bits (vl-msb-constint-bitlist-aux value nil))
 
923
       (blen (length bits))
 
924
 
 
925
       ((when (equal blen width))
 
926
        ;; Already the right width.  No need to pad.
 
927
        (mv t (ok) bits))
 
928
 
 
929
       ((when (< blen width))
 
930
        ;; Sometimes we need to pad with extra F bits to get to the
 
931
        ;; appropriate width.
 
932
        (mv t (ok) (make-list-ac (- width blen) 'acl2::f bits))))
 
933
 
 
934
    ;; Else, more bits than the width permits?  This shouldn't ever happen
 
935
    ;; if our sizing code is right.
 
936
    (mv nil
 
937
        (fatal :type :vl-programming-error
 
938
               :msg "Produced too many wires for ~a0. Finalwidth: ~x1.  ~x2 ~
 
939
                     Bits: ~x3."
 
940
               :args (list x (vl-atom->finalwidth x) blen bits))
 
941
        nil))
 
942
 
 
943
  ///
 
944
  (more-returns
 
945
   (bits true-listp :rule-classes :type-prescription))
1226
946
 
1227
947
  ;; Some basic unit tests.
1228
948
  (local (assert!
1251
971
                   (test-ok 10 1   (list f f   f f f f   f f f t))
1252
972
                   (test-ok 10 15  (list f f   f f f f   t t t t))
1253
973
                   (test-ok 10 127 (list f f   f t t t   t t t t))
1254
 
                   (test-ok 10 128 (list f f   t f f f   f f f f)))))))
1255
 
 
1256
 
  (defmvtypes vl-msb-constint-bitlist (booleanp nil true-listp))
1257
 
 
1258
 
  (local (in-theory (enable vl-msb-constint-bitlist)))
1259
 
 
1260
 
  (defthm vl-warninglist-p-of-vl-msb-constint-bitlist
1261
 
    (implies (force (vl-warninglist-p warnings))
1262
 
             (vl-warninglist-p (mv-nth 1 (vl-msb-constint-bitlist x warnings))))
1263
 
    :hints(("Goal" :in-theory (disable (force)))))
1264
 
 
1265
 
  (defthm true-listp-of-vl-msb-constint-bitlist-1
1266
 
    (implies (true-listp warnings)
1267
 
             (true-listp (mv-nth 1 (vl-msb-constint-bitlist x warnings))))
1268
 
    :rule-classes :type-prescription
1269
 
    :hints(("Goal" :in-theory (disable (force)))))
1270
 
 
1271
 
  (local (defthm vl-emodwirelist-p-of-make-list-ac
1272
 
           (implies (and (vl-emodwirelist-p ac)
1273
 
                         (vl-emodwire-p val))
1274
 
                    (vl-emodwirelist-p (make-list-ac n val ac)))))
1275
 
 
1276
 
  (defthm vl-emodwirelist-p-of-vl-msb-constint-bitlist
1277
 
    (vl-emodwirelist-p (mv-nth 2 (vl-msb-constint-bitlist x warnings)))
1278
 
    :hints(("Goal" :in-theory (disable (force))))))
1279
 
 
1280
 
 
1281
 
 
1282
 
(defsection vl-msb-wire-bitlist
 
974
                   (test-ok 10 128 (list f f   t f f f   f f f f))))))))
 
975
 
 
976
 
 
977
 
 
978
(define vl-msb-wire-bitlist
1283
979
  :parents (vl-msb-expr-bitlist)
1284
980
  :short "Produce the @(see vl-emodwire-p)s for a @(see vl-id-p)."
1285
981
 
1286
 
  :long "<p><b>Signature:</b> @(call vl-msb-wire-bitlist) returns @('(mv
1287
 
successp warnings bits)').</p>
1288
 
 
1289
 
<p>We are given an atomic, identifier expression.  This expression has some
1290
 
width and refers to a particular wire.  We return a wires associated with this
1291
 
name in MSB order.</p>"
1292
 
 
1293
 
  (defund vl-msb-wire-bitlist (x walist warnings)
1294
 
    (declare (xargs :guard (and (vl-expr-p x)
1295
 
                                (vl-atom-p x)
1296
 
                                (vl-wirealist-p walist)
1297
 
                                (vl-id-p (vl-atom->guts x))
1298
 
                                (vl-warninglist-p warnings))))
1299
 
    (b* ((width (vl-atom->finalwidth x))
1300
 
         (guts  (vl-atom->guts x))
1301
 
         (name  (vl-id->name guts))
1302
 
 
1303
 
         ((unless (posp width))
1304
 
          (b* ((w (make-vl-warning
1305
 
                   :type :vl-programming-error
 
982
  ((x        vl-expr-p)
 
983
   (walist   vl-wirealist-p)
 
984
   (warnings vl-warninglist-p))
 
985
  :guard (and (vl-atom-p x)
 
986
              (vl-id-p (vl-atom->guts x)))
 
987
  :returns (mv (successp booleanp :rule-classes :type-prescription)
 
988
               (warnings vl-warninglist-p)
 
989
               (bits     vl-emodwirelist-p))
 
990
  :long "<p>We are given an atomic, identifier expression.  This expression has
 
991
some width and refers to a particular wire.  We return a wires associated with
 
992
this name in MSB order.</p>"
 
993
 
 
994
  (b* ((width (vl-atom->finalwidth x))
 
995
       (guts  (vl-atom->guts x))
 
996
       (name  (vl-id->name guts))
 
997
 
 
998
       ((unless (posp width))
 
999
        (mv nil
 
1000
            (fatal :type :vl-programming-error
1306
1001
                   :msg "Expected only sized expressions, but ~a0 does not ~
1307
1002
                         have a finalwidth."
1308
 
                   :args (list x)
1309
 
                   :fatalp t
1310
 
                   :fn 'vl-msb-wire-bitlist)))
1311
 
            (mv nil (cons w warnings) nil)))
1312
 
 
1313
 
         (wires (mbe :logic (list-fix (cdr (hons-get name walist)))
1314
 
                     :exec  (cdr (hons-get name walist))))
1315
 
 
1316
 
         ((unless (consp wires))
1317
 
          (b* ((w (make-vl-warning
1318
 
                   :type :vl-bad-id
 
1003
                   :args (list x))
 
1004
            nil))
 
1005
 
 
1006
       (wires (mbe :logic (list-fix (cdr (hons-get name walist)))
 
1007
                   :exec  (cdr (hons-get name walist))))
 
1008
 
 
1009
       ((unless (and (consp wires)
 
1010
                     (mbt (vl-emodwirelist-p wires))))
 
1011
        (mv nil
 
1012
            (fatal :type :vl-bad-id
1319
1013
                   :msg "No wires for ~a0."
1320
 
                   :args (list name)
1321
 
                   :fatalp t
1322
 
                   :fn 'vl-msb-wire-bitlist)))
1323
 
            (mv nil (cons w warnings) nil)))
1324
 
 
1325
 
         (nwires (length wires))
1326
 
 
1327
 
         ((when (< width nwires))
1328
 
          (b* ((w (make-vl-warning
1329
 
                   :type :vl-programming-error
 
1014
                   :args (list name))
 
1015
            nil))
 
1016
 
 
1017
       (nwires (length wires))
 
1018
 
 
1019
       ((when (< width nwires))
 
1020
        (mv nil
 
1021
            (fatal :type :vl-programming-error
1330
1022
                   :msg "Produced too many wires for ~a0.  Finalwidth is ~x1, ~
1331
1023
                         but produced ~x2 bits: ~x3."
1332
 
                   :args (list x (vl-atom->finalwidth x) nwires wires)
1333
 
                   :fatalp t
1334
 
                   :fn 'vl-msb-wire-bitlist)))
1335
 
            (mv nil (cons w warnings) nil)))
1336
 
 
1337
 
         ((when (= nwires width))
1338
 
          (mv t warnings wires))
1339
 
 
1340
 
         ;; else, we need to implicitly zero-extend or sign-extend the wire
1341
 
         ;; based on its type; @(see vl-atom-welltyped-p).
1342
 
 
1343
 
         (type          (vl-atom->finaltype x))
1344
 
         (extension-bit (if (eq type :vl-signed)
1345
 
                            (car wires)
1346
 
                          'acl2::f))
1347
 
         (wires (append (replicate (- width nwires) extension-bit) wires)))
1348
 
 
1349
 
      (mv t warnings wires)))
1350
 
 
1351
 
  (local (in-theory (enable vl-msb-wire-bitlist)))
1352
 
 
1353
 
  (defmvtypes vl-msb-wire-bitlist (booleanp nil true-listp))
1354
 
 
1355
 
  (defthm true-listp-of-vl-msb-wire-bitlist-1
1356
 
    (implies (true-listp warnings)
1357
 
             (true-listp (mv-nth 1 (vl-msb-wire-bitlist x walist warnings))))
1358
 
    :rule-classes :type-prescription)
1359
 
 
1360
 
  (defthm vl-warninglist-p-of-vl-msb-wire-bitlist
1361
 
    (implies (force (vl-warninglist-p warnings))
1362
 
             (vl-warninglist-p (mv-nth 1 (vl-msb-wire-bitlist x walist warnings))))
1363
 
    :hints(("Goal" :in-theory (disable (force)))))
1364
 
 
1365
 
  (defthm vl-emodwirelist-p-of-vl-msb-wire-bitlist
1366
 
    (implies (force (vl-wirealist-p walist))
1367
 
             (vl-emodwirelist-p (mv-nth 2 (vl-msb-wire-bitlist x walist warnings))))))
1368
 
 
1369
 
 
1370
 
 
1371
 
(defsection vl-msb-partselect-bitlist
 
1024
                   :args (list x (vl-atom->finalwidth x) nwires wires))
 
1025
            nil))
 
1026
 
 
1027
       ((when (eql nwires width))
 
1028
        (mv t (ok) wires))
 
1029
 
 
1030
       ;; else, we need to implicitly zero-extend or sign-extend the wire
 
1031
       ;; based on its type; @(see vl-atom-welltyped-p).
 
1032
 
 
1033
       (type          (vl-atom->finaltype x))
 
1034
       (extension-bit (if (eq type :vl-signed)
 
1035
                          (car wires)
 
1036
                        'acl2::f))
 
1037
       (wires (append (replicate (- width nwires) extension-bit) wires)))
 
1038
 
 
1039
    (mv t (ok) wires))
 
1040
 
 
1041
  ///
 
1042
  (more-returns
 
1043
   (bits true-listp :rule-classes :type-prescription)))
 
1044
 
 
1045
 
 
1046
 
 
1047
(define vl-msb-partselect-bitlist
1372
1048
  :parents (vl-msb-expr-bitlist)
1373
1049
  :short "Produce the @(see vl-emodwire-p)s for a part-select."
1374
1050
 
1375
 
  :long "<p><b>Signature:</b> @(call vl-msb-partselect-bitlist) returns @('(mv
1376
 
successp warnings bits)').</p>
1377
 
 
1378
 
<p>We are given an part-select expression, @('x'), a wire alist, @('walist'),
1379
 
and an @(see warnings) accumulator, @('warnings').  accumulator.  We attempt to
1380
 
return the list of wires that correspond to this part select, in MSB order.  We
1381
 
are careful to ensure that the range is resolved, the indices are in bounds,
1382
 
and so on.</p>"
1383
 
 
1384
 
  (local (in-theory (enable hons-assoc-equal)))
1385
 
 
1386
 
  (defund vl-msb-partselect-bitlist (x walist warnings)
1387
 
    (declare (xargs :guard (and (vl-expr-p x)
1388
 
                                (not (vl-atom-p x))
1389
 
                                (equal (vl-nonatom->op x) :vl-partselect-colon)
1390
 
                                (vl-wirealist-p walist)
1391
 
                                (vl-warninglist-p warnings))))
1392
 
    (b* ((args  (vl-nonatom->args x))
1393
 
         (from  (first args))
1394
 
         (left  (second args))
1395
 
         (right (third args))
1396
 
 
1397
 
         ((unless (and (vl-idexpr-p from)
1398
 
                       (vl-expr-resolved-p left)
1399
 
                       (vl-expr-resolved-p right)))
1400
 
          (b* ((w (make-vl-warning
1401
 
                   :type :vl-bad-expr
 
1051
  ((x        vl-expr-p)
 
1052
   (walist   vl-wirealist-p)
 
1053
   (warnings vl-warninglist-p))
 
1054
  :guard (and (not (vl-atom-p x))
 
1055
              (equal (vl-nonatom->op x) :vl-partselect-colon))
 
1056
  :returns (mv (successp booleanp :rule-classes :type-prescription)
 
1057
               (warnings vl-warninglist-p)
 
1058
               (bits     vl-emodwirelist-p))
 
1059
  :long "<p>We attempt to return the list of wires that correspond to this part
 
1060
select, in MSB order.  We are careful to ensure that the range is resolved, the
 
1061
indices are in bounds, and so on.</p>"
 
1062
 
 
1063
  :prepwork ((local (in-theory (enable hons-assoc-equal))))
 
1064
 
 
1065
  (b* ((args  (vl-nonatom->args x))
 
1066
       (from  (first args))
 
1067
       (left  (second args))
 
1068
       (right (third args))
 
1069
 
 
1070
       ((unless (and (vl-idexpr-p from)
 
1071
                     (vl-expr-resolved-p left)
 
1072
                     (vl-expr-resolved-p right)))
 
1073
        (mv nil
 
1074
            (fatal :type :vl-bad-expr
1402
1075
                   :msg "Expected a simple name and resolved indices, but ~
1403
1076
                         found ~a0."
1404
 
                   :args (list x)
1405
 
                   :fatalp t
1406
 
                   :fn 'vl-msb-partselect-bitlist)))
1407
 
            (mv nil (cons w warnings) nil)))
1408
 
 
1409
 
         (name  (vl-idexpr->name from))
1410
 
         (left  (vl-resolved->val left))
1411
 
         (right (vl-resolved->val right))
1412
 
 
1413
 
         (entry (hons-get name walist))
1414
 
         ((unless entry)
1415
 
          (b* ((w (make-vl-warning
1416
 
                   :type :vl-bad-expr
 
1077
                   :args (list x))
 
1078
            nil))
 
1079
 
 
1080
       (name  (vl-idexpr->name from))
 
1081
       (left  (vl-resolved->val left))
 
1082
       (right (vl-resolved->val right))
 
1083
 
 
1084
       (entry (hons-get name walist))
 
1085
       ((unless entry)
 
1086
        (mv nil
 
1087
            (fatal :type :vl-bad-expr
1417
1088
                   :msg "No wire-alist entry for ~w0."
1418
 
                   :args (list name)
1419
 
                   :fatalp t
1420
 
                   :fn 'vl-msb-partselect-bitlist)))
1421
 
            (mv nil (cons w warnings) nil)))
1422
 
 
1423
 
         (wires (mbe :logic (list-fix (cdr entry))
1424
 
                     :exec  (cdr entry)))
1425
 
 
1426
 
         (plain-name (vl-plain-wire-name name))
1427
 
 
1428
 
         ((when (equal wires (list plain-name)))
1429
 
 
1430
 
; Special case.  This is a select of a single, non-ranged wire.  The only valid
1431
 
; possibility is that high and low are both zero, in which case we are choosing
1432
 
; name[0:0] which is the same as name.
1433
 
 
1434
 
          (if (and (= left 0) (= right 0))
1435
 
 
1436
 
; BOZO probably we should not be doing this.  But I suspect things will break
1437
 
; if we just remove this, so for now just add a non-fatal warning.  Hrmn, but
1438
 
; what about the scalared and vectored keywords?  Ugh.
1439
 
 
1440
 
; If you fix this consider also the similar thing happening for bit-selects,
1441
 
; and also fix the vl-expr-allwires function.
1442
 
 
1443
 
              (mv t
1444
 
                  (cons (make-vl-warning
1445
 
                         :type :vl-select-from-scalar
1446
 
                         :msg "~a0: permitting selecting bit 0 from a scalar ~
1447
 
                               wire, but this is probably wrong."
1448
 
                         :args (list x)
1449
 
                         :fatalp nil
1450
 
                         :fn 'vl-msb-partselect-bitlist)
1451
 
                      warnings)
1452
 
                  wires)
1453
 
 
1454
 
            (mv nil
1455
 
                (cons (make-vl-warning
1456
 
                       :type :vl-bad-expr
1457
 
                       :msg "~w0 is a lone wire, but found ~a1."
1458
 
                       :args (list name x)
1459
 
                       :fatalp t
1460
 
                       :fn 'vl-msb-partselect-bitlist)
1461
 
                      warnings)
1462
 
                nil)))
1463
 
 
1464
 
; Otherwise, this is the ordinary case, and we are selecting some part of some
1465
 
; ranged wire.  Since the wires in the walist are contiguous, we can check that
1466
 
; the whole part is in bound by merely checking that both indices are found.
1467
 
 
1468
 
         (name[left]     (make-vl-emodwire :basename name :index left))
1469
 
         (name[right]    (make-vl-emodwire :basename name :index right))
1470
 
         ((unless (and (member name[left] wires)
1471
 
                       (member name[right] wires)))
1472
 
          (b* ((w (make-vl-warning
1473
 
                   :type :vl-bad-expr
1474
 
                   :msg "Select ~a0 is out of range; valid range is from ~
1475
 
                         ~x1 to ~x2."
1476
 
                   :args (list x (car wires) (car (last wires)))
1477
 
                   :fatalp t
1478
 
                   :fn 'vl-msb-partselect-bitlist)))
1479
 
            (mv nil (cons w warnings) nil))))
1480
 
 
1481
 
; We're fine.  It seems easiest to just re-intern the symbols instead of
1482
 
; extracting the appropriate slice out of the wire alist.
1483
 
 
1484
 
        (mv t warnings (vl-emodwires-from-msb-to-lsb name left right))))
1485
 
 
1486
 
  (local (in-theory (enable vl-msb-partselect-bitlist)))
1487
 
 
1488
 
  (defmvtypes vl-msb-partselect-bitlist (booleanp nil true-listp))
1489
 
 
1490
 
  (defthm true-listp-of-vl-msb-partselect-bitlist-1
1491
 
    (implies (true-listp warnings)
1492
 
             (true-listp (mv-nth 1 (vl-msb-partselect-bitlist x walist warnings))))
1493
 
    :rule-classes :type-prescription)
1494
 
 
1495
 
  (defthm vl-warninglist-p-of-vl-msb-partselect-bitlist
1496
 
    (implies (force (vl-warninglist-p warnings))
1497
 
             (vl-warninglist-p
1498
 
              (mv-nth 1 (vl-msb-partselect-bitlist x walist warnings)))))
1499
 
 
1500
 
  (defthm vl-emodwirelist-p-of-vl-msb-partselect-bitlist
1501
 
    (vl-emodwirelist-p (mv-nth 2 (vl-msb-partselect-bitlist x walist warnings)))))
1502
 
 
1503
 
 
1504
 
 
1505
 
(defsection vl-msb-bitselect-bitlist
 
1089
                   :args (list name))
 
1090
            nil))
 
1091
 
 
1092
       (wires (mbe :logic (list-fix (cdr entry))
 
1093
                   :exec  (cdr entry)))
 
1094
 
 
1095
       (plain-name (vl-plain-wire-name name))
 
1096
 
 
1097
       ((when (equal wires (list plain-name)))
 
1098
        ;; Special case.  This is a select of a single, non-ranged wire.  The
 
1099
        ;; only valid possibility is that high and low are both zero, in which
 
1100
        ;; case we are choosing name[0:0] which is the same as name.
 
1101
        (if (and (eql left 0)
 
1102
                 (eql right 0))
 
1103
            ;; BOZO probably we should not be doing this.  But I suspect things
 
1104
            ;; will break if we just remove this, so for now just add a
 
1105
            ;; non-fatal warning.  Hrmn, but what about the scalared and
 
1106
            ;; vectored keywords?  Ugh.  If you fix this consider also the
 
1107
            ;; similar thing happening for bit-selects, and also fix the
 
1108
            ;; vl-expr-allwires function.
 
1109
            (mv t
 
1110
                (warn :type :vl-select-from-scalar
 
1111
                      :msg "~a0: permitting selecting bit 0 from a scalar ~
 
1112
                            wire, but this is probably wrong."
 
1113
                      :args (list x))
 
1114
                wires)
 
1115
 
 
1116
          (mv nil
 
1117
              (fatal :type :vl-bad-expr
 
1118
                     :msg "~w0 is a lone wire, but found ~a1."
 
1119
                     :args (list name x))
 
1120
              nil)))
 
1121
 
 
1122
       ;; Otherwise, this is the ordinary case, and we are selecting some part
 
1123
       ;; of some ranged wire.  Since the wires in the walist are contiguous,
 
1124
       ;; we can check that the whole part is in bound by merely checking that
 
1125
       ;; both indices are found.
 
1126
       (name[left]     (make-vl-emodwire :basename name :index left))
 
1127
       (name[right]    (make-vl-emodwire :basename name :index right))
 
1128
       ((unless (and (member name[left] wires)
 
1129
                     (member name[right] wires)))
 
1130
        (mv nil
 
1131
            (fatal :type :vl-bad-expr
 
1132
                   :msg "Select ~a0 is out of range; valid range is from ~x1 ~
 
1133
                         to ~x2."
 
1134
                   :args (list x (car wires) (car (last wires))))
 
1135
            nil)))
 
1136
 
 
1137
    ;; We're fine.  It seems easiest to just re-intern the symbols instead of
 
1138
    ;; extracting the appropriate slice out of the wire alist.
 
1139
    (mv t (ok) (vl-emodwires-from-msb-to-lsb name left right)))
 
1140
 
 
1141
  ///
 
1142
  (more-returns
 
1143
   (bits true-listp :rule-classes :type-prescription)))
 
1144
 
 
1145
 
 
1146
 
 
1147
(define vl-msb-bitselect-bitlist
1506
1148
  :parents (vl-msb-expr-bitlist)
1507
1149
  :short "Produce the @(see vl-emodwire-p)s for a bit-select."
1508
 
 
1509
 
  :long "<p><b>Signature:</b> @(call vl-msb-bitselect-bitlist) returns @('(mv
1510
 
successp warnings bits)').</p>
1511
 
 
1512
 
<p>We are given an bit-select expression, @('x'), a wire alist, @('walist'),
1513
 
and an @(see warnings) accumulator, @('warnings').  accumulator.  We attempt to
1514
 
return the list of wires that correspond to this bit select.  In practice this
1515
 
will be a singleton wire, or nil on failure.  We are careful to ensure that the
1516
 
selected bit is in bounds, etc.</p>"
1517
 
 
1518
 
  (local (in-theory (enable hons-assoc-equal)))
1519
 
 
1520
 
  (defund vl-msb-bitselect-bitlist (x walist warnings)
1521
 
    (declare (xargs :guard (and (vl-expr-p x)
1522
 
                                (not (vl-atom-p x))
1523
 
                                (equal (vl-nonatom->op x) :vl-bitselect)
1524
 
                                (vl-wirealist-p walist)
1525
 
                                (vl-warninglist-p warnings))))
1526
 
    (b* ((args  (vl-nonatom->args x))
1527
 
         (from  (first args))
1528
 
         (index (second args))
1529
 
 
1530
 
         ((unless (and (vl-idexpr-p from)
1531
 
                       (vl-expr-resolved-p index)
1532
 
                       (natp (vl-resolved->val index))))
1533
 
          (mv nil
1534
 
              (cons (make-vl-warning
1535
 
                     :type :vl-bad-expr
1536
 
                     :msg "Expected a simple name and resolved index, but ~
1537
 
                           found a0."
1538
 
                     :args (list x)
1539
 
                     :fatalp t
1540
 
                     :fn 'vl-msb-bitselect-bitlist)
1541
 
                    warnings)
1542
 
              nil))
1543
 
 
1544
 
         (name  (vl-idexpr->name from))
1545
 
         (index (vl-resolved->val index))
1546
 
         (entry (hons-get name walist))
1547
 
 
1548
 
         ((unless entry)
1549
 
          (mv nil
1550
 
              (cons (make-vl-warning
1551
 
                     :type :vl-bad-expr
1552
 
                     :msg "No wire-alist entry for ~w0."
1553
 
                     :args (list name)
1554
 
                     :fatalp t
1555
 
                     :fn 'vl-msb-bitselect-bitlist)
1556
 
                    warnings)
1557
 
              nil))
1558
 
 
1559
 
         (wires (mbe :logic (list-fix (cdr entry))
1560
 
                     :exec (cdr entry)))
1561
 
         (plain-name (vl-plain-wire-name name))
1562
 
 
1563
 
         ((when (equal wires (list plain-name)))
1564
 
 
1565
 
; Special case.  This is a select of a single, non-ranged wire.  The only valid
1566
 
; possibility is that the index is zero, in which case we are choosing name[0],
1567
 
; which is the same as name.  BOZO think about this again.  Should maybe warn here.
1568
 
 
1569
 
          (if (= index 0)
1570
 
              (mv t warnings wires)
1571
 
            (mv nil
1572
 
                (cons (make-vl-warning
1573
 
                       :type :vl-bad-expr
1574
 
                       :msg "~w0 is a lone wire, but found ~a1."
1575
 
                       :args (list name x)
1576
 
                       :fatalp t
1577
 
                       :fn 'vl-msb-bitselect-bitlist)
1578
 
                      warnings)
1579
 
                nil)))
1580
 
 
1581
 
; Ordinary case.  We are selecting from some wire with a range.  Figure out
1582
 
; what wire we want, and make sure it exists.
1583
 
 
1584
 
         (name[i] (make-vl-emodwire :basename name :index index))
1585
 
         ((unless (member name[i] wires))
1586
 
          (mv nil
1587
 
              (cons (make-vl-warning
1588
 
                     :type :vl-bad-expr
1589
 
                     :msg "Select ~a0 is out of range: the valid bits are ~
1590
 
                           ~s1 through ~s2."
1591
 
                     :args (list x (car wires) (car (last wires)))
1592
 
                     :fatalp t
1593
 
                     :fn 'vl-msb-bitselect-bitlist)
1594
 
                    warnings)
 
1150
  ((x        vl-expr-p)
 
1151
   (walist   vl-wirealist-p)
 
1152
   (warnings vl-warninglist-p))
 
1153
  :guard (and (not (vl-atom-p x))
 
1154
              (equal (vl-nonatom->op x) :vl-bitselect))
 
1155
  :returns (mv (successp booleanp :rule-classes :type-prescription)
 
1156
               (warnings vl-warninglist-p)
 
1157
               (bits     vl-emodwirelist-p))
 
1158
  :long "<p>We attempt to return the list of wires that correspond to this bit
 
1159
select.  In practice this will be a singleton wire, or nil on failure.  We are
 
1160
careful to ensure that the selected bit is in bounds, etc.</p>"
 
1161
 
 
1162
  :prepwork ((local (in-theory (enable hons-assoc-equal))))
 
1163
 
 
1164
  (b* ((args  (vl-nonatom->args x))
 
1165
       (from  (first args))
 
1166
       (index (second args))
 
1167
 
 
1168
       ((unless (and (vl-idexpr-p from)
 
1169
                     (vl-expr-resolved-p index)
 
1170
                     (natp (vl-resolved->val index))))
 
1171
        (mv nil
 
1172
            (fatal :type :vl-bad-expr
 
1173
                   :msg "Expected a simple name and resolved index, but found ~
 
1174
                         a0."
 
1175
                   :args (list x))
 
1176
            nil))
 
1177
 
 
1178
       (name  (vl-idexpr->name from))
 
1179
       (index (vl-resolved->val index))
 
1180
       (entry (hons-get name walist))
 
1181
 
 
1182
       ((unless entry)
 
1183
        (mv nil
 
1184
            (fatal :type :vl-bad-expr
 
1185
                   :msg "No wire-alist entry for ~w0."
 
1186
                   :args (list name))
 
1187
            nil))
 
1188
 
 
1189
       (wires (mbe :logic (list-fix (cdr entry))
 
1190
                   :exec (cdr entry)))
 
1191
       (plain-name (vl-plain-wire-name name))
 
1192
 
 
1193
       ((when (equal wires (list plain-name)))
 
1194
        ;; Special case.  This is a select of a single, non-ranged wire.  The
 
1195
        ;; only valid possibility is that the index is zero, in which case we
 
1196
        ;; are choosing name[0], which is the same as name.  BOZO think about
 
1197
        ;; this again.  Should maybe warn here.
 
1198
        (if (eql index 0)
 
1199
            (mv t (ok) wires)
 
1200
          (mv nil
 
1201
              (fatal :type :vl-bad-expr
 
1202
                     :msg "~w0 is a lone wire, but found ~a1."
 
1203
                     :args (list name x))
1595
1204
              nil)))
1596
 
 
1597
 
        (mv t warnings (list name[i]))))
1598
 
 
1599
 
  (local (in-theory (enable vl-msb-bitselect-bitlist)))
1600
 
 
1601
 
  (defmvtypes vl-msb-bitselect-bitlist (booleanp nil true-listp))
1602
 
 
1603
 
  (defthm true-listp-of-vl-msb-bitselect-bitlist-1
1604
 
    (implies (true-listp warnings)
1605
 
             (true-listp (mv-nth 1 (vl-msb-bitselect-bitlist x walist warnings))))
1606
 
    :rule-classes :type-prescription)
1607
 
 
1608
 
  (defthm vl-warninglist-p-of-vl-msb-bitselect-bitlist
1609
 
    (implies (force (vl-warninglist-p warnings))
1610
 
             (vl-warninglist-p
1611
 
              (mv-nth 1 (vl-msb-bitselect-bitlist x walist warnings)))))
1612
 
 
1613
 
  (defthm vl-emodwirelist-p-of-vl-msb-bitselect-bitlist
1614
 
    (vl-emodwirelist-p (mv-nth 2 (vl-msb-bitselect-bitlist x walist warnings)))))
1615
 
 
1616
 
 
1617
 
 
1618
 
(defsection vl-msb-replicate-bitlist
 
1205
       ;; Ordinary case.  We are selecting from some wire with a range.  Figure
 
1206
       ;; out what wire we want, and make sure it exists.
 
1207
       (name[i] (make-vl-emodwire :basename name :index index))
 
1208
       ((unless (member name[i] wires))
 
1209
        (mv nil
 
1210
            (fatal :type :vl-bad-expr
 
1211
                   :msg "Select ~a0 is out of range: the valid bits are ~s1 ~
 
1212
                         through ~s2."
 
1213
                   :args (list x (car wires) (car (last wires))))
 
1214
            nil)))
 
1215
 
 
1216
    (mv t (ok) (list name[i])))
 
1217
  ///
 
1218
  (more-returns
 
1219
   (bits true-listp :rule-classes :type-prescription)))
 
1220
 
 
1221
 
 
1222
 
 
1223
(define vl-msb-replicate-bitlist
1619
1224
  :parents (vl-msb-expr-bitlist)
1620
1225
  :short "@(call vl-msb-replicate-bitlist) appends @('bits') onto itself
1621
1226
repeatedly, making @('n') copies of @('bits') as a single list."
1622
 
 
1623
 
    :long "<p>This is used for multiple concatenations, e.g., @('{4
 
1227
  ((n    natp)
 
1228
   (bits true-listp))
 
1229
  :long "<p>This is used for multiple concatenations, e.g., @('{4
1624
1230
{a,b,c}}').</p>"
1625
1231
 
1626
 
  (defund vl-msb-replicate-bitlist (n bits)
1627
 
    (declare (xargs :guard (and (natp n)
1628
 
                                (true-listp bits))))
1629
 
    (if (zp n)
1630
 
        nil
1631
 
      (append bits (vl-msb-replicate-bitlist (- n 1) bits))))
1632
 
 
1633
 
  (local (in-theory (enable vl-msb-replicate-bitlist)))
1634
 
 
 
1232
  (if (zp n)
 
1233
      nil
 
1234
    (append bits (vl-msb-replicate-bitlist (- n 1) bits)))
 
1235
  ///
1635
1236
  (defthm true-listp-of-vl-msb-replicate-bitlist
1636
1237
    (true-listp (vl-msb-replicate-bitlist n bits))
1637
1238
    :rule-classes :type-prescription)
1658
1259
                    (list t t f  t t f  t t f)))))))
1659
1260
 
1660
1261
 
1661
 
 
1662
 
(defsection vl-msb-expr-bitlist
 
1262
(defines vl-msb-expr-bitlist
1663
1263
  :parents (vl-wirealist-p)
1664
1264
  :short "Produce the E-language, MSB-ordered list of bits for an expression."
1665
1265
 
1666
 
  :long "<p><b>Signature:</b> @(call vl-msb-expr-bitlist) returns @('(mv
1667
 
successp warnings bitlist)')</p>
1668
 
 
1669
 
<p>When we translate module and gate instances into E, the arguments of the
1670
 
instance are Verilog expressions, and we need to convert them into E-language
1671
 
patterns.  By the end of our simplification process, we think that each such
1672
 
expression should contain only:</p>
 
1266
  :long "<p>When we translate module and gate instances into E, the arguments
 
1267
of the instance are Verilog expressions, and we need to convert them into
 
1268
E-language patterns.  By the end of our simplification process, we think that
 
1269
each such expression should contain only:</p>
1673
1270
 
1674
1271
<ul>
1675
1272
 <li>Constant integers</li>
1682
1279
 
1683
1280
<p>This routine is intended to convert arbitrary expressions that include only
1684
1281
the above forms into a list of <b>MSB order</b> bits.</p>"
1685
 
 
1686
 
  (mutual-recursion
1687
 
 
1688
 
   (defund vl-msb-expr-bitlist (x walist warnings)
1689
 
     (declare (xargs :guard (and (vl-expr-p x)
1690
 
                                 (vl-wirealist-p walist)
1691
 
                                 (vl-warninglist-p warnings))
1692
 
                     :verify-guards nil
1693
 
                     :hints(("Goal" :in-theory (disable (force))))
1694
 
                     :measure (vl-expr-count x)))
1695
 
 
1696
 
     (if (vl-fast-atom-p x)
1697
 
         (let ((guts (vl-atom->guts x)))
1698
 
           (case (tag guts)
1699
 
             (:vl-constint (vl-msb-constint-bitlist x warnings))
1700
 
             (:vl-id       (vl-msb-wire-bitlist x walist warnings))
1701
 
             (otherwise
1702
 
              (mv nil
1703
 
                  (cons (make-vl-warning :type :vl-unimplemented
1704
 
                                         :msg "Need to add support for ~x0."
1705
 
                                         :args (list (tag guts))
1706
 
                                         :fatalp t
1707
 
                                         :fn 'vl-msb-expr-bitlist)
1708
 
                        warnings)
1709
 
                  nil))))
1710
 
 
1711
 
       (let* ((op   (vl-nonatom->op x))
1712
 
              (args (vl-nonatom->args x)))
1713
 
         (case op
1714
 
           ;; BOZO add additional length checks to the end of these
1715
 
           ;; functions.
1716
 
           (:vl-bitselect
1717
 
            (vl-msb-bitselect-bitlist x walist warnings))
1718
 
           (:vl-partselect-colon
1719
 
            (vl-msb-partselect-bitlist x walist warnings))
1720
 
           (:vl-concat
1721
 
            (vl-msb-exprlist-bitlist args walist warnings))
1722
 
           (:vl-multiconcat
1723
 
            (b* (((unless (mbt (consp args)))
1724
 
                  (prog2$
1725
 
                   (er hard 'vl-msb-expr-bitlist
1726
 
                       "Impossible case for termination")
1727
 
                   (mv nil warnings nil)))
1728
 
 
1729
 
                 (mult   (first args))
1730
 
                 (concat (second args))
1731
 
 
1732
 
                 ((unless (and (vl-expr-resolved-p mult)
1733
 
                               (natp (vl-resolved->val mult))))
1734
 
                  (mv nil
1735
 
                      (cons (make-vl-warning
1736
 
                             :type :vl-bad-expr
1737
 
                             :msg "Multiple concatenation with unresolved multiplicity: ~a0."
1738
 
                             :args (list x)
1739
 
                             :fatalp t
1740
 
                             :fn 'vl-msb-expr-bitlist)
1741
 
                            warnings)
1742
 
                      nil))
1743
 
 
1744
 
                 ((mv successp warnings bits)
1745
 
                  (vl-msb-expr-bitlist concat walist warnings))
1746
 
 
1747
 
                 ((unless successp)
1748
 
                  (mv successp warnings bits))
1749
 
 
1750
 
                 (replbits
1751
 
                  (vl-msb-replicate-bitlist (vl-resolved->val mult) bits)))
1752
 
 
1753
 
              (mv t warnings replbits)))
1754
 
           (otherwise
1755
 
            (mv nil
1756
 
                (cons (make-vl-warning :type :vl-unsupported
1757
 
                                       :msg "Unsupported operator ~x0."
1758
 
                                       :args (list op)
1759
 
                                       :fatalp t
1760
 
                                       :fn 'vl-msb-expr-bitlist)
1761
 
                      warnings)
1762
 
                nil))))))
1763
 
 
1764
 
   (defund vl-msb-exprlist-bitlist (x walist warnings)
1765
 
     (declare (xargs :guard (and (vl-exprlist-p x)
1766
 
                                 (vl-wirealist-p walist)
1767
 
                                 (vl-warninglist-p warnings))
1768
 
                     :measure (vl-exprlist-count x)))
1769
 
     (if (atom x)
1770
 
         (mv t warnings nil)
1771
 
       (b* (((mv car-successp warnings car-bits)
1772
 
             (vl-msb-expr-bitlist (car x) walist warnings))
1773
 
            ((mv cdr-successp warnings cdr-bits)
1774
 
             (vl-msb-exprlist-bitlist (cdr x) walist warnings)))
1775
 
         (mv (and car-successp cdr-successp)
1776
 
             warnings
1777
 
             (append car-bits cdr-bits))))))
1778
 
 
1779
 
  (FLAG::make-flag vl-flag-msb-expr-bitlist
1780
 
                   vl-msb-expr-bitlist
1781
 
                   :flag-mapping ((vl-msb-expr-bitlist . expr)
1782
 
                                  (vl-msb-exprlist-bitlist . list)))
1783
 
 
1784
 
  (defthm-vl-flag-msb-expr-bitlist
1785
 
    (defthm true-listp-of-vl-msb-expr-bitlist-1
1786
 
      (implies (true-listp warnings)
1787
 
               (true-listp (mv-nth 1 (vl-msb-expr-bitlist x walist warnings))))
1788
 
      :rule-classes :type-prescription
1789
 
      :flag expr)
1790
 
    (defthm true-listp-of-vl-msb-exprlist-bitlist-1
1791
 
      (implies (true-listp warnings)
1792
 
               (true-listp (mv-nth 1 (vl-msb-exprlist-bitlist x walist warnings))))
1793
 
      :rule-classes :type-prescription
1794
 
      :flag list)
1795
 
    :hints(("Goal"
1796
 
            :expand ((vl-msb-expr-bitlist x walist warnings)
1797
 
                     (vl-msb-exprlist-bitlist x walist warnings)))))
1798
 
 
1799
 
  (defthm-vl-flag-msb-expr-bitlist
 
1282
  :verify-guards nil
 
1283
 
 
1284
  (define vl-msb-expr-bitlist ((x        vl-expr-p)
 
1285
                               (walist   vl-wirealist-p)
 
1286
                               (warnings vl-warninglist-p))
 
1287
    :measure (vl-expr-count x)
 
1288
    :returns (mv (successp booleanp :rule-classes :type-prescription)
 
1289
                 (warnings vl-warninglist-p)
 
1290
                 (bits     vl-emodwirelist-p))
 
1291
    :flag :expr
 
1292
 
 
1293
    (b* (((when (vl-fast-atom-p x))
 
1294
          (let ((guts (vl-atom->guts x)))
 
1295
            (case (tag guts)
 
1296
              (:vl-constint (vl-msb-constint-bitlist x warnings))
 
1297
              (:vl-id       (vl-msb-wire-bitlist x walist warnings))
 
1298
              (otherwise
 
1299
               (mv nil
 
1300
                   (fatal :type :vl-unimplemented
 
1301
                          :msg "Need to add support for ~x0."
 
1302
                          :args (list (tag guts)))
 
1303
                   nil)))))
 
1304
 
 
1305
         (op   (vl-nonatom->op x))
 
1306
         (args (vl-nonatom->args x))
 
1307
         ;; BOZO add additional length checks to the end of these functions.
 
1308
         ((when (eq op :vl-bitselect))
 
1309
          (vl-msb-bitselect-bitlist x walist warnings))
 
1310
         ((when (eq op :vl-partselect-colon))
 
1311
          (vl-msb-partselect-bitlist x walist warnings))
 
1312
         ((when (eq op :vl-concat))
 
1313
          (vl-msb-exprlist-bitlist args walist warnings))
 
1314
         ((when (eq op :vl-multiconcat))
 
1315
          (b* ((mult   (first args))
 
1316
               (concat (second args))
 
1317
               ((unless (and (vl-expr-resolved-p mult)
 
1318
                             (natp (vl-resolved->val mult))))
 
1319
                (mv nil
 
1320
                    (fatal :type :vl-bad-expr
 
1321
                           :msg "Multiple concatenation with unresolved multiplicity: ~a0."
 
1322
                           :args (list x))
 
1323
                    nil))
 
1324
               ((mv successp warnings bits)
 
1325
                (vl-msb-expr-bitlist concat walist warnings))
 
1326
               ((unless successp)
 
1327
                ;; Already warned
 
1328
                (mv successp warnings bits))
 
1329
               (replbits
 
1330
                (vl-msb-replicate-bitlist (vl-resolved->val mult) bits)))
 
1331
            (mv t (ok) replbits))))
 
1332
      (mv nil
 
1333
          (fatal :type :vl-unsupported
 
1334
                 :msg "Unsupported operator ~x0."
 
1335
                 :args (list op))
 
1336
          nil)))
 
1337
 
 
1338
   (define vl-msb-exprlist-bitlist ((x        vl-exprlist-p)
 
1339
                                    (walist   vl-wirealist-p)
 
1340
                                    (warnings vl-warninglist-p))
 
1341
     :measure (vl-exprlist-count x)
 
1342
     :returns (mv (successp booleanp :rule-classes :type-prescription)
 
1343
                  (warnings vl-warninglist-p)
 
1344
                  (bits     vl-emodwirelist-p))
 
1345
     :flag :list
 
1346
     (b* (((when (atom x))
 
1347
           (mv t (ok) nil))
 
1348
          ((mv car-successp warnings car-bits)
 
1349
           (vl-msb-expr-bitlist (car x) walist warnings))
 
1350
          ((mv cdr-successp warnings cdr-bits)
 
1351
           (vl-msb-exprlist-bitlist (cdr x) walist warnings)))
 
1352
       (mv (and car-successp cdr-successp)
 
1353
           warnings
 
1354
           (append car-bits cdr-bits))))
 
1355
 
 
1356
   ///
 
1357
 
 
1358
   (defthm-vl-msb-expr-bitlist-flag
1800
1359
    (defthm true-listp-of-vl-msb-expr-bitlist-2
1801
1360
      (true-listp (mv-nth 2 (vl-msb-expr-bitlist x walist warnings)))
1802
1361
      :rule-classes :type-prescription
1803
 
      :flag expr)
 
1362
      :flag :expr)
1804
1363
    (defthm true-listp-of-vl-msb-exprlist-bitlist-2
1805
1364
      (true-listp (mv-nth 2 (vl-msb-exprlist-bitlist x walist warnings)))
1806
1365
      :rule-classes :type-prescription
1807
 
      :flag list)
1808
 
    :hints(("Goal"
1809
 
            :expand ((vl-msb-expr-bitlist x walist warnings)
1810
 
                     (vl-msb-exprlist-bitlist x walist warnings)))))
1811
 
 
1812
 
  (defthm-vl-flag-msb-expr-bitlist
1813
 
    (defthm vl-emodwirelist-p-of-vl-msb-expr-bitlist
1814
 
      (implies (force (vl-wirealist-p walist))
1815
 
               (vl-emodwirelist-p (mv-nth 2 (vl-msb-expr-bitlist x walist warnings))))
1816
 
      :flag expr)
1817
 
    (defthm symbol-listp-of-vl-msb-exprlist-bitlist
1818
 
      (implies (force (vl-wirealist-p walist))
1819
 
               (vl-emodwirelist-p (mv-nth 2 (vl-msb-exprlist-bitlist x walist warnings))))
1820
 
      :flag list)
1821
 
    :hints(("Goal"
1822
 
            :expand ((vl-msb-expr-bitlist x walist warnings)
1823
 
                     (vl-msb-exprlist-bitlist x walist warnings)))))
1824
 
 
1825
 
  (defthm-vl-flag-msb-expr-bitlist
1826
 
    (defthm vl-warninglist-p-of-vl-msb-expr-bitlist
1827
 
      (implies (force (vl-warninglist-p warnings))
1828
 
               (vl-warninglist-p (mv-nth 1 (vl-msb-expr-bitlist x walist warnings))))
1829
 
      :flag expr)
1830
 
    (defthm vl-warninglist-p-of-vl-msb-exprlist-bitlist
1831
 
      (implies (force (vl-warninglist-p warnings))
1832
 
               (vl-warninglist-p (mv-nth 1 (vl-msb-exprlist-bitlist x walist warnings))))
1833
 
      :flag list)
1834
 
    :hints(("Goal"
1835
 
            :expand ((vl-msb-expr-bitlist x walist warnings)
1836
 
                     (vl-msb-exprlist-bitlist x walist warnings)))))
1837
 
 
1838
 
  (verify-guards vl-msb-expr-bitlist))
 
1366
      :flag :list))
 
1367
 
 
1368
   (verify-guards vl-msb-expr-bitlist))
1839
1369
 
1840
1370