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

module Spartan6.Primitive.IO where

open import Spartan6.Prelude
open import Spartan6.Evidence

-- Official source: UG615 v14.7 (2013-10-02).
--
-- * IBUF: printed pages 109-110, one-bit I input and O output.
-- * OBUF: printed pages 216-217, a constantly driven one-bit output buffer.
-- * OBUFDS: printed page 218, logic table O=I and OB=not I.
-- * OBUFT: printed pages 220-221, logic table: T=0 transfers I, T=1
--   disables the driver and produces high impedance.
--
-- I/O standards, voltage, current, drive strength, slew, and pad electrical
-- behavior are outside this digital model.

ug615IO : PinnedSource
ug615IO = pinSource UG615 (revision "v14.7" (just "2013-10-02"))

ibuf : Bit → Bit
ibuf input = input

obuf : Bit → Bit
obuf input = input

record DifferentialOutput : Type₀ where
  constructor differentialOutput
  field
    positive : Bit
    negative : Bit

open DifferentialOutput public

obufds : Bit → DifferentialOutput
obufds input = differentialOutput input (not input)

-- High impedance is kept distinct from Bit.  No multi-driver resolution is
-- performed, so this type is a boundary drive contract rather than a net
-- value with invented Boolean behavior.

data OutputDrive : Type₀ where
  driven        : Bit → OutputDrive
  highImpedance : OutputDrive

obuft : Bit → Bit → OutputDrive
obuft input false = driven input
obuft input true = highImpedance

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

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

obufds-low : obufds low ≡ differentialOutput low high
obufds-low = refl

obufds-high : obufds high ≡ differentialOutput high low
obufds-high = refl

obuft-enabled : ∀ input → obuft input low ≡ driven input
obuft-enabled input = refl

obuft-disabled : ∀ input → obuft input high ≡ highImpedance
obuft-disabled input = refl