MTL_Monitor/tests/washing_machine/properties/prop4.hs

38 lines
1.9 KiB
Haskell

module Prop4 where
import Clash.Explicit.Testbench
import Clash.Prelude
import ProcessingElement(processingElement)
import Queue(queue,queuetest)
import Queue30(queue30,queuetest30)
queue_mealy11 inp = mealy queue (0:>0:>0:>0:>0:>0:>0:>Nil) inp
queue_mealy12 inp = mealy queue (0:>0:>0:>0:>0:>0:>0:>Nil) inp
queue_mealy13 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_diamond inp = mealy processingElement (1,(4,6,31,31,0,0,31,31,31,31),(31,31,31,31,0,0,31,31,6,6)) inp
prop4 (inp1,inp2) = queue_mealy13 (processingElement_mealy_or (bundle (queue_mealy11 (processingElement_mealy_not (bundle (inp1,inp1)) ), queue_mealy12 (processingElement_mealy_diamond (bundle (inp2,inp2)) ) )) )
topEntity
:: Clock System
-> Reset System
-> Enable System
-> (Signal System (Bool), Signal System (Bool))
-> Signal System ( Bool)
topEntity = exposeClockResetEnable prop4
testBench :: Signal System Bool
testBench = done
where
testInput1 = stimuliGenerator clk rst $(listToVecTH [False::Bool , False, False, True, 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, False, False, False, False, False,False, True, True, True, True, True, True, True,False, False, False])
done = expectOutput (topEntity clk rst en (testInput1, testInput2))
en = enableGen
clk = tbSystemClockGen (not <$> done)
rst = systemResetGen