• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
    • Gl
    • Esim
      • Symbolic-test-vectors
      • Esim-primitives
      • E-conversion
        • Vl-ealist-p
        • Modinsts-to-eoccs
        • Vl-module-make-esim
        • Exploding-vectors
          • Vl-wirealist-p
          • Emodwire-encoding
          • Vl-emodwire-p
          • Vl-emodwirelistlist
          • Vl-emodwirelist
        • Resolving-multiple-drivers
        • Vl-modulelist-make-esims
        • Vl-module-check-e-ok
        • Vl-collect-design-wires
        • Adding-z-drivers
        • Vl-design-to-e
        • Vl-design-to-e-check-ports
        • Vl-design-to-e-main
        • Port-bit-checking
      • Esim-steps
      • Patterns
      • Mod-internal-paths
      • Defmodules
      • Esim-simplify-update-fns
      • Esim-tutorial
      • Esim-vl
    • Vl2014
    • Sv
    • Vwsim
    • Fgl
    • Vl
    • X86isa
    • Svl
    • Rtl
  • Software-verification
  • Testing-utilities
  • Math

• Exploding-vectors

Emodwire-encoding

A simple encoding scheme to basenames that are free of certain special characters.

Usually Verilog wire names do not have special characters in them, but with escaped identifiers it is possible to have names that include brackets, dots, etc.

These special characters could pose certain problems. The most obvious is in a module such as this:

wire [7:0] w ;
wire w[3] ;

Here, the E wires corresponding to w would be ACL2::|w[7]| on down to ACL2::|w[0]|. But if we naively translate w[3] into ACL2::|w[3]| then there could be a name clash.

To avoid this kind of problem, we use a simple encoding scheme that ensures there are no brackets in the basename of a vl-emodwire-p. We originally used the following, trivial encoding scheme:

• [ ---> {1
• ] ---> {2
• { ---> {3

But later we decided to slightly extend this scheme, to ensure that the special characters ., !, and / also do not occur. Why? We think having . in a name could be confusing to some tools since it is used as a hierarchical identifier in Verilog. Meanwhile, ! is used as a hierarchical identifier in E (e.g., see mod-state). And we have occasionally seen other Verilog tools that use / as a hierarchical separator.

To ensure these characters also do not occur, we extend our encoding scheme in a simple way:

• . ---> {4
• ! ---> {5
• / ---> {6

This encoding is done automatically by the vl-emodwire constructor and the appropriate decoding is done by the vl-emodwire->basename accessor. Usually no encoding is necessary, so these functions are optimized for the case that there are no bracket or { characters.

Note that we actually implement the encoding and decoding functions in raw-lisp for better performance.

Definitions and Theorems

Function: vl-emodwire-encode-chars

(defun vl-emodwire-encode-chars (x)
       (declare (xargs :guard (character-listp x)))
       (if (atom x)
           nil
           (let ((rest (vl-emodwire-encode-chars (cdr x))))
                (case (car x)
                      (#\[ (list* #\{ #\1 rest))
                      (#\] (list* #\{ #\2 rest))
                      (#\{ (list* #\{ #\3 rest))
                      (#\. (list* #\{ #\4 rest))
                      (#\! (list* #\{ #\5 rest))
                      (#\/ (list* #\{ #\6 rest))
                      (otherwise (cons (car x) rest))))))

Theorem: character-listp-of-vl-emodwire-encode-chars

(defthm character-listp-of-vl-emodwire-encode-chars
        (implies (force (character-listp x))
                 (character-listp (vl-emodwire-encode-chars x))))

Theorem: no-special-chars-in-vl-emodwire-encode-chars

(defthm no-special-chars-in-vl-emodwire-encode-chars
        (and (not (member-equal #\[ (vl-emodwire-encode-chars x)))
             (not (member-equal #\] (vl-emodwire-encode-chars x)))
             (not (member-equal #\. (vl-emodwire-encode-chars x)))
             (not (member-equal #\! (vl-emodwire-encode-chars x)))
             (not (member-equal #\/ (vl-emodwire-encode-chars x)))))

Theorem: vl-emodwire-encode-chars-identity

(defthm vl-emodwire-encode-chars-identity
        (implies (and (not (member-equal #\[ x))
                      (not (member-equal #\] x))
                      (not (member-equal #\{ x))
                      (not (member-equal #\. x))
                      (not (member-equal #\! x))
                      (not (member-equal #\/ x)))
                 (equal (vl-emodwire-encode-chars x)
                        (list-fix x))))

Function: vl-emodwire-encoding-valid-p

(defun vl-emodwire-encoding-valid-p (x)
       (declare (xargs :guard (character-listp x)))
       (cond ((atom x) t)
             ((eql (car x) #\{)
              (and (consp (cdr x))
                   (or (eql (cadr x) #\1)
                       (eql (cadr x) #\2)
                       (eql (cadr x) #\3)
                       (eql (cadr x) #\4)
                       (eql (cadr x) #\5)
                       (eql (cadr x) #\6))
                   (vl-emodwire-encoding-valid-p (cddr x))))
             (t (vl-emodwire-encoding-valid-p (cdr x)))))

Theorem: vl-emodwire-encoding-valid-p-of-vl-emodwire-encode-chars

(defthm vl-emodwire-encoding-valid-p-of-vl-emodwire-encode-chars
        (vl-emodwire-encoding-valid-p (vl-emodwire-encode-chars x)))

Theorem: vl-emodwire-encoding-valid-p-typical

(defthm vl-emodwire-encoding-valid-p-typical
        (implies (not (member-equal #\{ x))
                 (vl-emodwire-encoding-valid-p x)))

Theorem: vl-emodwire-encoding-valid-p-of-append

(defthm vl-emodwire-encoding-valid-p-of-append
        (implies (and (force (vl-emodwire-encoding-valid-p x))
                      (force (vl-emodwire-encoding-valid-p y)))
                 (vl-emodwire-encoding-valid-p (append x y))))

Function: vl-emodwire-decode-chars

(defun vl-emodwire-decode-chars (x)
       (declare (xargs :guard (character-listp x)))
       (cond ((atom x) nil)
             ((and (eql (car x) #\{) (consp (cdr x)))
              (let ((rest (vl-emodwire-decode-chars (cddr x))))
                   (case (cadr x)
                         (#\1 (cons #\[ rest))
                         (#\2 (cons #\] rest))
                         (#\3 (cons #\{ rest))
                         (#\4 (cons #\. rest))
                         (#\5 (cons #\! rest))
                         (otherwise (cons #\/ rest)))))
             (t (cons (car x)
                      (vl-emodwire-decode-chars (cdr x))))))

Theorem: vl-emodwire-decode-chars-under-iff

(defthm vl-emodwire-decode-chars-under-iff
        (iff (vl-emodwire-decode-chars x)
             (consp x)))

Theorem: character-listp-of-vl-emodwire-decode-chars

(defthm character-listp-of-vl-emodwire-decode-chars
        (implies (force (character-listp x))
                 (character-listp (vl-emodwire-decode-chars x))))

Theorem: vl-emodwire-decode-chars-of-vl-emodwire-encode-chars

(defthm
 vl-emodwire-decode-chars-of-vl-emodwire-encode-chars
 (implies
      (force (character-listp x))
      (equal (vl-emodwire-decode-chars (vl-emodwire-encode-chars x))
             (list-fix x))))

Theorem: vl-emodwire-decode-chars-identity

(defthm vl-emodwire-decode-chars-identity
        (implies (case-split (not (member-equal #\{ x)))
                 (equal (vl-emodwire-decode-chars x)
                        (list-fix x))))

Theorem: equal-of-vl-emodwire-decode-chars

(defthm equal-of-vl-emodwire-decode-chars
        (implies (and (vl-emodwire-encoding-valid-p x)
                      (vl-emodwire-encoding-valid-p y)
                      (not (member-equal #\[ x))
                      (not (member-equal #\] x))
                      (not (member-equal #\. x))
                      (not (member-equal #\! x))
                      (not (member-equal #\/ x))
                      (not (member-equal #\[ y))
                      (not (member-equal #\] y))
                      (not (member-equal #\. y))
                      (not (member-equal #\! y))
                      (not (member-equal #\/ y)))
                 (equal (equal (vl-emodwire-decode-chars x)
                               (vl-emodwire-decode-chars y))
                        (equal (list-fix x) (list-fix y)))))

Function: vl-emodwire-encode-aux

(defun vl-emodwire-encode-aux (x)
       (declare (type string x))
       (b* ((chars (explode x))
            (encoded (vl-emodwire-encode-chars chars)))
           (implode encoded)))

Function: vl-emodwire-decode-aux

(defun vl-emodwire-decode-aux (x)
       (declare (type string x))
       (b* ((chars (explode x))
            (decoded (vl-emodwire-decode-chars chars)))
           (implode decoded)))

Function: vl-emodwire-encode

(defun vl-emodwire-encode (x)
       (declare (type string x))
       (mbe :logic (vl-emodwire-encode-aux x)
            :exec (if (or (position #\[ (the string x))
                          (position #\] (the string x))
                          (position #\{ (the string x))
                          (position #\. (the string x))
                          (position #\! (the string x))
                          (position #\/ (the string x)))
                      (vl-emodwire-encode-aux x)
                      x)))

Function: vl-emodwire-decode

(defun vl-emodwire-decode (x)
       (declare (type string x))
       (mbe :logic (vl-emodwire-decode-aux x)
            :exec (if (position #\{ x)
                      (vl-emodwire-decode-aux x)
                      x)))