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

module Spartan6.Examples.Validation where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Architecture.Profile as Profile
import Spartan6.Netlist.NormalizeRegister as RegisterNormalize
import Spartan6.Netlist.Raw as Raw
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Parameter as Parameter
open import Spartan6.Validation.Raw

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

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

rawFDRE : Raw.RawInstance
rawFDRE =
  Raw.rawInstance
    "toggle.q"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" (Raw.net 2)
     ∷ᴸ inputPort "C" (Raw.net 1)
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.constant low)
     ∷ᴸ outputPort "Q" (Raw.net 2)
     ∷ᴸ []ᴸ)
    []ᴸ
    (just low)

rawFDREDesign : Raw.RawDesign
rawFDREDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clk" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ) ∷ᴸ []ᴸ)
    (rawFDRE ∷ᴸ []ᴸ)

raw-FDRE-is-structurally-valid : StructurallyValid rawFDREDesign
raw-FDRE-is-structurally-valid = refl

raw-FDRE-structure-is-accepted :
  validateStructure rawFDREDesign
  ≡ Diagnostic.accepted (rawFDREDesign , refl)
raw-FDRE-structure-is-accepted = refl

misnamedFDRE : Raw.RawInstance
misnamedFDRE =
  Raw.rawInstance
    "toggle.q"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "NOT_D" (Raw.net 2)
     ∷ᴸ inputPort "C" (Raw.net 1)
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.constant low)
     ∷ᴸ outputPort "Q" (Raw.net 2)
     ∷ᴸ []ᴸ)
    []ᴸ
    (just low)

misnamedFDREDesign : Raw.RawDesign
misnamedFDREDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPorts rawFDREDesign)
    (misnamedFDRE ∷ᴸ []ᴸ)

misnamed-port-is-rejected-even-at-equal-width :
  structureDiagnostics misnamedFDREDesign
  ≡ issue Diagnostic.unknownPort
          "NOT_D"
          "D"
          "NOT_D"
          "Primitive port names and order must both match the canonical architecture schema; equal widths do not make ports interchangeable."
    ∷ᴸ []ᴸ
misnamed-port-is-rejected-even-at-equal-width = refl

-- Semantic admission remains closed while FDRE is deliberately marked
-- partially supported: parsing C/INIT and translation into the typed core are
-- still proof obligations.

raw-FDRE-profile-diagnostic :
  profileDiagnostics rawFDREDesign
  ≡ issue Diagnostic.unsupportedMode
          "toggle.q"
          "fully supported mode"
          "partially supported mode"
          "Semantic code exists, but raw decoding/admission obligations remain incomplete."
    ∷ᴸ []ᴸ
raw-FDRE-profile-diagnostic = refl

rawFDREWithStringINIT : Raw.RawInstance
rawFDREWithStringINIT =
  Raw.rawInstance
    "toggle.q"
    (Raw.knownPrimitive Architecture.FDRE)
    (Raw.rawInstancePorts rawFDRE)
    (Raw.rawParameter "INIT" "0" ∷ᴸ []ᴸ)
    (just low)

rawFDREWithStringINITDesign : Raw.RawDesign
rawFDREWithStringINITDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPorts rawFDREDesign)
    (rawFDREWithStringINIT ∷ᴸ []ᴸ)

raw-FDRE-string-INIT-is-explicitly-rejected :
  profileDiagnostics rawFDREWithStringINITDesign
  ≡ issue Diagnostic.unsupportedMode
          "toggle.q"
          "fully supported mode"
          "partially supported mode"
          "Semantic code exists, but raw decoding/admission obligations remain incomplete."
    ∷ᴸ Parameter.illegalScalarRegisterParameters "toggle.q"
raw-FDRE-string-INIT-is-explicitly-rejected = refl

wrongTargetDesign : Raw.RawDesign
wrongTargetDesign =
  Raw.rawDesign (just "different-profile")
    (Raw.rawTopPorts rawFDREDesign)
    (Raw.rawInstances rawFDREDesign)

contradictory-target-is-explicitly-rejected :
  profileDiagnostics wrongTargetDesign
  ≡ issue Diagnostic.contradictoryTarget
          "raw target profile"
          "spartan6-level1-development"
          "different-profile"
          "An explicit raw target must match the selected validation profile; an absent architecture-only target remains permitted."
    ∷ᴸ issue Diagnostic.unsupportedMode
          "toggle.q"
          "fully supported mode"
          "partially supported mode"
          "Semantic code exists, but raw decoding/admission obligations remain incomplete."
    ∷ᴸ []ᴸ
contradictory-target-is-explicitly-rejected = refl

wrong-target-is-still-structurally-valid :
  StructurallyValid wrongTargetDesign
wrong-target-is-still-structurally-valid = refl

translation-candidate-rejects-contradictory-target :
  RegisterNormalize.normaliseSingleRegister
    (wrongTargetDesign , wrong-target-is-still-structurally-valid)
  ≡ Diagnostic.rejected
      (targetDiagnosticsFor Profile.developmentProfile wrongTargetDesign)
translation-candidate-rejects-contradictory-target = refl

unknownInstance : Raw.RawInstance
unknownInstance =
  Raw.rawInstance
    "mystery"
    (Raw.unknownPrimitive "MYSTERY_CELL")
    []ᴸ
    []ᴸ
    nothing

unknownDesign : Raw.RawDesign
unknownDesign =
  Raw.rawDesign nothing []ᴸ (unknownInstance ∷ᴸ []ᴸ)

unknown-kind-diagnostic :
  structureDiagnostics unknownDesign
  ≡ issue Diagnostic.unknownPrimitive
          "mystery"
          "a primitive kind in the selected architecture profile"
          "MYSTERY_CELL"
          "Unknown kinds are rejected rather than approximated."
    ∷ᴸ []ᴸ
unknown-kind-diagnostic = refl

disconnectedFDRE : Raw.RawInstance
disconnectedFDRE =
  Raw.rawInstance
    "bad.q"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputPort "D" Raw.disconnected
     ∷ᴸ inputPort "C" (Raw.net 1)
     ∷ᴸ inputPort "CE" (Raw.constant high)
     ∷ᴸ inputPort "R" (Raw.constant low)
     ∷ᴸ outputPort "Q" (Raw.net 2)
     ∷ᴸ []ᴸ)
    []ᴸ
    (just low)

disconnectedDesign : Raw.RawDesign
disconnectedDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clk" Raw.inputPort 1 (Raw.net 1 ∷ᴸ []ᴸ) ∷ᴸ []ᴸ)
    (disconnectedFDRE ∷ᴸ []ᴸ)

disconnected-input-diagnostic :
  structureDiagnostics disconnectedDesign
  ≡ issue Diagnostic.undrivenInput
          "D"
          "a net or two-valued constant for every bit"
          "at least one disconnected bit"
          "Required semantic inputs may not be silently unconstrained."
    ∷ᴸ []ᴸ
disconnected-input-diagnostic = refl

cyclicLUT6 : Raw.RawInstance
cyclicLUT6 =
  Raw.rawInstance
    "loop"
    (Raw.knownPrimitive Architecture.LUT6)
    (inputPort "I0" (Raw.net 0)
     ∷ᴸ inputPort "I1" (Raw.constant low)
     ∷ᴸ inputPort "I2" (Raw.constant low)
     ∷ᴸ inputPort "I3" (Raw.constant low)
     ∷ᴸ inputPort "I4" (Raw.constant low)
     ∷ᴸ inputPort "I5" (Raw.constant low)
     ∷ᴸ outputPort "O" (Raw.net 0)
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "0000000000000000" ∷ᴸ []ᴸ)
    nothing

cyclicDesign : Raw.RawDesign
cyclicDesign =
  Raw.rawDesign nothing []ᴸ (cyclicLUT6 ∷ᴸ []ᴸ)

combinational-loop-diagnostic :
  structureDiagnostics cyclicDesign
  ≡ issue Diagnostic.combinationalLoop
          "combinational dependency graph"
          "an acyclic graph"
          "a dependency cycle"
          "Dependencies through explicit storage state are excluded; purely combinational cycles are rejected."
    ∷ᴸ []ᴸ
combinational-loop-diagnostic = refl