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

module Spartan6.Primitive.Mux where

open import Spartan6.Prelude

-- Official functional evidence:
--
-- AMD/Xilinx, "Spartan-6 Libraries Guide for HDL Designs", UG615
-- v14.7, 2 October 2013:
-- https://docs.amd.com/v/u/en-US/spartan6_hdl
--
-- * MUXF7 entry and logic table: PDF page 204, printed page 204.
-- * MUXF8 entry and logic table: PDF page 210, printed page 210.
--
-- Both entries specify the same two-valued selection rule: a Low S selects
-- I0, and a High S selects I1.  The additional rows involving X lie outside
-- this project's Bit model.  Routing, placement, and timing claims from the
-- entries are intentionally not represented here.

muxF7 : Bit → Bit → Bit → Bit
muxF7 input0 input1 selector = mux selector input0 input1

muxF8 : Bit → Bit → Bit → Bit
muxF8 input0 input1 selector = mux selector input0 input1

muxF7-low : ∀ input0 input1 → muxF7 input0 input1 low ≡ input0
muxF7-low input0 input1 = refl

muxF7-high : ∀ input0 input1 → muxF7 input0 input1 high ≡ input1
muxF7-high input0 input1 = refl

muxF8-low : ∀ input0 input1 → muxF8 input0 input1 low ≡ input0
muxF8-low input0 input1 = refl

muxF8-high : ∀ input0 input1 → muxF8 input0 input1 high ≡ input1
muxF8-high input0 input1 = refl