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

module Spartan6.Primitive.RAM128X1D where

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

import Spartan6.Foundation.Memory as Memory

-- Source: UG615 v14.7, "RAM128X1D", printed pages 245-246.
--
-- Printed page 245 specifies one 128-deep, one-bit memory with a read/write
-- port addressed by the seven-bit A bus and an independent read port addressed
-- by the seven-bit DPRA bus.  With WE high, a rising WCLK edge writes D at A
-- and the newly written value is subsequently reflected on SPO.  With WE low,
-- A reads asynchronously to SPO; DPRA reads asynchronously to DPO.  The same
-- page gives an optional 128-bit hexadecimal INIT and an all-zero default.
-- Printed page 246 repeats positive-edge write and asynchronous read in both
-- HDL templates and gives all zeros as the INIT attribute default.
--
-- The entry presents A and DPRA as undivided seven-bit buses and supplies no
-- individual bit weights.  This executable interface therefore takes already
-- decoded Fin 128 addresses in canonical order 0 through 127 instead of
-- inventing raw bus decoding.  It also does not decode arbitrary hexadecimal
-- INIT text.  Reads in this module describe stable states before or after the
-- abstract write transition.  UG615 gives no digital value for DPO during the
-- physical interval in which A = DPRA is being written; collision transients,
-- the stated "shortly after" delay, setup/hold behavior, unstable edge inputs,
-- placement, and electrical behavior are deliberately outside the model.

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

ram128x1dLocator : SourceLocator
ram128x1dLocator =
  locate ram128x1dPinnedSource "RAM128X1D"
    "printed page 245: introduction, port descriptions, positive-edge write, asynchronous SPO/DPO reads, and default INIT; printed page 246: INIT attribute and HDL templates"

ram128x1dTrace : RuleTraceability
ram128x1dTrace =
  traceRule "primitive.RAM128X1D.stable-two-valued"
            officialDocumentation
            (just ram128x1dLocator)
            partiallySupported
            guaranteed
            "Executable stable-state dual asynchronous read, hold, enabled rising-edge single write, post-write outputs, and all-zero default INIT; physical write/read collision transients, raw address/INIT decoding, and timing are not modelled."

RAM128X1DState : Type₀
RAM128X1DState = Memory.Memory  

-- Fin exposes only the documented decoded address order.  fzero is address 0,
-- fsuc fzero is address 1, and the final inhabitant denotes address 127.

RAM128X1DAddress : Type₀
RAM128X1DAddress = Fin 

RAM128X1DAAddress : Type₀
RAM128X1DAAddress = RAM128X1DAddress

RAM128X1DDPRAAddress : Type₀
RAM128X1DDPRAAddress = RAM128X1DAddress

wordBit : Word  → Bit
wordBit (bit ∷ []) = bit

-- Both observations are functions only of memory and their own address.  No
-- event or clock argument is needed, expressing the documented asynchronous
-- reads.  They are intended for stable states, not the physical write instant.

readSPO : RAM128X1DState → RAM128X1DAAddress → Bit
readSPO state address = wordBit (Memory.read address state)

readDPO : RAM128X1DState → RAM128X1DDPRAAddress → Bit
readDPO state dual-port-read-address =
  wordBit (Memory.read dual-port-read-address state)

-- There is one write path: D is written at A.  idle covers observations with
-- no low-to-high WCLK transition; a rising edge writes only when WE is high.

updateRAM128X1D :
  Event → Bit → RAM128X1DAAddress → Bit → RAM128X1DState
  → RAM128X1DState
updateRAM128X1D idle       write-enable address data-in state = state
updateRAM128X1D risingEdge write-enable address data-in state =
  Memory.writeIf write-enable address (data-in ∷ []) state

defaultInitialState : RAM128X1DState
defaultInitialState = replicate (low ∷ [])

-- The stable post-write facts are distinct from the undocumented values and
-- delays during the physical write/read collision interval.

data RAM128X1DBoundary : Type₀ where
  stableSPOAfterWrite       : RAM128X1DBoundary
  stableDPOAfterWrite       : RAM128X1DBoundary
  defaultINIT               : RAM128X1DBoundary
  writeReadCollisionInstant : RAM128X1DBoundary
  rawAddressBusDecoding     : RAM128X1DBoundary
  rawHexINITDecoding        : RAM128X1DBoundary
  physicalWriteTiming       : RAM128X1DBoundary

boundarySupport : RAM128X1DBoundary → SupportStatus
boundarySupport stableSPOAfterWrite       = fullySupported
boundarySupport stableDPOAfterWrite       = fullySupported
boundarySupport defaultINIT               = fullySupported
boundarySupport writeReadCollisionInstant = unsupportedFeature
boundarySupport rawAddressBusDecoding     = unsupportedFeature
boundarySupport rawHexINITDecoding        = unsupportedFeature
boundarySupport physicalWriteTiming       = unsupportedFeature

boundarySemantics : RAM128X1DBoundary → SemanticStatus
boundarySemantics stableSPOAfterWrite       = guaranteed
boundarySemantics stableDPOAfterWrite       = guaranteed
boundarySemantics defaultINIT               = guaranteed
boundarySemantics writeReadCollisionInstant = insufficientEvidence
boundarySemantics rawAddressBusDecoding     = unsupportedSemantics
boundarySemantics rawHexINITDecoding        = unsupportedSemantics
boundarySemantics physicalWriteTiming       = insufficientEvidence

boundaryNote : RAM128X1DBoundary → String
boundaryNote stableSPOAfterWrite =
  "UG615 printed page 245 explicitly says the written D value is reflected on SPO after the write."
boundaryNote stableDPOAfterWrite =
  "After a completed write, the documented asynchronous DPRA read observes the stable contents at DPRA; this is not a claim about the write instant."
boundaryNote defaultINIT =
  "UG615 printed pages 245-246 give all zeros as the default 128-bit INIT value."
boundaryNote writeReadCollisionInstant =
  "UG615 gives no two-valued DPO result during a physical write with A equal to DPRA; only stable pre/post states are executable."
boundaryNote rawAddressBusDecoding =
  "The entry gives two seven-bit buses but no individual bit weights; callers supply decoded Fin 128 addresses."
boundaryNote rawHexINITDecoding =
  "The entry gives no raw hexadecimal bit-to-address table; callers supply already address-indexed contents."
boundaryNote physicalWriteTiming =
  "The physical 'shortly after' delay and setup/hold behavior are outside this untimed event model."

-- Checked decoded-address order.

addressZero : RAM128X1DAddress
addressZero = fzero

addressOne : RAM128X1DAddress
addressOne = fsuc fzero

addressTwo : RAM128X1DAddress
addressTwo = fsuc (fsuc fzero)

address-one-is-successor-zero : addressOne ≡ fsuc fzero
address-one-is-successor-zero = refl

address-two-is-double-successor-zero : addressTwo ≡ fsuc (fsuc fzero)
address-two-is-double-successor-zero = refl

-- Checked hold and single-write laws.

no-rising-edge-holds : ∀ write-enable address data-in state
  → updateRAM128X1D idle write-enable address data-in state ≡ state
no-rising-edge-holds write-enable address data-in state = refl

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

disabled-rising-edge-preserves-SPO : ∀ read-address write-address data-in state
  → readSPO
      (updateRAM128X1D risingEdge low write-address data-in state)
      read-address
  ≡ readSPO state read-address
disabled-rising-edge-preserves-SPO read-address write-address data-in state =
  refl

disabled-rising-edge-preserves-DPO : ∀ read-address write-address data-in state
  → readDPO
      (updateRAM128X1D risingEdge low write-address data-in state)
      read-address
  ≡ readDPO state read-address
disabled-rising-edge-preserves-DPO read-address write-address data-in state =
  refl

enabled-rising-edge-writes-at-A : ∀ address data-in state
  → updateRAM128X1D risingEdge high address data-in state
  ≡ Memory.write address (data-in ∷ []) state
enabled-rising-edge-writes-at-A address data-in state = refl

-- The first theorem is the explicit SPO sentence from printed page 245.  The
-- second is only a stable post-state consequence of the asynchronous DPO read;
-- neither theorem assigns a transient value at the physical write instant.

same-A-SPO-after-write-is-D : ∀ address data-in state
  → readSPO
      (updateRAM128X1D risingEdge high address data-in state)
      address
  ≡ data-in
same-A-SPO-after-write-is-D address data-in state =
  cong wordBit
    (Memory.read-after-write-same address (data-in ∷ []) state)

same-DPRA-after-completed-write-is-D : ∀ address data-in state
  → readDPO
      (updateRAM128X1D risingEdge high address data-in state)
      address
  ≡ data-in
same-DPRA-after-completed-write-is-D address data-in state =
  cong wordBit
    (Memory.read-after-write-same address (data-in ∷ []) state)

-- The all-zero default is checked at every address without a raw hexadecimal
-- decoding assumption.

lookup-replicate : ∀ {ℓ n} {A : Type ℓ} (index : Fin n) (value : A)
  → lookup index (replicate value) ≡ value
lookup-replicate fzero value = refl
lookup-replicate (fsuc index) value = lookup-replicate index value

default-SPO-is-low : ∀ address
  → readSPO defaultInitialState address ≡ low
default-SPO-is-low address =
  cong wordBit (lookup-replicate address (low ∷ []))

default-DPO-is-low : ∀ address
  → readDPO defaultInitialState address ≡ low
default-DPO-is-low address =
  cong wordBit (lookup-replicate address (low ∷ []))

-- Independent address changes affect both asynchronous outputs without an
-- event.  This state differs from the default only at decoded address 1.

exampleState : RAM128X1DState
exampleState = Memory.write addressOne (high ∷ []) defaultInitialState

asynchronous-SPO-at-address-zero :
  readSPO exampleState addressZero ≡ low
asynchronous-SPO-at-address-zero = refl

asynchronous-SPO-at-address-one :
  readSPO exampleState addressOne ≡ high
asynchronous-SPO-at-address-one = refl

independent-asynchronous-DPO-at-address-one :
  readDPO exampleState addressOne ≡ high
independent-asynchronous-DPO-at-address-one = refl

independent-asynchronous-DPO-at-address-two :
  readDPO exampleState addressTwo ≡ low
independent-asynchronous-DPO-at-address-two = refl

stable-SPO-sees-completed-write :
  readSPO
    (updateRAM128X1D risingEdge high addressOne high defaultInitialState)
    addressOne
  ≡ high
stable-SPO-sees-completed-write = refl

stable-DPO-sees-completed-write :
  readDPO
    (updateRAM128X1D risingEdge high addressOne high defaultInitialState)
    addressOne
  ≡ high
stable-DPO-sees-completed-write = refl

stable-SPO-post-write-is-supported :
  fullySupported? (boundarySupport stableSPOAfterWrite) ≡ true
stable-SPO-post-write-is-supported = refl

write-read-collision-instant-is-not-executable :
  executable? (boundarySemantics writeReadCollisionInstant) ≡ false
write-read-collision-instant-is-not-executable = refl

raw-INIT-decoding-is-not-executable :
  executable? (boundarySemantics rawHexINITDecoding) ≡ false
raw-INIT-decoding-is-not-executable = refl