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

module Spartan6.Primitive.RAM256X1S 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, "RAM256X1S", printed pages 248-249.
--
-- Printed page 248 specifies a 256-word by one-bit single-port distributed
-- RAM with an eight-bit address bus A.  Its read is asynchronous: O displays
-- the contents selected by A independently of WE.  A low-to-high WCLK
-- transition writes D at the selected address when the active-high WE input
-- is asserted, and the output is updated to the newly written value after
-- that write.  Printed page 249 documents the 256-bit INIT attribute, its
-- all-zero default, and positive-edge-write/asynchronous-read HDL templates.
--
-- The entry presents A as one eight-bit bus; it does not label the individual
-- bus bits or give their weights.  The executable interface therefore accepts
-- the already decoded address Fin 256, in the canonical order 0 through 255,
-- rather than inventing a raw bus-to-index convention.  Likewise, arbitrary
-- raw hexadecimal INIT decoding is not claimed.  This is an untimed,
-- two-valued model: the physical delay implicit in "shortly after", setup and
-- hold behavior, unstable edge inputs, placement, and electrical behavior are
-- outside its scope.

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

ram256x1sLocator : SourceLocator
ram256x1sLocator =
  locate ram256x1sPinnedSource "RAM256X1S"
    "printed page 248: introduction, port table, write/read behavior, and default INIT; printed page 249: INIT attribute and positive-edge-write asynchronous-read templates"

ram256x1sTrace : RuleTraceability
ram256x1sTrace =
  traceRule "primitive.RAM256X1S.two-valued"
            officialDocumentation
            (just ram256x1sLocator)
            partiallySupported
            guaranteed
            "Executable decoded-address asynchronous read, hold, enabled rising-edge write, post-write output, and all-zero default INIT; raw address-bus/hex-INIT decoding and physical timing are not modelled."

RAM256X1SState : Type₀
RAM256X1SState = Memory.Memory  

-- Fin's constructors expose the supported decoded address order directly:
-- fzero denotes address 0, fsuc fzero denotes address 1, and so on through
-- address 255.  No claim about the encoding of UG615's raw A bus is made.

RAM256X1SAddress : Type₀
RAM256X1SAddress = Fin 

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

-- O is purely a function of the present contents and decoded address.  The
-- lack of Event, WE, D, or clock arguments expresses asynchronous read.

readRAM256X1S : RAM256X1SState → RAM256X1SAddress → Bit
readRAM256X1S state address = wordBit (Memory.read address state)

-- WCLK is represented by the project's abstract Event.  idle covers every
-- observation without a low-to-high transition, including falling edges.

updateRAM256X1S :
  Event → Bit → RAM256X1SAddress → Bit → RAM256X1SState
  → RAM256X1SState
updateRAM256X1S idle       write-enable address data-in state = state
updateRAM256X1S risingEdge write-enable address data-in state =
  Memory.writeIf write-enable address (data-in ∷ []) state

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

-- Supported documentary rows and deliberately excluded raw/physical cases.

data RAM256X1SBoundary : Type₀ where
  sameAddressPostWriteOutput : RAM256X1SBoundary
  defaultINIT                : RAM256X1SBoundary
  rawAddressBusDecoding      : RAM256X1SBoundary
  rawHexINITDecoding         : RAM256X1SBoundary
  physicalWriteTiming        : RAM256X1SBoundary

boundarySupport : RAM256X1SBoundary → SupportStatus
boundarySupport sameAddressPostWriteOutput = fullySupported
boundarySupport defaultINIT                = fullySupported
boundarySupport rawAddressBusDecoding      = unsupportedFeature
boundarySupport rawHexINITDecoding         = unsupportedFeature
boundarySupport physicalWriteTiming        = unsupportedFeature

boundarySemantics : RAM256X1SBoundary → SemanticStatus
boundarySemantics sameAddressPostWriteOutput = guaranteed
boundarySemantics defaultINIT                = guaranteed
boundarySemantics rawAddressBusDecoding      = unsupportedSemantics
boundarySemantics rawHexINITDecoding         = unsupportedSemantics
boundarySemantics physicalWriteTiming        = insufficientEvidence

boundaryNote : RAM256X1SBoundary → String
boundaryNote sameAddressPostWriteOutput =
  "UG615 printed page 248 says O is updated to the newly written value after the write; the model exposes that post-state value without a delay claim."
boundaryNote defaultINIT =
  "UG615 printed pages 248-249 give all zeros as the default value of the 256-bit INIT attribute."
boundaryNote rawAddressBusDecoding =
  "The entry exposes one eight-bit A bus but does not label its component bits or state their weights; this module accepts a decoded Fin 256 address."
boundaryNote rawHexINITDecoding =
  "The cited entry gives no raw hexadecimal bit-to-address table; callers must supply already address-indexed contents."
boundaryNote physicalWriteTiming =
  "The physical 'shortly after' delay and setup/hold behavior have no invented value in this untimed event model."

-- Checked decoded-address order.

addressZero : RAM256X1SAddress
addressZero = fzero

addressOne : RAM256X1SAddress
addressOne = fsuc fzero

addressTwo : RAM256X1SAddress
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 enabled-write laws.

no-rising-edge-holds : ∀ write-enable address data-in state
  → updateRAM256X1S 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
  → updateRAM256X1S risingEdge low address data-in state ≡ state
disabled-rising-edge-holds address data-in state = refl

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

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

-- UG615's post-write output statement, interpreted only after the state
-- transition.  This makes no assertion about analogue values during the edge.

same-address-post-write-output-is-D : ∀ address data-in state
  → readRAM256X1S
      (updateRAM256X1S risingEdge high address data-in state)
      address
  ≡ data-in
same-address-post-write-output-is-D address data-in state =
  cong wordBit
    (Memory.read-after-write-same address (data-in ∷ []) state)

-- The all-zero default is checked for every decoded address without assuming
-- any arbitrary hexadecimal-to-address convention.

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-output-is-low : ∀ address
  → readRAM256X1S defaultInitialState address ≡ low
default-output-is-low address =
  cong wordBit (lookup-replicate address (low ∷ []))

-- Address changes affect asynchronous O without any clock event.  This state
-- differs from the default only at decoded address 1.

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

asynchronous-read-address-zero :
  readRAM256X1S exampleState addressZero ≡ low
asynchronous-read-address-zero = refl

asynchronous-read-address-one :
  readRAM256X1S exampleState addressOne ≡ high
asynchronous-read-address-one = refl

write-address-one-read-after-write :
  readRAM256X1S
    (updateRAM256X1S risingEdge high addressOne high defaultInitialState)
    addressOne
  ≡ high
write-address-one-read-after-write = refl

same-address-post-write-is-supported :
  fullySupported? (boundarySupport sameAddressPostWriteOutput) ≡ true
same-address-post-write-is-supported = refl

raw-address-decoding-is-not-executable :
  executable? (boundarySemantics rawAddressBusDecoding) ≡ false
raw-address-decoding-is-not-executable = refl

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