← Back to branch summary

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

« back to all changes in this revision

Viewing changes to books/centaur/vl/loader/parser/tests/eventctrl.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/loader/parser/tests/eventctrl.lisp
32
32
(include-book "base")
33
33
(include-book "../eventctrl")
34
34
 
35
 
(assert!
36
 
 (b* ((tokens (make-test-tokens "@(foo or bar or baz)"))
37
 
      (warnings 'blah-warnings)
38
 
      (config   *vl-default-loadconfig*)
39
 
      ((mv err val tokens warnings)
40
 
       (vl-parse-delay-or-event-control)))
41
 
   (and (not err)
42
 
        (not tokens)
43
 
        (equal warnings 'blah-warnings)
44
 
        (equal val (make-vl-eventcontrol
45
 
                    :starp nil
46
 
                    :atoms
47
 
                    (list (make-vl-evatom
48
 
                           :type :vl-noedge
49
 
                           :expr (make-vl-atom :guts (vl-id "foo")))
50
 
                          (make-vl-evatom
51
 
                           :type :vl-noedge
52
 
                           :expr (make-vl-atom :guts (vl-id "bar")))
53
 
                          (make-vl-evatom
54
 
                           :type :vl-noedge
55
 
                           :expr (make-vl-atom :guts (vl-id "baz")))))))))
56
 
 
57
 
(assert!
58
 
 (b* ((tokens (make-test-tokens "@(posedge foo)"))
59
 
      (warnings 'blah-warnings)
60
 
      (config   *vl-default-loadconfig*)
61
 
      ((mv err val tokens warnings)
62
 
       (vl-parse-delay-or-event-control)))
63
 
   (and (not err)
64
 
        (not tokens)
65
 
        (equal warnings 'blah-warnings)
66
 
        (equal val (make-vl-eventcontrol
67
 
                    :starp nil
68
 
                    :atoms (list (make-vl-evatom
69
 
                                  :type :vl-posedge
70
 
                                  :expr (make-vl-atom :guts (vl-id "foo")))))))))
71
 
 
72
 
(assert!
73
 
 (b* ((tokens   (make-test-tokens "@(negedge foo)"))
74
 
      (warnings 'blah-warnings)
75
 
      (config   *vl-default-loadconfig*)
76
 
      ((mv err val tokens warnings)
77
 
       (vl-parse-delay-or-event-control)))
78
 
   (and (not err)
79
 
        (not tokens)
80
 
        (equal warnings 'blah-warnings)
81
 
        (equal val (make-vl-eventcontrol
82
 
                    :starp nil
83
 
                    :atoms (list (make-vl-evatom
84
 
                                  :type :vl-negedge
85
 
                                  :expr (make-vl-atom :guts (vl-id "foo")))))))))
86
 
 
87
 
(assert! (b* ((tokens   (make-test-tokens "@*"))
88
 
              (warnings 'blah-warnings)
89
 
              (config   *vl-default-loadconfig*)
90
 
              ((mv err val tokens warnings)
91
 
               (vl-parse-delay-or-event-control)))
92
 
           (and (not err)
93
 
                (not tokens)
94
 
                (equal warnings 'blah-warnings)
95
 
                (equal val (make-vl-eventcontrol
96
 
                            :starp t
97
 
                            :atoms nil)))))
98
 
 
99
 
(assert! (b* ((tokens   (make-test-tokens "@(*)"))
100
 
              (warnings 'blah-warnings)
101
 
              (config   *vl-default-loadconfig*)
102
 
              ((mv err val tokens warnings)
103
 
               (vl-parse-delay-or-event-control)))
104
 
           (and (not err)
105
 
                (not tokens)
106
 
                (equal warnings 'blah-warnings)
107
 
                (equal val (make-vl-eventcontrol
108
 
                            :starp t
109
 
                            :atoms nil)))))
110
 
 
111
 
(assert! (b* (((mv err val tokens warnings)
112
 
               (vl-parse-delay-or-event-control
113
 
                :tokens (make-test-tokens "@( *)")
114
 
                :warnings 'blah-warnings
115
 
                :config *vl-default-loadconfig*)))
116
 
           (and (not err)
117
 
                (not tokens)
118
 
                (equal warnings 'blah-warnings)
119
 
                (equal val (make-vl-eventcontrol
120
 
                            :starp t
121
 
                            :atoms nil)))))
122
 
 
123
 
(assert! (b* (((mv err val tokens warnings)
124
 
               (vl-parse-delay-or-event-control
125
 
                :tokens (make-test-tokens "@(* )")
126
 
                :warnings 'blah-warnings
127
 
                :config *vl-default-loadconfig*)))
128
 
           (and (not err)
129
 
                (not tokens)
130
 
                (equal warnings 'blah-warnings)
131
 
                (equal val (make-vl-eventcontrol
132
 
                            :starp t
133
 
                            :atoms nil)))))
134
 
 
135
 
(assert! (b* (((mv err val tokens warnings)
136
 
               (vl-parse-delay-or-event-control
137
 
                :tokens (make-test-tokens "@( * )")
138
 
                :warnings 'blah-warnings
139
 
                :config *vl-default-loadconfig*)))
140
 
           (and (not err)
141
 
                (not tokens)
142
 
                (equal warnings 'blah-warnings)
143
 
                (equal val (make-vl-eventcontrol
144
 
                            :starp t
145
 
                            :atoms nil)))))
146
 
 
 
35
(defparser-top vl-parse-delay-or-event-control)
 
36
 
 
37
(defmacro test-vl-parse-delay-or-eventcontrol (&key input expect (successp 't))
 
38
  `(assert!
 
39
    (b* ((tokens (make-test-tokens ,input))
 
40
         (pstate (make-vl-parsestate :warnings 'blah-warnings))
 
41
         (config *vl-default-loadconfig*)
 
42
         ((mv err val tokens (vl-parsestate pstate))
 
43
          (vl-parse-delay-or-event-control-top))
 
44
         ((when err)
 
45
          (not ,successp)))
 
46
      (debuggable-and ,successp
 
47
                      (not tokens)
 
48
                      (equal pstate.warnings 'blah-warnings)
 
49
                      (equal val ,expect)))))
 
50
 
 
51
(test-vl-parse-delay-or-eventcontrol :input "@(foo or bar or baz)"
 
52
                                     :expect
 
53
                                     (make-vl-eventcontrol
 
54
                                      :starp nil
 
55
                                      :atoms
 
56
                                      (list (make-vl-evatom
 
57
                                             :type :vl-noedge
 
58
                                             :expr (make-vl-atom :guts (vl-id "foo")))
 
59
                                            (make-vl-evatom
 
60
                                             :type :vl-noedge
 
61
                                             :expr (make-vl-atom :guts (vl-id "bar")))
 
62
                                            (make-vl-evatom
 
63
                                             :type :vl-noedge
 
64
                                             :expr (make-vl-atom :guts (vl-id "baz"))))))
 
65
 
 
66
(test-vl-parse-delay-or-eventcontrol :input "@(posedge foo)"
 
67
                                     :expect
 
68
                                     (make-vl-eventcontrol
 
69
                                      :starp nil
 
70
                                      :atoms (list (make-vl-evatom
 
71
                                                    :type :vl-posedge
 
72
                                                    :expr (make-vl-atom :guts (vl-id "foo"))))))
 
73
 
 
74
(test-vl-parse-delay-or-eventcontrol :input "@(negedge foo)"
 
75
                                     :expect
 
76
                                     (make-vl-eventcontrol
 
77
                                      :starp nil
 
78
                                      :atoms (list (make-vl-evatom
 
79
                                                    :type :vl-negedge
 
80
                                                    :expr (make-vl-atom :guts (vl-id "foo"))))))
 
81
 
 
82
(test-vl-parse-delay-or-eventcontrol :input "@*"
 
83
                                     :expect (make-vl-eventcontrol :starp t :atoms nil))
 
84
 
 
85
(test-vl-parse-delay-or-eventcontrol :input "@(*)"
 
86
                                     :expect (make-vl-eventcontrol :starp t :atoms nil))
 
87
 
 
88
(test-vl-parse-delay-or-eventcontrol :input "@( *)"
 
89
                                     :expect (make-vl-eventcontrol :starp t :atoms nil))
 
90
 
 
91
(test-vl-parse-delay-or-eventcontrol :input "@(* )"
 
92
                                     :expect (make-vl-eventcontrol :starp t :atoms nil))
 
93
 
 
94
(test-vl-parse-delay-or-eventcontrol :input "@( * )"
 
95
                                     :expect (make-vl-eventcontrol :starp t :atoms nil))
 
96
 
 
97
(test-vl-parse-delay-or-eventcontrol :input "@(foo or bar or baz or *)"
 
98
                                     :successp nil)
 
99
 
 
100
(test-vl-parse-delay-or-eventcontrol :input "@(foo or bar or)"
 
101
                                     :successp nil)
 
102
 
 
103
(test-vl-parse-delay-or-eventcontrol :input "@(* or foo)"
 
104
                                     :successp nil)
 
105
 
 
106
(test-vl-parse-delay-or-eventcontrol :input "@(foo or posedge bar)"
 
107
                                     :expect
 
108
                                     (make-vl-eventcontrol
 
109
                                      :starp nil
 
110
                                      :atoms (list (make-vl-evatom
 
111
                                                    :type :vl-noedge
 
112
                                                    :expr (make-vl-atom :guts (vl-id "foo")))
 
113
                                                   (make-vl-evatom
 
114
                                                    :type :vl-posedge
 
115
                                                    :expr (make-vl-atom :guts (vl-id "bar"))))))
 
116
 
 
117
(test-vl-parse-delay-or-eventcontrol :input "@(* or posedge bar)"
 
118
                                     :successp nil)
 
119
 
 
120
(test-vl-parse-delay-or-eventcontrol :input "@(posedge bar or *)"
 
121
                                     :successp nil)
 
122
 
 
123
(test-vl-parse-delay-or-eventcontrol :input "@(posedge bar or)"
 
124
                                     :successp nil)