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

module Spartan6.Examples.RawCarry4 where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.AdmissionCombinational as CombinationalAdmission
import Spartan6.Netlist.AdmissionCore as Admission
import Spartan6.Netlist.Carry4Builder as Builder
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.GenericBuilder as Generic
import Spartan6.Netlist.NormalizeCombinational as Candidate
import Spartan6.Netlist.NormalizeScheduledCombinational as Normalize
import Spartan6.Netlist.NormalizeScheduledCombinationalSoundness as Soundness
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.Carry4 as Carry
import Spartan6.Semantics.Design as Semantics
open import Spartan6.Validation.CheckResult using (accepted?)
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

inputScalar : String → Raw.Connection → Raw.RawPort
inputScalar name connection =
  Raw.rawPort name Raw.inputPort 1 (connection ∷ᴸ []ᴸ)

inputFour : String
  → Raw.Connection → Raw.Connection
  → Raw.Connection → Raw.Connection
  → Raw.RawPort
inputFour name c0 c1 c2 c3 =
  Raw.rawPort name Raw.inputPort 4
    (c0 ∷ᴸ c1 ∷ᴸ c2 ∷ᴸ c3 ∷ᴸ []ᴸ)

outputFour : String
  → Raw.NetId → Raw.NetId → Raw.NetId → Raw.NetId
  → Raw.RawPort
outputFour name n0 n1 n2 n3 =
  Raw.rawPort name Raw.outputPort 4
    (Raw.net n0 ∷ᴸ Raw.net n1 ∷ᴸ Raw.net n2
     ∷ᴸ Raw.net n3 ∷ᴸ []ᴸ)

rawCarry4 : Raw.Connection → Raw.Connection
  → List Raw.RawParameter → Maybe Bit
  → Raw.RawInstance
rawCarry4 ci cyinit parameters initial-bit =
  Raw.rawInstance
    "carry"
    (Raw.knownPrimitive Architecture.CARRY4)
    (inputScalar "CI" ci
     ∷ᴸ inputScalar "CYINIT" cyinit
     ∷ᴸ inputFour "DI"
         (Raw.constant low) (Raw.constant low)
         (Raw.constant low) (Raw.constant low)
     ∷ᴸ inputFour "S"
         (Raw.constant high) (Raw.constant high)
         (Raw.constant high) (Raw.constant high)
     ∷ᴸ outputFour "O" 0 1 2 3
     ∷ᴸ outputFour "CO" 4 5 6 7
     ∷ᴸ []ᴸ)
    parameters initial-bit

emptyBuilder : Generic.Builder 0 0
emptyBuilder = Generic.initialBuilder []ᴸ []ᴸ

literalWires : ∀ {count}
  → Vec Bit count → Vec (Checked.Wire 0 0 0) count
literalWires = map Checked.literalWire

oNets : Vec Raw.NetId 4
oNets = 0 ∷ 1 ∷ 2 ∷ 3 ∷ []

coNets : Vec Raw.NetId 4
coNets = 4 ∷ 5 ∷ 6 ∷ 7 ∷ []

literalCarryBuilder : Bit → Vec Bit 4 → Vec Bit 4
                    → Generic.Builder 0 0
literalCarryBuilder entry di select =
  Builder.buildCarry4
    emptyBuilder
    (Checked.literalWire entry)
    (literalWires di)
    (literalWires select)
    oNets coNets

positiveRawCarry4 : Raw.RawInstance
positiveRawCarry4 =
  rawCarry4 (Raw.constant high) (Raw.constant low) []ᴸ nothing

positiveExpectedBuilder : Generic.Builder 0 0
positiveExpectedBuilder =
  literalCarryBuilder high Carry.allLow4 Carry.allHigh4

positive-builds-eight-stages :
  Diagnostic.mapResult Builder.carryBuilder
    (Builder.processCARRY4 positiveRawCarry4 emptyBuilder)
  ≡ Diagnostic.accepted positiveExpectedBuilder
positive-builds-eight-stages = refl

simultaneousRawCarry4 : Raw.RawInstance
simultaneousRawCarry4 =
  rawCarry4 (Raw.constant high) (Raw.constant high) []ᴸ nothing

simultaneous-entry-is-rejected :
  accepted? (Builder.processCARRY4 simultaneousRawCarry4 emptyBuilder)
  ≡ false
simultaneous-entry-is-rejected = refl

parameterizedRawCarry4 : Raw.RawInstance
parameterizedRawCarry4 =
  rawCarry4
    (Raw.constant high) (Raw.constant low)
    (Raw.rawParameter "UNSUPPORTED" "1" ∷ᴸ []ᴸ)
    nothing

nonempty-parameters-are-rejected :
  accepted? (Builder.processCARRY4 parameterizedRawCarry4 emptyBuilder)
  ≡ false
nonempty-parameters-are-rejected = refl

bothLowRawCarry4 : Raw.RawInstance
bothLowRawCarry4 =
  rawCarry4 (Raw.constant low) (Raw.constant low) []ᴸ nothing

both-low-records-CI-provenance :
  Diagnostic.mapResult Builder.carry-build-entry-provenance
    (Builder.processCARRY4 bothLowRawCarry4 emptyBuilder)
  ≡ Diagnostic.accepted Builder.ciSource
both-low-records-CI-provenance = refl

cyinitRawCarry4 : Raw.RawInstance
cyinitRawCarry4 =
  rawCarry4 (Raw.constant low) (Raw.constant high) []ᴸ nothing

literal-low-CI-records-CYINIT-provenance :
  Diagnostic.mapResult Builder.carry-build-entry-provenance
    (Builder.processCARRY4 cyinitRawCarry4 emptyBuilder)
  ≡ Diagnostic.accepted Builder.cyinitSource
literal-low-CI-records-CYINIT-provenance = refl

local0 local1 local2 local3 local4 local5 local6 local7 : Fin 8
local0 = fzero
local1 = fsuc fzero
local2 = fsuc (fsuc fzero)
local3 = fsuc (fsuc (fsuc fzero))
local4 = fsuc (fsuc (fsuc (fsuc fzero)))
local5 = fsuc (fsuc (fsuc (fsuc (fsuc fzero))))
local6 = fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero)))))
local7 = fsuc (fsuc (fsuc (fsuc (fsuc (fsuc (fsuc fzero))))))

outputWires : Vec (Checked.Wire 0 0 8) 8
outputWires =
  Checked.localWire local7
  ∷ Checked.localWire local5
  ∷ Checked.localWire local3
  ∷ Checked.localWire local1
  ∷ Checked.localWire local6
  ∷ Checked.localWire local4
  ∷ Checked.localWire local2
  ∷ Checked.localWire local0
  ∷ []

lookupNets : ∀ {inputCount registerCount localCount count}
  → Vec Raw.NetId count
  → Generic.Bindings inputCount registerCount localCount
  → Vec
      (Maybe (Checked.Wire inputCount registerCount localCount))
      count
lookupNets [] bindings = []
lookupNets (net-id ∷ net-ids) bindings =
  Generic.lookupNet net-id bindings ∷ lookupNets net-ids bindings

allOutputNets : Vec Raw.NetId 8
allOutputNets = 0 ∷ 1 ∷ 2 ∷ 3 ∷ 4 ∷ 5 ∷ 6 ∷ 7 ∷ []

all-eight-raw-outputs-are-bound :
  lookupNets allOutputNets
    (Generic.builderBindings positiveExpectedBuilder)
  ≡ map just outputWires
all-eight-raw-outputs-are-bound = refl

literalCarryNetlist : Bit → Vec Bit 4 → Vec Bit 4
                    → Checked.CheckedNetlist 0 8 0 8
literalCarryNetlist entry
  di@(di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
  select@(s0 ∷ s1 ∷ s2 ∷ s3 ∷ []) =
  Checked.checkedNetlist
    []
    (Generic.builderNodes (literalCarryBuilder entry di select))
    outputWires
    []

flattenCarryOutput : Carry.Carry4Output → Vec Bit 8
flattenCarryOutput
  (Carry.carry4Output
    (o0 ∷ o1 ∷ o2 ∷ o3 ∷ [])
    (co0 ∷ co1 ∷ co2 ∷ co3 ∷ [])) =
  o0 ∷ o1 ∷ o2 ∷ o3
  ∷ co0 ∷ co1 ∷ co2 ∷ co3 ∷ []

literal-builder-corresponds-to-UG615 :
  ∀ entry di select
  → Semantics.observe
      (Checked.compileNetlist (literalCarryNetlist entry di select))
      [] []
    ≡ flattenCarryOutput
        (Carry.evalCarry4 (Carry.fromCI entry) di select)
literal-builder-corresponds-to-UG615 entry
  (di0 ∷ di1 ∷ di2 ∷ di3 ∷ [])
  (s0 ∷ s1 ∷ s2 ∷ s3 ∷ []) = refl

positive-observation :
  Semantics.observe
    (Checked.compileNetlist
      (literalCarryNetlist high Carry.allLow4 Carry.allHigh4))
    [] []
  ≡ low ∷ low ∷ low ∷ low
    ∷ high ∷ high ∷ high ∷ high ∷ []
positive-observation = refl

-- End-to-end exact-design admission through the unified scheduled core.

topOutput : String → Raw.NetId → Raw.RawTopPort
topOutput name net-id =
  Raw.rawTopPort name Raw.outputPort 1 (Raw.net net-id ∷ᴸ []ᴸ)

carryTopOutputs : List Raw.RawTopPort
carryTopOutputs =
  topOutput "O0" 0 ∷ᴸ topOutput "O1" 1
  ∷ᴸ topOutput "O2" 2 ∷ᴸ topOutput "O3" 3
  ∷ᴸ topOutput "CO0" 4 ∷ᴸ topOutput "CO1" 5
  ∷ᴸ topOutput "CO2" 6 ∷ᴸ topOutput "CO3" 7
  ∷ᴸ []ᴸ

positiveCarryDesign : Raw.RawDesign
positiveCarryDesign =
  Raw.rawDesign nothing carryTopOutputs (positiveRawCarry4 ∷ᴸ []ᴸ)

positive-carry-is-structurally-valid :
  Validation.StructurallyValid positiveCarryDesign
positive-carry-is-structurally-valid = refl

positiveCarryCandidate : Candidate.CheckedCombinationalCandidate
positiveCarryCandidate =
  Candidate.checkedCombinationalCandidate
    positiveCarryDesign positive-carry-is-structurally-valid
    0 8 8
    (literalCarryNetlist high Carry.allLow4 Carry.allHigh4)

positive-carry-normalises-through-generic-schedule :
  Normalize.normaliseScheduledCombinational
    (positiveCarryDesign , positive-carry-is-structurally-valid)
  ≡ Diagnostic.accepted positiveCarryCandidate
positive-carry-normalises-through-generic-schedule = refl

positiveCarryWitness :
  Soundness.ScheduledCombinationalBuildWitness
    positiveCarryDesign positive-carry-is-structurally-valid
    positiveCarryCandidate
positiveCarryWitness =
  Soundness.normaliseScheduledCombinational-witness
    (positiveCarryDesign , positive-carry-is-structurally-valid)
    positiveCarryCandidate
    positive-carry-normalises-through-generic-schedule

positiveCarryProfile :
  CombinationalAdmission.RestrictedCombinationalProfile
    positiveCarryDesign
positiveCarryProfile =
  CombinationalAdmission.restrictedCombinationalProfile
    positive-carry-is-structurally-valid
    positiveCarryCandidate
    positive-carry-normalises-through-generic-schedule
    positiveCarryWitness
    CombinationalAdmission.restrictedCombinationalCandidate

positiveCarryCombinationalAdmission :
  CombinationalAdmission.RestrictedCombinationalAdmission
positiveCarryCombinationalAdmission =
  positiveCarryDesign , positiveCarryProfile

positiveCarryCoreAdmission : Admission.RestrictedCoreAdmission
positiveCarryCoreAdmission =
  Admission.admittedCombinational positiveCarryCombinationalAdmission

positive-carry-is-unified-exact-design-admitted :
  Admission.admitRestrictedCore
    (positiveCarryDesign , positive-carry-is-structurally-valid)
  ≡ Diagnostic.accepted positiveCarryCoreAdmission
positive-carry-is-unified-exact-design-admitted = refl

admitted-positive-carry-executes-expected-outputs :
  Semantics.observe
    (Admission.executableDesign
      (Admission.admittedExecutable positiveCarryCoreAdmission))
    [] []
  ≡ low ∷ low ∷ low ∷ low
    ∷ high ∷ high ∷ high ∷ high ∷ []
admitted-positive-carry-executes-expected-outputs = refl

simultaneousCarryDesign : Raw.RawDesign
simultaneousCarryDesign =
  Raw.rawDesign nothing carryTopOutputs
    (simultaneousRawCarry4 ∷ᴸ []ᴸ)

simultaneous-carry-is-structurally-valid :
  Validation.StructurallyValid simultaneousCarryDesign
simultaneous-carry-is-structurally-valid = refl

simultaneous-carry-remains-unified-rejected :
  accepted?
    (Admission.admitRestrictedCore
      (simultaneousCarryDesign
      , simultaneous-carry-is-structurally-valid))
  ≡ false
simultaneous-carry-remains-unified-rejected = refl