sbv-7.13: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright | (c) Levent Erkok
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Data.SBV.Tools.GenTest

Contents

- Test case generation

Description

Test generation from symbolic programs

Synopsis

- genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors
- data TestVectors
- getTestValues :: TestVectors -> [([CW], [CW])]
- renderTest :: TestStyle -> TestVectors -> String
- data TestStyle
  - = Haskell String
  - | C String
  - | Forte String Bool ([Int], [Int])

# Test case generation

genTest :: Outputtable a => Int -> Symbolic a -> IO TestVectors Source #

Generate a set of concrete test values from a symbolic program. The output can be rendered as test vectors in different languages as necessary. Use the function `output` call to indicate what fields should be in the test result. (Also see `constrain` for filtering acceptable test values.)

data TestVectors Source #

Type of test vectors (abstract)

getTestValues :: TestVectors -> [([CW], [CW])] Source #

Retrieve the test vectors for further processing. This function is useful in cases where `renderTest` is not sufficient and custom output (or further preprocessing) is needed.

renderTest :: TestStyle -> TestVectors -> String Source #

Render the test as a Haskell value with the given name `n`.

data TestStyle Source #

Test output style

Constructors

Haskell String | As a Haskell value with given name
C String | As a C array of structs with given name
Forte String Bool ([Int], [Int]) | As a Forte/Verilog value with given name. If the boolean is True then vectors are blasted big-endian, otherwise little-endian The indices are the split points on bit-vectors for input and output values