module Prop3 where
import Clash.Explicit.Testbench
import Clash.Prelude
import ProcessingElement(processingElement)
import Queue(queue,queuetest)
import Queue30(queue30,queuetest30)

queue_mealy7 inp  = mealy queue (0:>Nil) inp
queue_mealy8 inp  = mealy queue (0:>Nil) inp
queue_mealy9 inp  = mealy queue (0:>Nil) inp
queue_mealy10 inp = mealy queue (0:>Nil) inp

processingElement_mealy_or inp = mealy processingElement (0,(0,0,31,31,31,31,31,31,31,31),(31,31,0,0,31,31,31,31,31,31)) inp

processingElement_mealy_not inp = mealy processingElement (1,(31,31,0,0,31,31,31,31,31,31),(0,0,31,31,31,31,31,31,31,31)) inp

processingElement_mealy_next inp = mealy processingElement (1,(1,1,31,31,0,0,31,31,31,31),(31,31,1,1,0,0,31,31,31,31)) inp

prop3 (inp1,inp2) = queue_mealy10 (processingElement_mealy_or (bundle (queue_mealy9 (processingElement_mealy_not (bundle (inp1,inp1)) ) , queue_mealy8 (processingElement_mealy_next (bundle (queue_mealy7 (processingElement_mealy_or (bundle (inp1, inp2) ) ), queue_mealy7 (processingElement_mealy_or (bundle (inp1, inp2) ) )  ) ) ))))

topEntity
  :: Clock System
  -> Reset System
  -> Enable System
  -> (Signal System (Bool), Signal System (Bool))
  -> Signal System ( Bool)
topEntity = exposeClockResetEnable prop3

testBench :: Signal System Bool
testBench = done
  where
    testInput1    = stimuliGenerator clk rst $(listToVecTH [False::Bool , False, True, False, False, False, False, False, False, False, False, False, False, False, False, False])
    testInput2    = stimuliGenerator clk rst $(listToVecTH [False::Bool , False, False, False, False, False, False, True, True, True, True, True, True, True,False, False, False])
    expectOutput = outputVerifier' clk rst $(listToVecTH [False::Bool , False, True, True, False, True, True, True, True, True, True, True, True , True, True, True,True])
    done         = expectOutput (topEntity clk rst en (testInput1, testInput2))
    en           = enableGen
    clk          = tbSystemClockGen (not <$> done)
    rst          = systemResetGen