(vl-nedgeflop-clkedge-assigns edges clks dels) → assigns
Function:
(defun vl-nedgeflop-clkedge-assigns (edges clks dels) (declare (xargs :guard (and (vl-exprlist-p edges) (vl-exprlist-p clks) (vl-exprlist-p dels)))) (declare (xargs :guard (and (eql (len edges) (len clks)) (eql (len edges) (len dels))))) (let ((__function__ 'vl-nedgeflop-clkedge-assigns)) (declare (ignorable __function__)) (if (atom edges) nil (cons (make-vl-assign :lvalue (car edges) :expr (make-vl-nonatom :op :vl-binary-bitand :args (list (car clks) (make-vl-nonatom :op :vl-unary-bitnot :args (list (car dels)) :finalwidth 1 :finaltype :vl-unsigned)) :finalwidth 1 :finaltype :vl-unsigned) :loc *vl-fakeloc*) (vl-nedgeflop-clkedge-assigns (cdr edges) (cdr clks) (cdr dels))))))
Theorem:
(defthm vl-assignlist-p-of-vl-nedgeflop-clkedge-assigns (implies (and (vl-exprlist-p edges) (vl-exprlist-p clks) (vl-exprlist-p dels) (eql (len edges) (len clks)) (eql (len edges) (len dels))) (b* ((assigns (vl-nedgeflop-clkedge-assigns edges clks dels))) (vl-assignlist-p assigns))) :rule-classes :rewrite)