Spartan6.Netlist.NormalizeMixed

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

module Spartan6.Netlist.NormalizeMixed where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.GenericBuilder as Generic
import Spartan6.Netlist.NormalizeRegisters as Registers
import Spartan6.Netlist.Raw as Raw
import Spartan6.Netlist.RegisterMode as Single
import Spartan6.Netlist.Schedule as Schedule
import Spartan6.Netlist.TopInterface as TopInterface
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

-- Mixed combinational/state candidate translation.
--
-- Register Q nets are allocated first.  The checked scheduler then repeatedly
-- selects a processable non-register occurrence, so acyclic forward references
-- need not already be in topological source order and equal-valued duplicates
-- retain occurrence-sensitive provenance.  Finally two anonymous mux nodes
-- per FDRE/FDSE compute all next values from current-state/combinational wires.
-- Anonymous next-state nodes never introduce raw net IDs and therefore cannot
-- shadow source connectivity.

singleton : Diagnostic.Diagnostic → Diagnostic.Diagnostics
singleton item = item ∷ᴸ []ᴸ

issue : Diagnostic.DiagnosticCode → String → String → String → String
      → Diagnostic.Diagnostic
issue code subject expected observed detail =
  Diagnostic.diagnostic code Diagnostic.reject subject expected observed detail

record InstancePartition : Type₀ where
  constructor instancePartition
  field
    partitionRegisters     : List Registers.RegisterDescriptor
    partitionCombinational : List Raw.RawInstance

open InstancePartition public

prependRegister : Registers.RegisterDescriptor
                → Diagnostic.CheckResult InstancePartition
                → Diagnostic.CheckResult InstancePartition
prependRegister descriptor (Diagnostic.rejected diagnostics) =
  Diagnostic.rejected diagnostics
prependRegister descriptor
  (Diagnostic.accepted (instancePartition registers combinational)) =
  Diagnostic.accepted
    (instancePartition (descriptor ∷ᴸ registers) combinational)

prependCombinational : Raw.RawInstance
                     → Diagnostic.CheckResult InstancePartition
                     → Diagnostic.CheckResult InstancePartition
prependCombinational item (Diagnostic.rejected diagnostics) =
  Diagnostic.rejected diagnostics
prependCombinational item
  (Diagnostic.accepted (instancePartition registers combinational)) =
  Diagnostic.accepted
    (instancePartition registers (item ∷ᴸ combinational))

mutual
  partitionRegisterItem : Raw.RawInstance → List Raw.RawInstance
                        → Diagnostic.CheckResult InstancePartition
  partitionRegisterItem item items with Registers.normaliseDescriptor item
  ... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
  ... | Diagnostic.accepted descriptor =
    prependRegister descriptor (partitionInstances items)

  partitionInstances : List Raw.RawInstance
                     → Diagnostic.CheckResult InstancePartition
  partitionInstances []ᴸ =
    Diagnostic.accepted (instancePartition []ᴸ []ᴸ)
  partitionInstances (item ∷ᴸ items) with Raw.rawInstanceKind item
  ... | Raw.knownPrimitive Architecture.FDRE =
    partitionRegisterItem item items
  ... | Raw.knownPrimitive Architecture.FDSE =
    partitionRegisterItem item items
  ... | kind = prependCombinational item (partitionInstances items)

registerQNets : List Registers.RegisterDescriptor → List Raw.NetId
registerQNets []ᴸ = []ᴸ
registerQNets (descriptor ∷ᴸ descriptors) =
  Registers.descriptorQNet descriptor ∷ᴸ registerQNets descriptors

descriptorBindings : ∀ {inputCount}
  → (descriptors : List Registers.RegisterDescriptor)
  → Generic.Bindings inputCount (lengthList descriptors) 0
descriptorBindings []ᴸ = []ᴸ
descriptorBindings (descriptor ∷ᴸ descriptors) =
  Generic.bindNet
    (Registers.descriptorQNet descriptor)
    (Checked.storedWire fzero)
  ∷ᴸ Generic.liftRegisterBindings (descriptorBindings descriptors)

mixedInitialBuilder :
  (input-nets : List Raw.NetId)
  → (registers : List Registers.RegisterDescriptor)
  → Generic.Builder (lengthList input-nets) (lengthList registers)
mixedInitialBuilder input-nets registers =
  Generic.builder 0 Checked.noNodes
    (descriptorBindings registers
     ++ᴸ Generic.inputBindings input-nets)

appendAnonymous : ∀ {inputCount registerCount}
  → (current : Generic.Builder inputCount registerCount)
  → Checked.Node inputCount registerCount
      (Generic.builderLocalCount current)
  → Generic.Builder inputCount registerCount
appendAnonymous (Generic.builder local-count nodes bindings) node =
  Generic.builder
    (suc local-count)
    (nodes Checked.▻ node)
    (Generic.liftLocalBindings bindings)

liftTwice : ∀ {inputCount registerCount localCount}
  → Checked.Wire inputCount registerCount localCount
  → Checked.Wire inputCount registerCount (suc (suc localCount))
liftTwice (Checked.externalWire index) = Checked.externalWire index
liftTwice (Checked.storedWire index) = Checked.storedWire index
liftTwice (Checked.localWire index) =
  Checked.localWire (fsuc (fsuc index))
liftTwice (Checked.literalWire bit) = Checked.literalWire bit

liftNextTwice : ∀ {inputCount registerCount localCount count}
  → Vec (Checked.Wire inputCount registerCount localCount) count
  → Vec
      (Checked.Wire inputCount registerCount (suc (suc localCount)))
      count
liftNextTwice [] = []
liftNextTwice (wire ∷ wires) = liftTwice wire ∷ liftNextTwice wires

record BuiltRegisters
  (inputCount registerCount nextCount : ℕ) : Type₀ where
  constructor builtRegisters
  field
    builtBuilder : Generic.Builder inputCount registerCount
    builtNext :
      Vec
        (Checked.Wire inputCount registerCount
          (Generic.builderLocalCount builtBuilder))
        nextCount

open BuiltRegisters public

finishRegisterNodes : ∀ {inputCount registerCount nextCount}
  → Registers.RegisterDescriptor
  → BuiltRegisters inputCount registerCount nextCount
  → Diagnostic.CheckResult
      (BuiltRegisters inputCount registerCount (suc nextCount))
finishRegisterNodes {inputCount = inputCount} {registerCount = registerCount}
  descriptor (builtRegisters current next-wires)
  with Generic.resolveOneConnection
    "register.Q" (Generic.builderBindings current)
    (Raw.net (Registers.descriptorQNet descriptor))
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted current-wire
  with Generic.resolveScalarPort
    "register.D" (Generic.builderBindings current)
    (Single.registerD (Registers.descriptorPorts descriptor))
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted data-wire
  with Generic.resolveScalarPort
    "register.CE" (Generic.builderBindings current)
    (Single.registerCE (Registers.descriptorPorts descriptor))
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted enable-wire
  with Generic.resolveScalarPort
    "register.control" (Generic.builderBindings current)
    (Single.registerControl (Registers.descriptorPorts descriptor))
...       | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...       | Diagnostic.accepted control-wire =
  Diagnostic.accepted
    (builtRegisters after-control
      (Checked.localWire fzero ∷ liftNextTwice next-wires))
  where
  after-enable : Generic.Builder inputCount registerCount
  after-enable =
    appendAnonymous current
      (Checked.muxNode enable-wire current-wire data-wire)

  after-control : Generic.Builder inputCount registerCount
  after-control =
    appendAnonymous after-enable
      (Checked.muxNode
        (Generic.liftLocalWire control-wire)
        (Checked.localWire fzero)
        (Checked.literalWire
          (Single.modeForcedValue (Registers.descriptorMode descriptor))))

buildRegisterNodes : ∀ {inputCount registerCount}
  → (descriptors : List Registers.RegisterDescriptor)
  → Generic.Builder inputCount registerCount
  → Diagnostic.CheckResult
      (BuiltRegisters inputCount registerCount
        (lengthList descriptors))
buildRegisterNodes []ᴸ current =
  Diagnostic.accepted (builtRegisters current [])
buildRegisterNodes (descriptor ∷ᴸ descriptors) current with
  buildRegisterNodes descriptors current
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted built = finishRegisterNodes descriptor built

initialValues : (descriptors : List Registers.RegisterDescriptor)
  → Vec Bit (lengthList descriptors)
initialValues []ᴸ = []
initialValues (descriptor ∷ᴸ descriptors) =
  Single.modeInitial (Registers.descriptorMode descriptor)
  ∷ initialValues descriptors

resolveOutputConnections : ∀ {inputCount registerCount localCount}
  → String
  → Generic.Bindings inputCount registerCount localCount
  → List Raw.Connection
  → Diagnostic.CheckResult
      (List (Checked.Wire inputCount registerCount localCount))
resolveOutputConnections = TopInterface.resolveOutputConnections

collectOutputWires : ∀ {inputCount registerCount}
  → List Raw.RawTopPort
  → (current : Generic.Builder inputCount registerCount)
  → Diagnostic.CheckResult
      (List
        (Checked.Wire inputCount registerCount
          (Generic.builderLocalCount current)))
collectOutputWires = TopInterface.collectBuilderOutputWires

record CheckedMixedCandidate : Type₀ where
  constructor checkedMixedCandidate
  field
    candidateSource          : Raw.RawDesign
    candidateStructuralProof : Validation.StructurallyValid candidateSource
    candidateInputCount      : ℕ
    candidateOutputCount     : ℕ
    candidateRegisterCount   : ℕ
    candidateLocalCount      : ℕ
    candidateClockInput      : Fin candidateInputCount
    candidateNetlist         :
      Checked.CheckedNetlist
        candidateInputCount candidateOutputCount
        candidateRegisterCount candidateLocalCount

open CheckedMixedCandidate public

finishCandidate :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (input-nets : List Raw.NetId)
  → (registers : List Registers.RegisterDescriptor)
  → Fin (lengthList input-nets)
  → (built :
      BuiltRegisters
        (lengthList input-nets) (lengthList registers)
        (lengthList registers))
  → (outputs :
      List
        (Checked.Wire
          (lengthList input-nets) (lengthList registers)
          (Generic.builderLocalCount (builtBuilder built))))
  → CheckedMixedCandidate
finishCandidate design structural-proof input-nets registers clock-index
  built outputs =
  checkedMixedCandidate
    design structural-proof
    (lengthList input-nets)
    (lengthList outputs)
    (lengthList registers)
    (Generic.builderLocalCount (builtBuilder built))
    clock-index
    (Checked.checkedNetlist
      (initialValues registers)
      (Generic.builderNodes (builtBuilder built))
      (TopInterface.listToVec outputs)
      (builtNext built))

normaliseBuiltCombinational :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → (input-nets : List Raw.NetId)
  → (registers : List Registers.RegisterDescriptor)
  → Fin (lengthList input-nets)
  → Generic.Builder (lengthList input-nets) (lengthList registers)
  → Diagnostic.CheckResult CheckedMixedCandidate
normaliseBuiltCombinational design structural-proof input-nets registers
  clock-index combinational-builder with
  buildRegisterNodes registers combinational-builder
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted built with
  collectOutputWires (Raw.rawTopPorts design) (builtBuilder built)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted outputs =
  Diagnostic.accepted
    (finishCandidate
      design structural-proof input-nets registers clock-index built outputs)

normalisePartition :
  (design : Raw.RawDesign)
  → Validation.StructurallyValid design
  → List Raw.NetId
  → InstancePartition
  → Diagnostic.CheckResult CheckedMixedCandidate
normalisePartition design structural-proof input-nets partition with
  Registers.commonClock input-nets (partitionRegisters partition)
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted clock-index with
  Schedule.scheduleInstances
    (mixedInitialBuilder input-nets (partitionRegisters partition))
    (partitionCombinational partition)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted scheduled =
  normaliseBuiltCombinational
    design structural-proof input-nets (partitionRegisters partition)
    clock-index (Schedule.finalBuilder scheduled)

normaliseMixed : Validation.StructurallyChecked
               → Diagnostic.CheckResult CheckedMixedCandidate
normaliseMixed (design , structural-proof) with
  TopInterface.checkDevelopmentTarget design
... | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
... | Diagnostic.accepted tt with
  TopInterface.collectInputNets (Raw.rawTopPorts design)
...   | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...   | Diagnostic.accepted input-nets with
  partitionInstances (Raw.rawInstances design)
...     | Diagnostic.rejected diagnostics = Diagnostic.rejected diagnostics
...     | Diagnostic.accepted partition =
  normalisePartition design structural-proof input-nets partition