|
|
|---|
|
|
|
|---|
Definitions of commonly used constants and some functions to
convert between
Definitions of constants (of the form
(define nWp (x) (unsigned-byte-p W x))
(define nW ((x integerp)) (mbe :logic (loghead W x) :exec (logand 2^W-1 x)))
(define iWp (x) (signed-byte-p W x))
(define iW ((x integerp)) (logext W x))
(define nW-to-iW ((x nWp :type (unsigned-byte W))) (mbe :logic (logext W x) :exec (if (< x 2^(W-1)) x (- x 2^W))))
(define iW-to-Nw ((x iWp :type (signed-byte W))) (mbe :logic (loghead W x) :exec (if (>= x 0) x (+ x 2^W))))
The function