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

module Spartan6.Examples.RawLUT where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeCombinational as Normalize
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

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

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

-- INIT 0xAAAA... has vendor-index bits 0,1,0,1,... and therefore implements
-- O=I0 independently of I1..I5 under the documented LUT address ordering.

rawIdentityLUT : Raw.RawInstance
rawIdentityLUT =
  Raw.rawInstance
    "identity"
    (Raw.knownPrimitive Architecture.LUT6)
    (inputPort "I0" (Raw.net )
     ∷ᴸ 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 )
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "AAAAAAAAAAAAAAAA" ∷ᴸ []ᴸ)
    nothing

rawIdentityDesign : Raw.RawDesign
rawIdentityDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawIdentityLUT ∷ᴸ []ᴸ)

raw-identity-is-structurally-valid :
  Validation.StructurallyValid rawIdentityDesign
raw-identity-is-structurally-valid = refl

alternatingPairs : (count : ℕ) → Vec Bit (count · )
alternatingPairs zero = []
alternatingPairs (suc count) = low ∷ high ∷ alternatingPairs count

identityTable : LUT.LUT6Table
identityTable = alternatingPairs 

identityNetlist : Checked.CheckedNetlist    
identityNetlist =
  Checked.checkedNetlist
    []
    (Checked.noNodes Checked.▻
      Checked.lutNode identityTable
        (Checked.externalWire fzero
         ∷ Checked.literalWire low
         ∷ Checked.literalWire low
         ∷ Checked.literalWire low
         ∷ Checked.literalWire low
         ∷ Checked.literalWire low
         ∷ []))
    (Checked.localWire fzero ∷ [])
    []

identityCandidate : Normalize.CheckedCombinationalCandidate
identityCandidate =
  Normalize.checkedCombinationalCandidate
    rawIdentityDesign
    raw-identity-is-structurally-valid
      
    identityNetlist

raw-identity-normalises :
  Normalize.normaliseCombinational
    (rawIdentityDesign , raw-identity-is-structurally-valid)
  ≡ Diagnostic.accepted identityCandidate
raw-identity-normalises = refl

compiledIdentity : Semantics.Design   
compiledIdentity = Checked.compileNetlist identityNetlist

compiled-identity-low :
  Semantics.observe compiledIdentity (low ∷ []) [] ≡ low ∷ []
compiled-identity-low = refl

compiled-identity-high :
  Semantics.observe compiledIdentity (high ∷ []) [] ≡ high ∷ []
compiled-identity-high = refl

rawIdentityStage : String → Raw.NetId → Raw.NetId → Raw.RawInstance
rawIdentityStage name input-net output-net =
  Raw.rawInstance
    name
    (Raw.knownPrimitive Architecture.LUT6)
    (inputPort "I0" (Raw.net input-net)
     ∷ᴸ 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 output-net)
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "AAAAAAAAAAAAAAAA" ∷ᴸ []ᴸ)
    nothing

forwardReferenceDesign : Raw.RawDesign
forwardReferenceDesign =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawIdentityStage "consumer"  
     ∷ᴸ rawIdentityStage "producer"  
     ∷ᴸ []ᴸ)

forward-reference-design-is-acyclic-and-structurally-valid :
  Validation.StructurallyValid forwardReferenceDesign
forward-reference-design-is-acyclic-and-structurally-valid = refl

forward-reference-needs-topological-order :
  Normalize.normaliseCombinational
    (forwardReferenceDesign ,
     forward-reference-design-is-acyclic-and-structurally-valid)
  ≡ Diagnostic.rejected
      (Normalize.unresolvedConnection "LUT6.I0" (Raw.net ))
forward-reference-needs-topological-order = refl

rawIdentityLUT2 : Raw.RawInstance
rawIdentityLUT2 =
  Raw.rawInstance
    "identity2"
    (Raw.knownPrimitive Architecture.LUT2)
    (inputPort "I0" (Raw.net )
     ∷ᴸ inputPort "I1" (Raw.constant low)
     ∷ᴸ outputPort "O" (Raw.net )
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "A" ∷ᴸ []ᴸ)
    nothing

rawIdentityLUT2Design : Raw.RawDesign
rawIdentityLUT2Design =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawIdentityLUT2 ∷ᴸ []ᴸ)

raw-lut2-is-structurally-valid :
  Validation.StructurallyValid rawIdentityLUT2Design
raw-lut2-is-structurally-valid = refl

identityLUT2Netlist : Checked.CheckedNetlist    
identityLUT2Netlist =
  Checked.checkedNetlist
    []
    (Checked.noNodes Checked.▻
      Checked.lutNode
        (low ∷ high ∷ low ∷ high ∷ [])
        (Checked.externalWire fzero ∷ Checked.literalWire low ∷ []))
    (Checked.localWire fzero ∷ [])
    []

identityLUT2Candidate : Normalize.CheckedCombinationalCandidate
identityLUT2Candidate =
  Normalize.checkedCombinationalCandidate
    rawIdentityLUT2Design raw-lut2-is-structurally-valid
       identityLUT2Netlist

raw-lut2-normalises :
  Normalize.normaliseCombinational
    (rawIdentityLUT2Design , raw-lut2-is-structurally-valid)
  ≡ Diagnostic.accepted identityLUT2Candidate
raw-lut2-normalises = refl

compiledLUT2 : Semantics.Design   
compiledLUT2 = Checked.compileNetlist identityLUT2Netlist

compiled-lut2-passes-high :
  Semantics.observe compiledLUT2 (high ∷ []) [] ≡ high ∷ []
compiled-lut2-passes-high = refl

rawInvertingLUT1 : Raw.RawInstance
rawInvertingLUT1 =
  Raw.rawInstance
    "not1"
    (Raw.knownPrimitive Architecture.LUT1)
    (inputPort "I0" (Raw.net )
     ∷ᴸ outputPort "O" (Raw.net )
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ)
    nothing

rawInvertingLUT1Design : Raw.RawDesign
rawInvertingLUT1Design =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort  (Raw.net  ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (rawInvertingLUT1 ∷ᴸ []ᴸ)

raw-lut1-is-structurally-valid :
  Validation.StructurallyValid rawInvertingLUT1Design
raw-lut1-is-structurally-valid = refl

invertingLUT1Netlist : Checked.CheckedNetlist    
invertingLUT1Netlist =
  Checked.checkedNetlist
    []
    (Checked.noNodes Checked.▻
      Checked.lutNode
        (high ∷ low ∷ [])
        (Checked.externalWire fzero ∷ []))
    (Checked.localWire fzero ∷ [])
    []

invertingLUT1Candidate : Normalize.CheckedCombinationalCandidate
invertingLUT1Candidate =
  Normalize.checkedCombinationalCandidate
    rawInvertingLUT1Design raw-lut1-is-structurally-valid
       invertingLUT1Netlist

raw-lut1-normalises :
  Normalize.normaliseCombinational
    (rawInvertingLUT1Design , raw-lut1-is-structurally-valid)
  ≡ Diagnostic.accepted invertingLUT1Candidate
raw-lut1-normalises = refl

compiledLUT1 : Semantics.Design   
compiledLUT1 = Checked.compileNetlist invertingLUT1Netlist

compiled-lut1-inverts-low :
  Semantics.observe compiledLUT1 (low ∷ []) [] ≡ high ∷ []
compiled-lut1-inverts-low = refl

compiled-lut1-inverts-high :
  Semantics.observe compiledLUT1 (high ∷ []) [] ≡ low ∷ []
compiled-lut1-inverts-high = refl