Match
(vl-lex-time-or-real-number echars breakp st) → (mv token? remainder)
Verilog-2005 has no
sign ::= + | - exp ::= e | E real_number ::= // no embedded spaces unsigned_number . unsigned_number | unsigned_number [ . unsigned_number ] exp [ sign ] unsigned_number
SystemVerilog-2012 slightly tweaks
real_number ::= // no embedded spaces fixed_point_number | unsigned_number [ . unsigned_number ] exp [ sign ] unsigned_number fixed_point_number ::= unsigned_number . unsigned_number
However, this new
time_literal ::= // no embedded spaces unsigned_number time_unit | fixed_point_number time_unit time_unit ::= s | ms | us | ns | ps | fs
And lexing these is slightly subtle because we now need to check for these
extra possibilities, e.g.,
Function:
(defun vl-lex-time-or-real-number (echars breakp st) (declare (xargs :guard (and (vl-echarlist-p echars) (booleanp breakp) (vl-lexstate-p st)))) (let ((__function__ 'vl-lex-time-or-real-number)) (declare (ignorable __function__)) (b* ((breakp (and breakp t)) ((mv ipart ipart-rest) (vl-read-unsigned-number echars)) ((unless ipart) (mv nil echars)) ((mv tail tail-rest) (vl-read-real-tail ipart-rest)) ((when tail) (mv (make-vl-realtoken :etext (append ipart tail) :breakp breakp) tail-rest)) ((vl-lexstate st) st) ((mv units units-rest) (if st.timelitsp (vl-read-time-unit ipart-rest) (mv nil ipart-rest))) ((when units) (mv (make-vl-timetoken :etext (append ipart units) :quantity (vl-echarlist->string ipart) :units (vl-timeunit-lookup (vl-echarlist->string units)) :breakp breakp) units-rest)) ((mv dot dot-rest) (vl-read-literal "." ipart-rest)) ((unless dot) (mv nil echars)) ((mv fpart fpart-rest) (vl-read-unsigned-number dot-rest)) ((unless fpart) (mv nil echars)) ((mv tail tail-rest) (vl-read-real-tail fpart-rest)) ((when tail) (mv (make-vl-realtoken :etext (append ipart dot fpart tail) :breakp breakp) tail-rest)) ((mv units units-rest) (if st.timelitsp (vl-read-time-unit fpart-rest) (mv nil fpart-rest))) ((when units) (mv (make-vl-timetoken :etext (append ipart dot fpart units) :quantity (vl-echarlist->string (append ipart dot fpart)) :units (vl-timeunit-lookup (vl-echarlist->string units)) :breakp breakp) units-rest))) (mv (make-vl-realtoken :etext (append ipart dot fpart) :breakp breakp) fpart-rest))))
Theorem:
(defthm vl-token-p-of-vl-lex-time-or-real-number (implies (and (force (vl-echarlist-p echars)) t) (equal (vl-token-p (mv-nth 0 (vl-lex-time-or-real-number echars breakp st))) (if (mv-nth 0 (vl-lex-time-or-real-number echars breakp st)) t nil))))
Theorem:
(defthm true-listp-of-vl-lex-time-or-real-number (equal (true-listp (mv-nth 1 (vl-lex-time-or-real-number echars breakp st))) (true-listp echars)) :rule-classes ((:rewrite) (:type-prescription :corollary (implies (true-listp echars) (true-listp (mv-nth 1 (vl-lex-time-or-real-number echars breakp st)))))))
Theorem:
(defthm vl-echarlist-p-of-vl-lex-time-or-real-number (implies (force (vl-echarlist-p echars)) (equal (vl-echarlist-p (mv-nth 1 (vl-lex-time-or-real-number echars breakp st))) t)))
Theorem:
(defthm append-of-vl-lex-time-or-real-number (implies (and (mv-nth 0 (vl-lex-time-or-real-number echars breakp st)) (force (vl-echarlist-p echars)) t) (equal (append (vl-token->etext (mv-nth 0 (vl-lex-time-or-real-number echars breakp st))) (mv-nth 1 (vl-lex-time-or-real-number echars breakp st))) echars)))
Theorem:
(defthm no-change-loser-of-vl-lex-time-or-real-number (implies (not (mv-nth 0 (vl-lex-time-or-real-number echars breakp st))) (equal (mv-nth 1 (vl-lex-time-or-real-number echars breakp st)) echars)))
Theorem:
(defthm acl2-count-of-vl-lex-time-or-real-number-weak (<= (acl2-count (mv-nth 1 (vl-lex-time-or-real-number echars breakp st))) (acl2-count echars)) :rule-classes ((:rewrite) (:linear)))
Theorem:
(defthm acl2-count-of-vl-lex-time-or-real-number-strong (implies (and (mv-nth 0 (vl-lex-time-or-real-number echars breakp st)) t) (< (acl2-count (mv-nth 1 (vl-lex-time-or-real-number echars breakp st))) (acl2-count echars))) :rule-classes ((:rewrite) (:linear)))