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

module Spartan6.Benchmarks.Fixtures where

open import Spartan6.Prelude

import Spartan6.Architecture.Primitive as Architecture
import Spartan6.Netlist.Raw as Raw

-- Compact raw-design generators used to keep scale tests out of handwritten
-- fixture terms.  Net IDs, not diagnostic names, distinguish occurrences.

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

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

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 ∷ᴸ []ᴸ)

netConnectionsFrom : Raw.NetId -> ℕ -> List Raw.Connection
netConnectionsFrom first zero = []ᴸ
netConnectionsFrom first (suc count) =
  Raw.net first ∷ᴸ netConnectionsFrom (suc first) count

double : ℕ -> ℕ
double zero = zero
double (suc count) = suc (suc (double count))

eightfold : ℕ -> ℕ
eightfold zero = zero
eightfold (suc count) = 8 + eightfold count

addEight : ℕ -> ℕ
addEight value = 8 + value

identityLUT1 : Raw.NetId -> Raw.NetId -> Raw.RawInstance
identityLUT1 input-net output-net =
  Raw.rawInstance
    "benchmark.identity"
    (Raw.knownPrimitive Architecture.LUT1)
    (inputScalar "I0" (Raw.net input-net)
     ∷ᴸ outputScalar "O" output-net
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "2" ∷ᴸ []ᴸ)
    nothing

invertingLUT1 : Raw.NetId -> Raw.NetId -> Raw.RawInstance
invertingLUT1 input-net output-net =
  Raw.rawInstance
    "benchmark.invert"
    (Raw.knownPrimitive Architecture.LUT1)
    (inputScalar "I0" (Raw.net input-net)
     ∷ᴸ outputScalar "O" output-net
     ∷ᴸ []ᴸ)
    (Raw.rawParameter "INIT" "1" ∷ᴸ []ᴸ)
    nothing

orderedChainInstances : Raw.NetId -> ℕ -> List Raw.RawInstance
orderedChainInstances input-net zero = []ᴸ
orderedChainInstances input-net (suc count) =
  identityLUT1 input-net (suc input-net)
  ∷ᴸ orderedChainInstances (suc input-net) count

reverseChainInstances : Raw.NetId -> ℕ -> List Raw.RawInstance
reverseChainInstances input-net zero = []ᴸ
reverseChainInstances input-net (suc count) =
  reverseChainInstances (suc input-net) count
  ++ᴸ identityLUT1 input-net (suc input-net) ∷ᴸ []ᴸ

orderedChainDesign : ℕ -> Raw.RawDesign
orderedChainDesign count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1
       (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort 1
       (Raw.net count ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (orderedChainInstances 0 count)

reverseChainDesign : ℕ -> Raw.RawDesign
reverseChainDesign count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1
       (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "output" Raw.outputPort 1
       (Raw.net count ∷ᴸ []ᴸ)
     ∷ᴸ []ᴸ)
    (reverseChainInstances 0 count)

fanOutInstances : Raw.NetId -> ℕ -> List Raw.RawInstance
fanOutInstances output-net zero = []ᴸ
fanOutInstances output-net (suc count) =
  identityLUT1 0 output-net
  ∷ᴸ fanOutInstances (suc output-net) count

fanOutDesign : ℕ -> Raw.RawDesign
fanOutDesign count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1
       (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "outputs" Raw.outputPort count
       (netConnectionsFrom 1 count)
     ∷ᴸ []ᴸ)
    (fanOutInstances 1 count)

independentInstances : Raw.NetId -> Raw.NetId -> ℕ
  -> List Raw.RawInstance
independentInstances input-net output-net zero = []ᴸ
independentInstances input-net output-net (suc count) =
  identityLUT1 input-net output-net
  ∷ᴸ independentInstances (suc input-net) (suc output-net) count

independentDesign : ℕ -> Raw.RawDesign
independentDesign count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "inputs" Raw.inputPort count
       (netConnectionsFrom 0 count)
     ∷ᴸ Raw.rawTopPort "outputs" Raw.outputPort count
       (netConnectionsFrom count count)
     ∷ᴸ []ᴸ)
    (independentInstances 0 count count)

obufdsInstance : Raw.NetId -> Raw.NetId -> Raw.NetId
  -> Raw.RawInstance
obufdsInstance input-net positive-net negative-net =
  Raw.rawInstance
    "benchmark.OBUFDS"
    (Raw.knownPrimitive Architecture.OBUFDS)
    (inputScalar "I" (Raw.net input-net)
     ∷ᴸ outputScalar "O" positive-net
     ∷ᴸ outputScalar "OB" negative-net
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

multiOutputInstances : Raw.NetId -> ℕ -> List Raw.RawInstance
multiOutputInstances first-output zero = []ᴸ
multiOutputInstances first-output (suc count) =
  obufdsInstance 0 first-output (suc first-output)
  ∷ᴸ multiOutputInstances (suc (suc first-output)) count

multiOutputDesign : ℕ -> Raw.RawDesign
multiOutputDesign count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "input" Raw.inputPort 1
       (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "differential-outputs" Raw.outputPort
       (double count) (netConnectionsFrom 1 (double count))
     ∷ᴸ []ᴸ)
    (multiOutputInstances 1 count)

carry4Instance : Raw.Connection -> Raw.NetId -> Raw.RawInstance
carry4Instance entry first-output =
  Raw.rawInstance
    "benchmark.CARRY4"
    (Raw.knownPrimitive Architecture.CARRY4)
    (inputScalar "CI" entry
     ∷ᴸ inputScalar "CYINIT" (Raw.constant low)
     ∷ᴸ 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"
       first-output
       (suc first-output)
       (suc (suc first-output))
       (suc (suc (suc first-output)))
     ∷ᴸ outputFour "CO"
       (suc (suc (suc (suc first-output))))
       (suc (suc (suc (suc (suc first-output)))))
       (suc (suc (suc (suc (suc (suc first-output))))))
       (suc (suc (suc (suc (suc (suc (suc first-output)))))))
     ∷ᴸ []ᴸ)
    []ᴸ
    nothing

carry4ChainInstances : Raw.NetId -> Raw.Connection -> ℕ
  -> List Raw.RawInstance
carry4ChainInstances first-output entry zero = []ᴸ
carry4ChainInstances first-output entry (suc count) =
  carry4Instance entry first-output
  ∷ᴸ carry4ChainInstances
        (addEight first-output)
        (Raw.net
          (suc (suc (suc (suc (suc (suc (suc first-output))))))))
        count

repeatedCarry4Design : ℕ -> Raw.RawDesign
repeatedCarry4Design count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "outputs" Raw.outputPort (eightfold count)
       (netConnectionsFrom 0 (eightfold count))
     ∷ᴸ []ᴸ)
    (carry4ChainInstances 0 (Raw.constant high) count)

registerInstance : ℕ -> ℕ -> Raw.RawInstance
registerInstance register-count index =
  Raw.rawInstance
    "benchmark.register"
    (Raw.knownPrimitive Architecture.FDRE)
    (inputScalar "D" (Raw.net (suc (register-count + index)))
     ∷ᴸ inputScalar "C" (Raw.net 0)
     ∷ᴸ inputScalar "CE" (Raw.constant high)
     ∷ᴸ inputScalar "R" (Raw.constant low)
     ∷ᴸ outputScalar "Q" (suc index)
     ∷ᴸ []ᴸ)
    []ᴸ
    (just low)

registerInstances : ℕ -> ℕ -> ℕ -> List Raw.RawInstance
registerInstances register-count index zero = []ᴸ
registerInstances register-count index (suc remaining) =
  registerInstance register-count index
  ∷ᴸ registerInstances register-count (suc index) remaining

registerInverters : ℕ -> ℕ -> ℕ -> List Raw.RawInstance
registerInverters register-count index zero = []ᴸ
registerInverters register-count index (suc remaining) =
  invertingLUT1
    (suc index)
    (suc (register-count + index))
  ∷ᴸ registerInverters register-count (suc index) remaining

mixedRegisterDesign : ℕ -> Raw.RawDesign
mixedRegisterDesign register-count =
  Raw.rawDesign nothing
    (Raw.rawTopPort "clock" Raw.inputPort 1
       (Raw.net 0 ∷ᴸ []ᴸ)
     ∷ᴸ Raw.rawTopPort "registers" Raw.outputPort register-count
       (netConnectionsFrom 1 register-count)
     ∷ᴸ []ᴸ)
    (registerInstances register-count 0 register-count
     ++ᴸ registerInverters register-count 0 register-count)

-- Standard check-time terms.  Clients can use the generators directly for a
-- scale sweep without regenerating source files.

orderedChainBenchmark : Raw.RawDesign
orderedChainBenchmark = orderedChainDesign 32

reverseChainBenchmark : Raw.RawDesign
reverseChainBenchmark = reverseChainDesign 32

fanOutBenchmark : Raw.RawDesign
fanOutBenchmark = fanOutDesign 32

independentBenchmark : Raw.RawDesign
independentBenchmark = independentDesign 32

multiOutputBenchmark : Raw.RawDesign
multiOutputBenchmark = multiOutputDesign 16

repeatedCarry4Benchmark : Raw.RawDesign
repeatedCarry4Benchmark = repeatedCarry4Design 8

mixedRegisterBenchmark : Raw.RawDesign
mixedRegisterBenchmark = mixedRegisterDesign 16