support - ACL2 Book

other

(in-package "SV")

other

(include-book "xdoc/top" :dir :system)

other

(defxdoc sv-tutorial
  :parents (sv)
  :short "Basic tutorial: how to use the svex package to do datapath verification."
  :long " <p>The subtopics are listed in the intended order of the
tutorial, which first covers verification of a simple 16-bit combinational ALU
module, then a counter module to illustrate how to deal with state over time,
and finally a multiplier implementation to show how to structurally decompose
your proofs.</p>

<p>Note: A much higher level of detail is present in the comments of this book
than in the xdoc tutorial.  The xdoc tutorial is intended to give a high-level
idea of how to do it; to actually replicate it, you will likely want to look at
the sources.</p>

<p>To begin the ALU example, start at @(see translating-verilog-to-svex).</p>")

def-saved-eventmacro

(defmacro def-saved-event
  (name form)
  `(make-event (let* ((form ',SV::FORM))
      (value `(progn (table saved-forms-table ',',SV::NAME ',SV::FORM)
          ,SV::FORM)))))

def-saved-noneventmacro

(defmacro def-saved-nonevent
  (name form &key (return '?res) writep)
  (declare (ignorable return))
  `(make-event (b* ((form ',SV::FORM) (?res :ok)
        ,@(AND SV::WRITEP '((SV::STATE (SV::F-PUT-GLOBAL 'WRITES-OKP T SV::STATE))))
        ((er ?ans) (trans-eval-default-warning ',SV::FORM
            '(def-saved-nonevent ,SV::NAME)
            state
            t)))
      (value `(table saved-forms-table ',',SV::NAME ',SV::FORM)))))

deftutorialmacro

(defmacro deftutorial
  (name &rest args)
  (let ((parent (car (cadr (assoc-keyword :parents args)))))
    `(progn (local (table tutorial-ordering-table
          ',SV::PARENT
          (let* ((table (table-alist 'tutorial-ordering-table world)) (topics (cdr (assoc ',SV::PARENT table))))
            (cons ',SV::NAME topics))))
      (defxdoc ,SV::NAME . ,SV::ARGS))))

$macro

(defmacro $
  (name)
  `(cdr (assoc ',SV::NAME
      (table-alist 'saved-forms-table (w state)))))

recreate-saved-forms-tablefunction

(defun recreate-saved-forms-table
  (pairs)
  (if (atom pairs)
    nil
    (cons `(table saved-forms-table
        ',(CAAR SV::PAIRS)
        ',(CDAR SV::PAIRS))
      (recreate-saved-forms-table (cdr pairs)))))