		Search-engine friendly clone of the ACL2 documentation.

Debug.lisp

Svtv-debug-init

Prepares an SV design for SVTV debugging, to the extent possible without specifying an SVTV.

Signature
(svtv-debug-init design &key (moddb 'moddb) (aliases 'aliases) (debugdata 'debugdata)) → (mv err moddb-out aliases-out debugdata-out)
Arguments: design — Guard (design-p design).

This does the initial compilation of the design, creating the moddb, aliases table, and local wire assignments and delays. See svtv-debug-set-svtv for the next step, which composes the signals into their nextstate and update functions given a timing diagram.

Technical: Erases and recreates the moddb, aliases, and debugdata stobjs.

Definitions and Theorems

Function: svtv-debug-init-fn

(defun svtv-debug-init-fn (design moddb aliases debugdata)
 (declare (xargs :stobjs (moddb aliases debugdata)))
 (declare (xargs :guard (design-p design)))
 (declare
  (xargs
       :guard
       (svarlist-addr-p (modalist-vars (design->modalist design)))))
 (let ((__function__ 'svtv-debug-init))
   (declare (ignorable __function__))
   (b* ((design (design-fix design))
        ((mv err assigns
             delays ?constraints moddb aliases)
         (svex-design-flatten-and-normalize design
                                            :indexedp nil))
        ((when err)
         (raise "~@0~%" err)
         (mv err moddb aliases debugdata))
        (modidx (moddb-modname-get-index (design->top design)
                                         moddb))
        (debugdata (set-debugdata->design design debugdata))
        (debugdata (set-debugdata->modidx modidx debugdata))
        (debugdata (set-debugdata->assigns assigns debugdata))
        (debugdata (set-debugdata->delays delays debugdata))
        (debugdata (set-debugdata->updates nil debugdata))
        (debugdata (set-debugdata->nextstates nil debugdata))
        (debugdata (set-debugdata->status :initialized debugdata)))
     (mv nil moddb aliases debugdata))))

Theorem: svtv-debug-init-moddb-ok

(defthm svtv-debug-init-moddb-ok
  (b* (((mv ?err
            ?moddb-out ?aliases-out ?debugdata-out)
        (svtv-debug-init-fn design moddb aliases debugdata)))
    (and (moddb-mods-ok moddb-out)
         (moddb-basics-ok moddb-out))))

Theorem: svtv-debug-init-modidx-ok

(defthm svtv-debug-init-modidx-ok
  (b* (((mv ?err
            ?moddb-out ?aliases-out ?debugdata-out)
        (svtv-debug-init-fn design moddb aliases debugdata)))
    (implies (not err)
             (< (nth *debugdata->modidx* debugdata-out)
                (nfix (nth *moddb->nmods1* moddb-out))))))

Theorem: svtv-debug-init-totalwires-ok

(defthm svtv-debug-init-totalwires-ok
 (b* (((mv ?err
           ?moddb-out ?aliases-out ?debugdata-out)
       (svtv-debug-init-fn design moddb aliases debugdata)))
  (implies
   (not err)
   (<= (moddb-mod-totalwires (nth *debugdata->modidx* debugdata-out)
                             moddb-out)
       (len aliases-out)))))

Theorem: svtv-debug-init-fn-of-design-fix-design

(defthm svtv-debug-init-fn-of-design-fix-design
  (equal (svtv-debug-init-fn (design-fix design)
                             moddb aliases debugdata)
         (svtv-debug-init-fn design moddb aliases debugdata)))

Theorem: svtv-debug-init-fn-design-equiv-congruence-on-design

(defthm svtv-debug-init-fn-design-equiv-congruence-on-design
 (implies
  (design-equiv design design-equiv)
  (equal (svtv-debug-init-fn design moddb aliases debugdata)
         (svtv-debug-init-fn design-equiv moddb aliases debugdata)))
 :rule-classes :congruence)

Theorem: svtv-debug-init-fn-of-moddb-fix-moddb

(defthm svtv-debug-init-fn-of-moddb-fix-moddb
  (equal (svtv-debug-init-fn design (moddb-fix moddb)
                             aliases debugdata)
         (svtv-debug-init-fn design moddb aliases debugdata)))

Theorem: svtv-debug-init-fn-moddb-equiv-congruence-on-moddb

(defthm svtv-debug-init-fn-moddb-equiv-congruence-on-moddb
 (implies
  (moddb-equiv moddb moddb-equiv)
  (equal (svtv-debug-init-fn design moddb aliases debugdata)
         (svtv-debug-init-fn design moddb-equiv aliases debugdata)))
 :rule-classes :congruence)

Theorem: svtv-debug-init-fn-of-lhslist-fix-aliases

(defthm svtv-debug-init-fn-of-lhslist-fix-aliases
  (equal (svtv-debug-init-fn design moddb (lhslist-fix aliases)
                             debugdata)
         (svtv-debug-init-fn design moddb aliases debugdata)))

Theorem: svtv-debug-init-fn-lhslist-equiv-congruence-on-aliases

(defthm svtv-debug-init-fn-lhslist-equiv-congruence-on-aliases
 (implies
  (lhslist-equiv aliases aliases-equiv)
  (equal (svtv-debug-init-fn design moddb aliases debugdata)
         (svtv-debug-init-fn design moddb aliases-equiv debugdata)))
 :rule-classes :congruence)