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

module Spartan6.Examples.RawOBUFDS 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.BuildOBUFDS as Build
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.Semantics.Design as Semantics
open import Spartan6.Validation.CheckResult using (accepted?)
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
import Spartan6.Validation.Raw as Validation

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

outputPort : String → Raw.NetId → Raw.RawPort
outputPort name net-id =
  Raw.rawPort name Raw.outputPort 1 (Raw.net net-id ∷ᴸ []ᴸ)

canonicalPorts : Raw.NetId → Raw.NetId → Raw.NetId
               → List Raw.RawPort
canonicalPorts input-net positive-net negative-net =
  inputPort "I" (Raw.net input-net)
  ∷ᴸ outputPort "O" positive-net
  ∷ᴸ outputPort "OB" negative-net
  ∷ᴸ []ᴸ

rawOBUFDS : Raw.RawInstance
rawOBUFDS =
  Raw.rawInstance
    "diff_out"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (canonicalPorts 0 1 2)
    []ᴸ
    nothing

rawOBUFDSDesign : Raw.RawDesign
rawOBUFDSDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "positive" Raw.outputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "negative" Raw.outputPort 1 (Raw.net 2 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawOBUFDS ∷ᴸ []ᴸ)

raw-obufds-is-structurally-valid :
  Validation.StructurallyValid rawOBUFDSDesign
raw-obufds-is-structurally-valid = refl

initialBuilder : Generic.Builder 1 0
initialBuilder = Generic.initialBuilder (0 ∷ᴸ []ᴸ) []ᴸ

expectedBuilder : Generic.Builder 1 0
expectedBuilder =
  Generic.builder
    1
    (Checked.noNodes Checked.▻
      Checked.invertNode (Checked.externalWire fzero))
    (Generic.bindNet 2 (Checked.localWire fzero)
     ∷ᴸ Generic.bindNet 1 (Checked.externalWire fzero)
     ∷ᴸ Generic.bindNet 0 (Checked.externalWire fzero)
     ∷ᴸ []ᴸ)

raw-obufds-builds :
  Build.processOBUFDS rawOBUFDS initialBuilder
  ≡ Diagnostic.accepted expectedBuilder
raw-obufds-builds = refl

accepted-mode-follows-from-success : Build.AcceptedOBUFDSMode rawOBUFDS
accepted-mode-follows-from-success =
  Build.processOBUFDS-mode-sound
    rawOBUFDS initialBuilder expectedBuilder raw-obufds-builds

-- The original raw output IDs remain separate keys.  O aliases the resolved
-- input wire, whereas OB identifies the new local inversion node.

positive-net-retains-input-provenance :
  Generic.lookupNet 1 (Generic.builderBindings expectedBuilder)
  ≡ just (Checked.externalWire fzero)
positive-net-retains-input-provenance = refl

negative-net-retains-inverter-provenance :
  Generic.lookupNet 2 (Generic.builderBindings expectedBuilder)
  ≡ just (Checked.localWire fzero)
negative-net-retains-inverter-provenance = refl

negative-path-is-an-explicit-inverter :
  Generic.builderNodes expectedBuilder
  ≡ (Checked.noNodes Checked.▻
      Checked.invertNode (Checked.externalWire fzero))
negative-path-is-an-explicit-inverter = refl

obufdsNetlist : Checked.CheckedNetlist 1 2 0 1
obufdsNetlist =
  Checked.checkedNetlist
    []
    (Generic.builderNodes expectedBuilder)
    (Checked.externalWire fzero ∷ Checked.localWire fzero ∷ [])
    []

compiledOBUFDS : Semantics.Design 1 2 0
compiledOBUFDS = Checked.compileNetlist obufdsNetlist

compiled-low-has-complementary-outputs :
  Semantics.observe compiledOBUFDS (low ∷ []) []
  ≡ low ∷ high ∷ []
compiled-low-has-complementary-outputs = refl

compiled-high-has-complementary-outputs :
  Semantics.observe compiledOBUFDS (high ∷ []) []
  ≡ high ∷ low ∷ []
compiled-high-has-complementary-outputs = refl

-- Electrical attributes are not silently ignored.  The isolated mode accepts
-- no string parameters and no stored initial bit.

rawOBUFDSWithElectricalAttribute : Raw.RawInstance
rawOBUFDSWithElectricalAttribute =
  Raw.rawInstance
    "diff_out_attribute"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (canonicalPorts 0 1 2)
    (Raw.rawParameter "IOSTANDARD" "LVDS_25" ∷ᴸ []ᴸ)
    nothing

electrical-attribute-is-rejected :
  Build.processOBUFDS rawOBUFDSWithElectricalAttribute initialBuilder
  ≡ Diagnostic.rejected
      (Parameter.illegalParameterlessParameters "diff_out_attribute")
electrical-attribute-is-rejected = refl

rawOBUFDSWithInitialBit : Raw.RawInstance
rawOBUFDSWithInitialBit =
  Raw.rawInstance
    "diff_out_initial"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (canonicalPorts 0 1 2)
    []ᴸ
    (just low)

initial-bit-is-rejected :
  Build.processOBUFDS rawOBUFDSWithInitialBit initialBuilder
  ≡ Diagnostic.rejected
      (Parameter.unexpectedParameterlessInitialBit "diff_out_initial")
initial-bit-is-rejected = refl

rawOBUFDSMissingOB : Raw.RawInstance
rawOBUFDSMissingOB =
  Raw.rawInstance
    "diff_out_missing_ob"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (inputPort "I" (Raw.net 0)
     ∷ᴸ outputPort "O" 1
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

missing-negative-port-is-rejected :
  Build.processOBUFDS rawOBUFDSMissingOB initialBuilder
  ≡ Diagnostic.rejected
      (Validation.instanceStructuralDiagnostics rawOBUFDSMissingOB)
missing-negative-port-is-rejected = refl

rawOBUFDSUnresolvedInput : Raw.RawInstance
rawOBUFDSUnresolvedInput =
  Raw.rawInstance
    "diff_out_unresolved"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (canonicalPorts 99 1 2)
    []ᴸ
    nothing

unresolved-input-is-rejected :
  Build.processOBUFDS rawOBUFDSUnresolvedInput initialBuilder
  ≡ Diagnostic.rejected
      (Generic.unresolvedConnection "OBUFDS.I" (Raw.net 99))
unresolved-input-is-rejected = refl

rawOBUFDSSameOutputNet : Raw.RawInstance
rawOBUFDSSameOutputNet =
  Raw.rawInstance
    "diff_out_same_net"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (canonicalPorts 0 1 1)
    []ᴸ
    nothing

shared-output-net-is-rejected :
  Build.processOBUFDS rawOBUFDSSameOutputNet initialBuilder
  ≡ Diagnostic.rejected (Build.sameOutputNetDiagnostics 1)
shared-output-net-is-rejected = refl

-- OBUFT remains a different, unsupported behavior with no high-impedance
-- approximation in this slice.

rawOBUFT : Raw.RawInstance
rawOBUFT =
  Raw.rawInstance
    "tri_state"
    (Raw.knownPrimitive Architecture.OBUFT)
    []ᴸ []ᴸ nothing

obuft-is-not-translated :
  Build.processOBUFDS rawOBUFT initialBuilder
  ≡ Diagnostic.rejected (Build.wrongPrimitiveDiagnostics "tri_state")
obuft-is-not-translated = refl

-- End-to-end exact-design admission now uses the same witnessed OBUFDS mode
-- through GenericBuilder and the scheduled pure route.

obufdsCandidate : Candidate.CheckedCombinationalCandidate
obufdsCandidate =
  Candidate.checkedCombinationalCandidate
    rawOBUFDSDesign raw-obufds-is-structurally-valid
    1 2 1 obufdsNetlist

raw-obufds-normalises-through-generic-schedule :
  Normalize.normaliseScheduledCombinational
    (rawOBUFDSDesign , raw-obufds-is-structurally-valid)
  ≡ Diagnostic.accepted obufdsCandidate
raw-obufds-normalises-through-generic-schedule = refl

obufdsWitness :
  Soundness.ScheduledCombinationalBuildWitness
    rawOBUFDSDesign raw-obufds-is-structurally-valid obufdsCandidate
obufdsWitness =
  Soundness.normaliseScheduledCombinational-witness
    (rawOBUFDSDesign , raw-obufds-is-structurally-valid)
    obufdsCandidate
    raw-obufds-normalises-through-generic-schedule

obufdsProfile :
  CombinationalAdmission.RestrictedCombinationalProfile rawOBUFDSDesign
obufdsProfile =
  CombinationalAdmission.restrictedCombinationalProfile
    raw-obufds-is-structurally-valid
    obufdsCandidate
    raw-obufds-normalises-through-generic-schedule
    obufdsWitness
    CombinationalAdmission.restrictedCombinationalCandidate

obufdsCombinationalAdmission :
  CombinationalAdmission.RestrictedCombinationalAdmission
obufdsCombinationalAdmission = rawOBUFDSDesign , obufdsProfile

obufdsCoreAdmission : Admission.RestrictedCoreAdmission
obufdsCoreAdmission =
  Admission.admittedCombinational obufdsCombinationalAdmission

raw-obufds-is-unified-exact-design-admitted :
  Admission.admitRestrictedCore
    (rawOBUFDSDesign , raw-obufds-is-structurally-valid)
  ≡ Diagnostic.accepted obufdsCoreAdmission
raw-obufds-is-unified-exact-design-admitted = refl

admitted-obufds-low-is-complementary :
  Semantics.observe
    (Admission.executableDesign
      (Admission.admittedExecutable obufdsCoreAdmission))
    (low ∷ []) []
  ≡ low ∷ high ∷ []
admitted-obufds-low-is-complementary = refl

admitted-obufds-high-is-complementary :
  Semantics.observe
    (Admission.executableDesign
      (Admission.admittedExecutable obufdsCoreAdmission))
    (high ∷ []) []
  ≡ high ∷ low ∷ []
admitted-obufds-high-is-complementary = refl

canonicalRawOBUFT : Raw.RawInstance
canonicalRawOBUFT =
  Raw.rawInstance
    "tri_state_canonical"
    (Raw.knownPrimitive Architecture.OBUFT)
    (inputPort "I" (Raw.net 0)
     ∷ᴸ inputPort "T" (Raw.constant low)
     ∷ᴸ outputPort "O" 1
     ∷ᴸ []ᴸ)
    []ᴸ nothing

canonicalOBUFTDesign : Raw.RawDesign
canonicalOBUFTDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1 (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort 1 (Raw.net 1 ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (canonicalRawOBUFT ∷ᴸ []ᴸ)

canonical-obuft-is-structurally-valid :
  Validation.StructurallyValid canonicalOBUFTDesign
canonical-obuft-is-structurally-valid = refl

obuft-remains-unified-rejected :
  accepted?
    (Admission.admitRestrictedCore
      (canonicalOBUFTDesign , canonical-obuft-is-structurally-valid))
  ≡ false
obuft-remains-unified-rejected = refl