Data.SBV.Tools.GenTest

Test generation from symbolic programs

Test case generation

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

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 and pConstrain for filtering acceptable test values.)

data TestVectors

Type of test vectors (abstract)

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

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

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

data TestStyle

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