		Search-engine friendly clone of the ACL2 documentation.

Vector-simulation

Aignet-vecsim-top

Logically same as aignet-vecsim, but optimizes by calling aignet-vecsim1 when s32v has only 1 column

Signature
(aignet-vecsim-top s32v aignet) → s32v

Definitions and Theorems

Function: aignet-vecsim-top

(defun aignet-vecsim-top (s32v aignet)
  (declare (xargs :stobjs (s32v aignet)))
  (declare (xargs :guard (<= (num-fanins aignet)
                             (s32v-nrows s32v))))
  (let ((__function__ 'aignet-vecsim-top))
    (declare (ignorable __function__))
    (mbe :logic (aignet-vecsim s32v aignet)
         :exec
         (if (eql (s32v-ncols s32v) 1)
             (aignet-vecsim1 s32v aignet)
           (aignet-vecsim s32v aignet)))))