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

module Spartan6.Benchmarks.Regression where

open import Spartan6.Prelude

import Spartan6.Benchmarks.Counters
import Spartan6.Benchmarks.Fixtures as Fixtures
import Spartan6.Netlist.Checked as Checked
import Spartan6.Netlist.NormalizeCombinational as Candidate
import Spartan6.Netlist.NormalizeMixed as Mixed
import Spartan6.Netlist.NormalizeScheduledCombinational as Pure
import Spartan6.Netlist.Raw as Raw
import Spartan6.Semantics.Design as Semantics
import Spartan6.Validation.Diagnostic as Diagnostic
import Spartan6.Validation.Raw as Validation

vecToList : ∀ {count} -> Vec Bit count -> List Bit
vecToList [] = []ᴸ
vecToList (bit ∷ bits) = bit ∷ᴸ vecToList bits

pureObservation :
  Diagnostic.CheckResult Candidate.CheckedCombinationalCandidate
  -> Maybe (List Bit)
pureObservation (Diagnostic.rejected diagnostics) = nothing
pureObservation (Diagnostic.accepted candidate) =
  just
    (vecToList
      (Semantics.observe compiled (replicate high) []))
  where
  compiled : Semantics.Design
    (Candidate.candidateInputCount candidate)
    (Candidate.candidateOutputCount candidate)
    0
  compiled = Checked.compileNetlist (Candidate.candidateNetlist candidate)

mixedInitialObservation :
  Diagnostic.CheckResult Mixed.CheckedMixedCandidate
  -> Maybe (List Bit)
mixedInitialObservation (Diagnostic.rejected diagnostics) = nothing
mixedInitialObservation (Diagnostic.accepted candidate) =
  just
    (vecToList
      (Semantics.observe compiled (replicate low)
        (Semantics.initial compiled)))
  where
  compiled : Semantics.Design
    (Mixed.candidateInputCount candidate)
    (Mixed.candidateOutputCount candidate)
    (Mixed.candidateRegisterCount candidate)
  compiled = Checked.compileNetlist (Mixed.candidateNetlist candidate)

mixedOneEdgeObservation :
  Diagnostic.CheckResult Mixed.CheckedMixedCandidate
  -> Maybe (List Bit)
mixedOneEdgeObservation (Diagnostic.rejected diagnostics) = nothing
mixedOneEdgeObservation (Diagnostic.accepted candidate) =
  just
    (vecToList
      (Semantics.observe compiled external
        (Semantics.step compiled Semantics.risingEdge external
          (Semantics.initial compiled))))
  where
  compiled : Semantics.Design
    (Mixed.candidateInputCount candidate)
    (Mixed.candidateOutputCount candidate)
    (Mixed.candidateRegisterCount candidate)
  compiled = Checked.compileNetlist (Mixed.candidateNetlist candidate)

  external : Semantics.Inputs compiled
  external = replicate high

orderedDesign : Raw.RawDesign
orderedDesign = Fixtures.orderedChainDesign 3

ordered-valid : Validation.StructurallyValid orderedDesign
ordered-valid = refl

ordered-chain-preserves-high :
  pureObservation
    (Pure.normaliseScheduledCombinational (orderedDesign , ordered-valid))
  ≡ just (high ∷ᴸ []ᴸ)
ordered-chain-preserves-high = refl

reverseDesign : Raw.RawDesign
reverseDesign = Fixtures.reverseChainDesign 3

reverse-valid : Validation.StructurallyValid reverseDesign
reverse-valid = refl

reverse-chain-preserves-high :
  pureObservation
    (Pure.normaliseScheduledCombinational (reverseDesign , reverse-valid))
  ≡ just (high ∷ᴸ []ᴸ)
reverse-chain-preserves-high = refl

fanOutDesign : Raw.RawDesign
fanOutDesign = Fixtures.fanOutDesign 4

fan-out-valid : Validation.StructurallyValid fanOutDesign
fan-out-valid = refl

fan-out-replicates-high :
  pureObservation
    (Pure.normaliseScheduledCombinational (fanOutDesign , fan-out-valid))
  ≡ just (high ∷ᴸ high ∷ᴸ high ∷ᴸ high ∷ᴸ []ᴸ)
fan-out-replicates-high = refl

independentDesign : Raw.RawDesign
independentDesign = Fixtures.independentDesign 4

independent-valid : Validation.StructurallyValid independentDesign
independent-valid = refl

independent-nodes-preserve-high :
  pureObservation
    (Pure.normaliseScheduledCombinational
      (independentDesign , independent-valid))
  ≡ just (high ∷ᴸ high ∷ᴸ high ∷ᴸ high ∷ᴸ []ᴸ)
independent-nodes-preserve-high = refl

multiOutputDesign : Raw.RawDesign
multiOutputDesign = Fixtures.multiOutputDesign 2

multi-output-valid : Validation.StructurallyValid multiOutputDesign
multi-output-valid = refl

multi-output-is-complementary :
  pureObservation
    (Pure.normaliseScheduledCombinational
      (multiOutputDesign , multi-output-valid))
  ≡ just (high ∷ᴸ low ∷ᴸ high ∷ᴸ low ∷ᴸ []ᴸ)
multi-output-is-complementary = refl

carry4Design : Raw.RawDesign
carry4Design = Fixtures.repeatedCarry4Design 2

carry4-valid : Validation.StructurallyValid carry4Design
carry4-valid = refl

carry4-chain-propagates-high :
  pureObservation
    (Pure.normaliseScheduledCombinational (carry4Design , carry4-valid))
  ≡ just
      (low ∷ᴸ low ∷ᴸ low ∷ᴸ low
       ∷ᴸ high ∷ᴸ high ∷ᴸ high ∷ᴸ high
       ∷ᴸ low ∷ᴸ low ∷ᴸ low ∷ᴸ low
       ∷ᴸ high ∷ᴸ high ∷ᴸ high ∷ᴸ high
       ∷ᴸ []ᴸ)
carry4-chain-propagates-high = refl

mixedDesign : Raw.RawDesign
mixedDesign = Fixtures.mixedRegisterDesign 3

mixed-valid : Validation.StructurallyValid mixedDesign
mixed-valid = refl

mixed-registers-start-low :
  mixedInitialObservation (Mixed.normaliseMixed (mixedDesign , mixed-valid))
  ≡ just (low ∷ᴸ low ∷ᴸ low ∷ᴸ []ᴸ)
mixed-registers-start-low = refl

mixed-registers-rise-simultaneously :
  mixedOneEdgeObservation (Mixed.normaliseMixed (mixedDesign , mixed-valid))
  ≡ just (high ∷ᴸ high ∷ᴸ high ∷ᴸ []ᴸ)
mixed-registers-rise-simultaneously = refl