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

module Spartan6.Primitive.BlockRAM where

open import Spartan6.Prelude
open import Spartan6.Evidence
  using (SemanticStatus; documentedUnspecified;
         SupportStatus; unsupportedFeature)
import Spartan6.Foundation.Memory as Memory

-- Official functional evidence:
--
-- AMD/Xilinx, "Spartan-6 FPGA Block RAM Resources User Guide", UG383
-- v1.5, 8 July 2011:
-- https://docs.amd.com/v/u/en-US/ug383
--
-- * "Summary": PDF page 7, printed page 8.  Block RAM can be configured
--   single-port; reads and writes are synchronous; a write can expose the
--   new word, the old word, or leave the output unchanged.
-- * "Spartan-6 FPGA Block RAM Features": PDF page 11, printed page 12.
--   Reads and writes each require one clock edge, outputs are latched, and
--   the three read-during-write modes are WRITE_FIRST, READ_FIRST, and
--   NO_CHANGE.
-- * Table 5: PDF page 12, printed page 13.  When EN is inactive, no write
--   occurs and the output bus retains its previous value.
-- * "Read Operation", "Write Operation", and "Write Modes": PDF page 13,
--   printed page 14.  These sections define one-edge latch-mode behavior and
--   the WRITE_FIRST output.
-- * "READ_FIRST or Read-Before-Write Mode" and "NO_CHANGE Mode": PDF page
--   14, printed page 15.  These sections define the other two outputs.
-- * "Conflict Avoidance": PDF page 15, printed page 16.  This model avoids
--   those conditional and unreliable cases entirely by exposing one port.
--
-- AMD/Xilinx, "Spartan-6 FPGA: 9 Kb Block RAM Configuration
-- Initialization and Configuration Readback", XCN11014 v1.0,
-- 23 May 2011:
-- https://docs.amd.com/v/u/en-US/xcn11014
--
-- * "9 Kb Block RAM Configuration Initialization": PDF page 1, printed
--   page 1.  Configuration-event initial contents are undefined.
-- * "9 Kb Block RAM Configuration Readback": PDF page 1, printed page 1.
--   Configuration readback is unsupported and can corrupt memory contents.
--
-- Scope: this is a generic, one-port, untimed digital core in latch mode.
-- Its initial state is supplied explicitly by the caller; it is never claimed
-- to be configuration-derived 9 Kb contents.  Dual-port operation and all
-- collisions, optional output pipeline registers, reset behavior, byte and
-- parity lanes, ECC, configuration readback, legal physical width/depth
-- combinations, placement, and timing are not modeled.

data WriteMode : Type₀ where
  WRITE_FIRST : WriteMode
  READ_FIRST  : WriteMode
  NO_CHANGE   : WriteMode

record SinglePortState (depth width : ℕ) : Type₀ where
  constructor singlePortState
  field
    memoryContents : Memory.Memory depth width
    outputLatch    : Word width

open SinglePortState public

record PortCommand (depth width : ℕ) : Type₀ where
  constructor portCommand
  field
    commandAddress     : Fin depth
    commandInput       : Word width
    commandEnable      : Bit
    commandWriteEnable : Bit

open PortCommand public

-- One application represents one active edge of the single port clock.

clockEdge : ∀ {depth width}
          → WriteMode
          → PortCommand depth width
          → SinglePortState depth width
          → SinglePortState depth width
clockEdge mode
          (portCommand address inputValue false writeEnabled)
          state =
  state
clockEdge mode
          (portCommand address inputValue true false)
          state =
  singlePortState
    (memoryContents state)
    (Memory.read address (memoryContents state))
clockEdge WRITE_FIRST
          (portCommand address inputValue true true)
          state =
  singlePortState
    (Memory.write address inputValue (memoryContents state))
    inputValue
clockEdge READ_FIRST
          (portCommand address inputValue true true)
          state =
  singlePortState
    (Memory.write address inputValue (memoryContents state))
    (Memory.read address (memoryContents state))
clockEdge NO_CHANGE
          (portCommand address inputValue true true)
          state =
  singlePortState
    (Memory.write address inputValue (memoryContents state))
    (outputLatch state)

disabled-holds : ∀ {depth width}
  (mode : WriteMode) (address : Fin depth) (inputValue : Word width)
  (writeEnabled : Bit) (state : SinglePortState depth width)
  → clockEdge mode
      (portCommand address inputValue low writeEnabled) state
    ≡ state
disabled-holds mode address inputValue writeEnabled state = refl

read-loads-latch : ∀ {depth width}
  (mode : WriteMode) (address : Fin depth) (inputValue : Word width)
  (state : SinglePortState depth width)
  → outputLatch
      (clockEdge mode (portCommand address inputValue high low) state)
    ≡ Memory.read address (memoryContents state)
read-loads-latch mode address inputValue state = refl

write-first-output : ∀ {depth width}
  (address : Fin depth) (inputValue : Word width)
  (state : SinglePortState depth width)
  → outputLatch
      (clockEdge WRITE_FIRST
        (portCommand address inputValue high high) state)
    ≡ inputValue
write-first-output address inputValue state = refl

read-first-output : ∀ {depth width}
  (address : Fin depth) (inputValue : Word width)
  (state : SinglePortState depth width)
  → outputLatch
      (clockEdge READ_FIRST
        (portCommand address inputValue high high) state)
    ≡ Memory.read address (memoryContents state)
read-first-output address inputValue state = refl

no-change-output : ∀ {depth width}
  (address : Fin depth) (inputValue : Word width)
  (state : SinglePortState depth width)
  → outputLatch
      (clockEdge NO_CHANGE
        (portCommand address inputValue high high) state)
    ≡ outputLatch state
no-change-output address inputValue state = refl

write-stores : ∀ {depth width}
  (mode : WriteMode) (address : Fin depth) (inputValue : Word width)
  (state : SinglePortState depth width)
  → Memory.read address
      (memoryContents
        (clockEdge mode
          (portCommand address inputValue high high) state))
    ≡ inputValue
write-stores WRITE_FIRST address inputValue state =
  Memory.read-after-write-same address inputValue (memoryContents state)
write-stores READ_FIRST address inputValue state =
  Memory.read-after-write-same address inputValue (memoryContents state)
write-stores NO_CHANGE address inputValue state =
  Memory.read-after-write-same address inputValue (memoryContents state)

-- XCN11014 is represented as a status, not as invented initial data.

nineKbInitializationStatus : SemanticStatus
nineKbInitializationStatus = documentedUnspecified

nineKbConfigurationReadbackStatus : SupportStatus
nineKbConfigurationReadbackStatus = unsupportedFeature

nineKb-initialization-is-unspecified :
  nineKbInitializationStatus ≡ documentedUnspecified
nineKb-initialization-is-unspecified = refl

nineKb-readback-is-unsupported :
  nineKbConfigurationReadbackStatus ≡ unsupportedFeature
nineKb-readback-is-unsupported = refl

-- A small word-level example separates all three write-mode outputs.

exampleMemory : Memory.Memory  
exampleMemory =
  (low ∷ low ∷ []) ∷
  (high ∷ low ∷ []) ∷
  []

exampleState : SinglePortState  
exampleState = singlePortState exampleMemory (low ∷ high ∷ [])

exampleWrite : PortCommand  
exampleWrite = portCommand fzero (high ∷ high ∷ []) high high

example-write-first :
  outputLatch (clockEdge WRITE_FIRST exampleWrite exampleState)
  ≡ (high ∷ high ∷ [])
example-write-first = refl

example-read-first :
  outputLatch (clockEdge READ_FIRST exampleWrite exampleState)
  ≡ (low ∷ low ∷ [])
example-read-first = refl

example-no-change :
  outputLatch (clockEdge NO_CHANGE exampleWrite exampleState)
  ≡ (low ∷ high ∷ [])
example-no-change = refl

example-write-stored :
  Memory.read fzero
    (memoryContents (clockEdge NO_CHANGE exampleWrite exampleState))
  ≡ (high ∷ high ∷ [])
example-write-stored = refl