3
(set-enforce-redundancy t)
5
(local (include-book "../support/support/openers"))
9
; In this file, an event-control (evctl) data structure is either (posedge
10
; clk), (negedge clk), or (even n).
12
(defun negate-event-control (evctl)
13
(if (equal evctl '(even n))
15
(let* ((edge0 (car evctl))
21
(er hard 'gen-model-preamble-common
22
"Unable to handle edge specifier ~x0."
24
`(not (,edge (,clk (1- n)) (,clk n))))))
26
(defun negate-event-control-list (x)
27
(declare (xargs :guard (true-listp x)))
30
(cons (negate-event-control (car x))
31
(negate-event-control-list (cdr x)))))
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)
40
`(defthm ,(intern-in-package-of-symbol
41
(concatenate 'string (symbol-name name) "$OPEN")
43
(implies (and (integerp n)
45
,@(negate-event-control-list evctl-lst))
50
,@(and (eq type :wire) `((,name (1- n)))))))))))