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

module Spartan6.Primitive.SRL16E where

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

-- Source: UG615 v14.7, "SRL16E", printed pages 308-309.
--
-- Printed page 308 gives the address formula
--
--   length = 8 * A3 + 4 * A2 + 2 * A1 + A0 + 1,
--
-- states that the internal register is always 16 bits, and states that on a
-- low-to-high CLK transition with CE high, D enters the first bit while every
-- old bit moves to the next higher position.  With CE low, clock transitions
-- are ignored.  Its logic table records hold for CE=0 and the enabled rising
-- edge shift for CE=1.  Printed page 309 gives the one-bit Q, D, CLK, and CE
-- ports, the four-bit A address, and the 16-bit INIT attribute.

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

srl16eLocator : SourceLocator
srl16eLocator =
  locate srl16ePinnedSource "SRL16E"
    "printed pages 308-309: introduction, logic table, ports, and INIT attribute"

srl16eTrace : RuleTraceability
srl16eTrace =
  traceRule "primitive.SRL16E.two-valued"
            officialDocumentation
            (just srl16eLocator)
            partiallySupported
            guaranteed
            "Executable untimed state, address, hold, and enabled rising-edge shift semantics; raw INIT decoding and netlist admission are not provided here."

-- State is ordered from the first shift stage to the last shift stage.
-- Consequently index 0 is selected by A3A2A1A0=0000 and index 15 is selected
-- by A3A2A1A0=1111.

SRL16EState : Type₀
SRL16EState = Word 

record SRL16EAddress : Type₀ where
  constructor addressBits
  field
    a3 : Bit
    a2 : Bit
    a1 : Bit
    a0 : Bit

open SRL16EAddress public

address0000 address0001 address1000 address1111 : SRL16EAddress
address0000 = addressBits low  low  low  low
address0001 = addressBits low  low  low  high
address1000 = addressBits high low  low  low
address1111 = addressBits high high high high

-- A3 is the most-significant address bit and A0 is the least-significant.

readSRL16E : SRL16EState → SRL16EAddress → Bit
readSRL16E
  (s0  ∷ s1  ∷ s2  ∷ s3
   ∷ s4  ∷ s5  ∷ s6  ∷ s7
   ∷ s8  ∷ s9  ∷ s10 ∷ s11
   ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ [])
  (addressBits a3-bit a2-bit a1-bit a0-bit) =
  mux a3-bit
    (mux a2-bit
      (mux a1-bit (mux a0-bit s0  s1)  (mux a0-bit s2  s3))
      (mux a1-bit (mux a0-bit s4  s5)  (mux a0-bit s6  s7)))
    (mux a2-bit
      (mux a1-bit (mux a0-bit s8  s9)  (mux a0-bit s10 s11))
      (mux a1-bit (mux a0-bit s12 s13) (mux a0-bit s14 s15)))

-- One enabled rising edge computes every destination from the same source
-- state.  The final old bit falls off the end.

shiftIn : Bit → SRL16EState → SRL16EState
shiftIn data-in
  (s0  ∷ s1  ∷ s2  ∷ s3
   ∷ s4  ∷ s5  ∷ s6  ∷ s7
   ∷ s8  ∷ s9  ∷ s10 ∷ s11
   ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ []) =
  data-in
  ∷ s0  ∷ s1  ∷ s2  ∷ s3
  ∷ s4  ∷ s5  ∷ s6  ∷ s7
  ∷ s8  ∷ s9  ∷ s10 ∷ s11
  ∷ s12 ∷ s13 ∷ s14 ∷ []

-- CLK is represented only by the project's untimed abstract event.  An idle
-- event cannot update state.  A rising edge updates exactly when CE is high.

updateSRL16E : Event → Bit → Bit → SRL16EState → SRL16EState
updateSRL16E idle       enable data-in state = state
updateSRL16E risingEdge false  data-in state = state
updateSRL16E risingEdge true   data-in state = shiftIn data-in state

defaultInitialState : SRL16EState
defaultInitialState =
  low ∷ low ∷ low ∷ low
  ∷ low ∷ low ∷ low ∷ low
  ∷ low ∷ low ∷ low ∷ low
  ∷ low ∷ low ∷ low ∷ low ∷ []

-- Checked hold examples.

idle-holds : ∀ enable data-in state
           → updateSRL16E idle enable data-in state ≡ state
idle-holds enable data-in state = refl

disabled-rising-edge-holds : ∀ data-in state
                           → updateSRL16E risingEdge low data-in state ≡ state
disabled-rising-edge-holds data-in state = refl

disabled-rising-edge-preserves-read : ∀ data-in state address
  → readSRL16E (updateSRL16E risingEdge low data-in state) address
  ≡ readSRL16E state address
disabled-rising-edge-preserves-read data-in state address = refl

-- This vector equality checks the simultaneous/source-state shift rule for
-- all 16 destinations at once.

enabled-rising-edge-shifts-source-state :
  ∀ data-in s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15
  → updateSRL16E risingEdge high data-in
      (s0  ∷ s1  ∷ s2  ∷ s3
       ∷ s4  ∷ s5  ∷ s6  ∷ s7
       ∷ s8  ∷ s9  ∷ s10 ∷ s11
       ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ [])
  ≡ data-in
    ∷ s0  ∷ s1  ∷ s2  ∷ s3
    ∷ s4  ∷ s5  ∷ s6  ∷ s7
    ∷ s8  ∷ s9  ∷ s10 ∷ s11
    ∷ s12 ∷ s13 ∷ s14 ∷ []
enabled-rising-edge-shifts-source-state
  data-in s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 = refl

-- Checked address ordering and endpoint examples.

address-0000-selects-first :
  ∀ s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15
  → readSRL16E
      (s0  ∷ s1  ∷ s2  ∷ s3
       ∷ s4  ∷ s5  ∷ s6  ∷ s7
       ∷ s8  ∷ s9  ∷ s10 ∷ s11
       ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ [])
      address0000
  ≡ s0
address-0000-selects-first
  s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 = refl

address-0001-selects-second :
  ∀ s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15
  → readSRL16E
      (s0  ∷ s1  ∷ s2  ∷ s3
       ∷ s4  ∷ s5  ∷ s6  ∷ s7
       ∷ s8  ∷ s9  ∷ s10 ∷ s11
       ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ [])
      address0001
  ≡ s1
address-0001-selects-second
  s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 = refl

address-1000-selects-ninth :
  ∀ s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15
  → readSRL16E
      (s0  ∷ s1  ∷ s2  ∷ s3
       ∷ s4  ∷ s5  ∷ s6  ∷ s7
       ∷ s8  ∷ s9  ∷ s10 ∷ s11
       ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ [])
      address1000
  ≡ s8
address-1000-selects-ninth
  s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 = refl

address-1111-selects-last :
  ∀ s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15
  → readSRL16E
      (s0  ∷ s1  ∷ s2  ∷ s3
       ∷ s4  ∷ s5  ∷ s6  ∷ s7
       ∷ s8  ∷ s9  ∷ s10 ∷ s11
       ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ [])
      address1111
  ≡ s15
address-1111-selects-last
  s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 = refl

new-data-appears-at-length-one : ∀ data-in state
  → readSRL16E (updateSRL16E risingEdge high data-in state) address0000
  ≡ data-in
new-data-appears-at-length-one data-in
  (s0  ∷ s1  ∷ s2  ∷ s3
   ∷ s4  ∷ s5  ∷ s6  ∷ s7
   ∷ s8  ∷ s9  ∷ s10 ∷ s11
   ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ []) = refl

last-stage-reads-previous-stage :
  ∀ data-in s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15
  → readSRL16E
      (updateSRL16E risingEdge high data-in
        (s0  ∷ s1  ∷ s2  ∷ s3
         ∷ s4  ∷ s5  ∷ s6  ∷ s7
         ∷ s8  ∷ s9  ∷ s10 ∷ s11
         ∷ s12 ∷ s13 ∷ s14 ∷ s15 ∷ []))
      address1111
  ≡ s14
last-stage-reads-previous-stage
  data-in s0 s1 s2 s3 s4 s5 s6 s7 s8 s9 s10 s11 s12 s13 s14 s15 = refl

default-initial-output-is-low : ∀ address
  → readSRL16E defaultInitialState address ≡ low
default-initial-output-is-low (addressBits false false false false) = refl
default-initial-output-is-low (addressBits false false false true)  = refl
default-initial-output-is-low (addressBits false false true  false) = refl
default-initial-output-is-low (addressBits false false true  true)  = refl
default-initial-output-is-low (addressBits false true  false false) = refl
default-initial-output-is-low (addressBits false true  false true)  = refl
default-initial-output-is-low (addressBits false true  true  false) = refl
default-initial-output-is-low (addressBits false true  true  true)  = refl
default-initial-output-is-low (addressBits true  false false false) = refl
default-initial-output-is-low (addressBits true  false false true)  = refl
default-initial-output-is-low (addressBits true  false true  false) = refl
default-initial-output-is-low (addressBits true  false true  true)  = refl
default-initial-output-is-low (addressBits true  true  false false) = refl
default-initial-output-is-low (addressBits true  true  false true)  = refl
default-initial-output-is-low (addressBits true  true  true  false) = refl
default-initial-output-is-low (addressBits true  true  true  true)  = refl