1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
|
-----------------------------------------------------------------------------
-- |
-- Module : TestSuite.BitPrecise.Legato
-- Copyright : (c) Levent Erkok
-- License : BSD3
-- Maintainer: erkokl@gmail.com
-- Stability : experimental
--
-- Test suite for Documentation.SBV.Examples.BitPrecise.Legato
-----------------------------------------------------------------------------
{-# OPTIONS_GHC -Wall -Werror #-}
module TestSuite.BitPrecise.Legato(tests) where
import Data.SBV.Internals hiding (free, output)
import Documentation.SBV.Examples.BitPrecise.Legato
import Utils.SBVTestFramework
-- Test suite
tests :: TestTree
tests = testGroup "BitPrecise.Legato" [
goldenVsStringShow "legato" legatoPgm
, goldenVsStringShow "legato_c" legatoC
]
where legatoPgm = runSAT $ do
x <- free "x"
y <- free "y"
lo <- free "lo"
regX <- free "regX"
regA <- free "regA"
flagC <- free "flagC"
flagZ <- free "flagZ"
pure $ legatoIsCorrect (x, y, lo, regX, regA, flagC, flagZ)
thd (_, _, r) = r
legatoC = thd <$> compileToC' "legatoMult" (do
cgSetDriverValues [87, 92]
x <- cgInput "x"
y <- cgInput "y"
let (hi, lo) = runLegato (initMachine (x, y, 0, 0, 0, sFalse, sFalse))
cgOutput "hi" hi
cgOutput "lo" lo)
|
