{-# OPTIONS --safe --cubical #-}

module Spartan6.Primitive.Clock where

open import Spartan6.Prelude
open import Spartan6.Semantics.Design using (Event; idle; risingEdge)

-- UG615 v14.7, printed pages 53-54, documents BUFG as a one-input,
-- one-output global clock buffer.  Printed page 55 gives the BUFGCE logic
-- table: CE=0 forces O low and CE=1 transfers I.  The functions below retain
-- only that untimed digital rule; skew, glitches, routing, and physical clock
-- quality are not represented.

bufg : Bit → Bit
bufg input = input

bufgce : Bit → Bit → Bit
bufgce input enable = mux enable low input

transportEvent : Event → Event
transportEvent event = event

gateEvent : Bit → Event → Event
gateEvent enable idle = idle
gateEvent false risingEdge = idle
gateEvent true risingEdge = risingEdge

bufg-transports : ∀ input → bufg input ≡ input
bufg-transports input = refl

bufgce-disabled : ∀ input → bufgce input low ≡ low
bufgce-disabled input = refl

bufgce-enabled : ∀ input → bufgce input high ≡ input
bufgce-enabled input = refl

disabled-rising-edge-is-suppressed : gateEvent low risingEdge ≡ idle
disabled-rising-edge-is-suppressed = refl

enabled-rising-edge-is-transported : gateEvent high risingEdge ≡ risingEdge
enabled-rising-edge-is-transported = refl