Basic constructor macro for vl-clocking-direction-head structures.
(make-vl-clocking-direction-head [:inp <inp>] [:outp <outp>] [:iskew <iskew>] [:oskew <oskew>])
This is the usual way to construct vl-clocking-direction-head structures. It simply conses together a structure with the specified fields.
This macro generates a new vl-clocking-direction-head structure from scratch. See also change-vl-clocking-direction-head, which can "change" an existing structure, instead.
This is an ordinary
Macro:
(defmacro make-vl-clocking-direction-head (&rest args) (std::make-aggregate 'vl-clocking-direction-head args '((:inp) (:outp) (:iskew) (:oskew)) 'make-vl-clocking-direction-head nil))
Function:
(defun vl-clocking-direction-head (inp outp iskew oskew) (declare (xargs :guard (and (booleanp inp) (booleanp outp) (vl-maybe-clkskew-p iskew) (vl-maybe-clkskew-p oskew)))) (declare (xargs :guard t)) (let ((__function__ 'vl-clocking-direction-head)) (declare (ignorable __function__)) (b* ((inp (mbe :logic (acl2::bool-fix inp) :exec inp)) (outp (mbe :logic (acl2::bool-fix outp) :exec outp)) (iskew (mbe :logic (vl-maybe-clkskew-fix iskew) :exec iskew)) (oskew (mbe :logic (vl-maybe-clkskew-fix oskew) :exec oskew))) (cons :vl-clocking-direction-head (std::prod-cons (std::prod-cons inp outp) (std::prod-cons iskew oskew))))))