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

module Spartan6.Examples.ImportedYosys where

open import Spartan6.Prelude

import Spartan6.Import.YosysCorpus as Corpus
import Spartan6.Netlist.AdmissionCore as Core
import Spartan6.Netlist.AdmissionMixed as Admission
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeMixed as Normalize
import Spartan6.Netlist.NormalizeMixedSoundness as Soundness
import Spartan6.Netlist.Raw as Raw
import Spartan6.Primitive.LUT as LUT
import Spartan6.Semantics.Design as Semantics
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

-- Corpus.toggleRawDesign is an explicit small term.  The safe corpus
-- certificate contains the sole equality proving that the generated ff-json
-- tree decodes to this exact term, plus no-fallback acceptance/extraction
-- evidence.  Semantic proofs below therefore do not renormalize the JSON.

importedRawDesign : Raw.RawDesign
importedRawDesign = Corpus.toggleRawDesign

imported-is-structurally-valid :
  Validation.StructurallyValid importedRawDesign
imported-is-structurally-valid = refl

clockIndex resetIndex enableIndex : Fin 
clockIndex = fzero
resetIndex = fsuc fzero
enableIndex = fsuc (fsuc fzero)

-- Yosys emits LUT2 INIT=0110 (canonical hexadecimal 6) for Q XOR
-- toggle_enable and one low-initialized FDRE.  Register Q is allocated before
-- scheduling, so the LUT may read current Q while its result drives D.

importedNetlist : Checked.CheckedNetlist    
importedNetlist =
  Checked.checkedNetlist
    (low ∷ [])
    (((Checked.noNodes Checked.▻
      Checked.lutNode
        LUT.xorTable
        (Checked.storedWire fzero
         ∷ Checked.externalWire enableIndex
         ∷ []))
      Checked.▻
      Checked.muxNode
        (Checked.literalWire high)
        (Checked.storedWire fzero)
        (Checked.localWire fzero))
      Checked.▻
      Checked.muxNode
        (Checked.externalWire resetIndex)
        (Checked.localWire fzero)
        (Checked.literalWire low))
    (Checked.storedWire fzero ∷ [])
    (Checked.localWire fzero ∷ [])

importedCandidate : Normalize.CheckedMixedCandidate
importedCandidate =
  Normalize.checkedMixedCandidate
    importedRawDesign imported-is-structurally-valid
        clockIndex importedNetlist

imported-yosys-normalises :
  Normalize.normaliseMixed
    (importedRawDesign , imported-is-structurally-valid)
  ≡ Diagnostic.accepted importedCandidate
imported-yosys-normalises = refl

importedWitness :
  Soundness.MixedBuildWitness
    importedRawDesign imported-is-structurally-valid importedCandidate
importedWitness =
  Soundness.normaliseMixed-witness
    (importedRawDesign , imported-is-structurally-valid)
    importedCandidate imported-yosys-normalises

importedProfile : Admission.RestrictedMixedProfile importedRawDesign
importedProfile =
  Admission.restrictedMixedProfile
    imported-is-structurally-valid
    importedCandidate
    imported-yosys-normalises
    importedWitness
    Admission.restrictedTranslationCandidate

importedAdmission : Admission.RestrictedMixedAdmission
importedAdmission = importedRawDesign , importedProfile

real-yosys-artifact-is-core-admitted :
  Core.admitRestrictedCore
    (importedRawDesign , imported-is-structurally-valid)
  ≡ Diagnostic.accepted (Core.admittedMixed importedAdmission)
real-yosys-artifact-is-core-admitted = refl

importedExecutable : Core.ExecutableCore
importedExecutable =
  Core.admittedExecutable (Core.admittedMixed importedAdmission)

initial-imported-output-is-low :
  Semantics.observe
    (Core.executableDesign importedExecutable)
    (low ∷ low ∷ low ∷ [])
    (Semantics.initial (Core.executableDesign importedExecutable))
  ≡ low ∷ []
initial-imported-output-is-low = refl

enabled-edge-toggles-high :
  Semantics.step
    (Core.executableDesign importedExecutable)
    Semantics.risingEdge
    (high ∷ low ∷ high ∷ [])
    (low ∷ [])
  ≡ high ∷ []
enabled-edge-toggles-high = refl

second-enabled-edge-toggles-low :
  Semantics.step
    (Core.executableDesign importedExecutable)
    Semantics.risingEdge
    (high ∷ low ∷ high ∷ [])
    (high ∷ [])
  ≡ low ∷ []
second-enabled-edge-toggles-low = refl

reset-overrides-toggle :
  Semantics.step
    (Core.executableDesign importedExecutable)
    Semantics.risingEdge
    (high ∷ high ∷ high ∷ [])
    (high ∷ [])
  ≡ low ∷ []
reset-overrides-toggle = refl

-- A second real Yosys artefact contains the Xilinx INV cell, which is not in
-- the current raw primitive universe.  The safe decoder preserves it as an
-- unknown primitive and structural validation rejects it explicitly rather
-- than rewriting it silently.

unknownRawDesign : Raw.RawDesign
unknownRawDesign = Corpus.unknownRawDesign

unknown-inverter-diagnostic : Diagnostic.Diagnostic
unknown-inverter-diagnostic =
  Validation.issue
    Diagnostic.unknownPrimitive
    "$abc$1406$auto$blifparse.cc:557:parse_blif$1407"
    "a primitive kind in the selected architecture profile"
    "INV"
    "Unknown kinds are rejected rather than approximated."

unknown-inverter-structure-diagnostics :
  Validation.structureDiagnostics unknownRawDesign
  ≡ Validation.singleton unknown-inverter-diagnostic
unknown-inverter-structure-diagnostics = refl

unknown-inverter-is-rejected :
  Validation.validateStructure unknownRawDesign
  ≡ Diagnostic.rejected
      (Validation.singleton unknown-inverter-diagnostic)
unknown-inverter-is-rejected = refl