← Back to branch summary

~ubuntu-branches/ubuntu/gutsy/acl2/gutsy

« back to all changes in this revision

Viewing changes to books/rtl/rel6/support/lib1/openers.lisp

  • Committer: Bazaar Package Importer
  • Author(s): Camm Maguire
  • Date: 2006-12-04 10:35:42 UTC
  • mfrom: (1.1.5 upstream) (3.1.1 etch)
  • Revision ID: james.westby@ubuntu.com-20061204103542-68nf4pkilci0018n
Tags: 3.1-1
New upstream release

Show diffs side-by-side

added added

removed removed

Lines of Context:
books/rtl/rel6/support/lib1/openers.lisp
 
1
(in-package "ACL2")
 
2
 
 
3
(set-enforce-redundancy t)
 
4
 
 
5
(local (include-book "../support/openers"))
 
6
 
 
7
(program)
 
8
 
 
9
; In this file, an event-control (evctl) data structure is either (posedge
 
10
; clk), (negedge clk), or (even n).
 
11
 
 
12
(defun negate-event-control (evctl)
 
13
  (if (equal evctl '(even n))
 
14
      (list 'not evctl)
 
15
    (let* ((edge0 (car evctl))
 
16
           (clk (cadr evctl))
 
17
           (edge (case edge0
 
18
                   (posedge 'pedge)
 
19
                   (negedge 'nedge)
 
20
                   (otherwise
 
21
                    (er hard 'gen-model-preamble-common
 
22
                        "Unable to handle edge specifier ~x0."
 
23
                        edge0)))))
 
24
      `(not (,edge (,clk (1- n)) (,clk n))))))
 
25
 
 
26
(defun negate-event-control-list (x)
 
27
  (declare (xargs :guard (true-listp x)))
 
28
  (if (endp x)
 
29
      nil
 
30
    (cons (negate-event-control (car x))
 
31
          (negate-event-control-list (cdr x)))))
 
32
 
 
33
(defmacro def$open (name type &rest evctl-lst)
 
34
  (if (eq type :skipped)
 
35
      `(value-triple '(def$open ,name :skipped))
 
36
    (let ((evctl-lst (if (eq type :input)
 
37
                         (assert$ (null evctl-lst)
 
38
                                  '((even n)))
 
39
                       evctl-lst)))
 
40
      `(defthm ,(intern-in-package-of-symbol
 
41
                 (concatenate 'string (symbol-name name) "$OPEN")
 
42
                 name)
 
43
         (implies (and (integerp n)
 
44
                       (< 0 n)
 
45
                       ,@(negate-event-control-list evctl-lst))
 
46
                  (equal (,name n)
 
47
                         (,name (1- n))))
 
48
         :hints (("Goal"
 
49
                  :expand ((,name n)
 
50
                           ,@(and (eq type :wire) `((,name (1- n)))))))))))