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

module Spartan6.Benchmarks.Workloads where

open import Spartan6.Prelude

import Spartan6.Benchmarks.Fixtures as Fixtures
import Spartan6.Benchmarks.Regression
import Spartan6.Netlist.NormalizeMixed as Mixed
import Spartan6.Netlist.NormalizeScheduledCombinational as Pure
import Spartan6.Validation.Raw as Validation
open import Spartan6.Validation.CheckResult using (accepted?)

ordered-valid :
  Validation.StructurallyValid Fixtures.orderedChainBenchmark
ordered-valid = refl

ordered-workload-accepts :
  accepted?
    (Pure.normaliseScheduledCombinational
      (Fixtures.orderedChainBenchmark , ordered-valid))
  ≡ true
ordered-workload-accepts = refl

reverse-valid :
  Validation.StructurallyValid Fixtures.reverseChainBenchmark
reverse-valid = refl

reverse-workload-accepts :
  accepted?
    (Pure.normaliseScheduledCombinational
      (Fixtures.reverseChainBenchmark , reverse-valid))
  ≡ true
reverse-workload-accepts = refl

fan-out-valid : Validation.StructurallyValid Fixtures.fanOutBenchmark
fan-out-valid = refl

fan-out-workload-accepts :
  accepted?
    (Pure.normaliseScheduledCombinational
      (Fixtures.fanOutBenchmark , fan-out-valid))
  ≡ true
fan-out-workload-accepts = refl

independent-valid :
  Validation.StructurallyValid Fixtures.independentBenchmark
independent-valid = refl

independent-workload-accepts :
  accepted?
    (Pure.normaliseScheduledCombinational
      (Fixtures.independentBenchmark , independent-valid))
  ≡ true
independent-workload-accepts = refl

multi-output-valid :
  Validation.StructurallyValid Fixtures.multiOutputBenchmark
multi-output-valid = refl

multi-output-workload-accepts :
  accepted?
    (Pure.normaliseScheduledCombinational
      (Fixtures.multiOutputBenchmark , multi-output-valid))
  ≡ true
multi-output-workload-accepts = refl

carry4-valid :
  Validation.StructurallyValid Fixtures.repeatedCarry4Benchmark
carry4-valid = refl

carry4-workload-accepts :
  accepted?
    (Pure.normaliseScheduledCombinational
      (Fixtures.repeatedCarry4Benchmark , carry4-valid))
  ≡ true
carry4-workload-accepts = refl

mixed-valid :
  Validation.StructurallyValid Fixtures.mixedRegisterBenchmark
mixed-valid = refl

mixed-workload-accepts :
  accepted?
    (Mixed.normaliseMixed
      (Fixtures.mixedRegisterBenchmark , mixed-valid))
  ≡ true
mixed-workload-accepts = refl