Copyright	(c) Alexandre Joannou 2020-2021
License	MIT
Stability	experimental
Safe Haskell	Safe-Inferred
Language	GHC2021

Blarney.Backend.SMT

Description

Convert Blarney Netlist to SMT scripts.

Synopsis

data VerifyDepth
- = Range Int Int
- | IncreaseFrom Int
fixedDepth :: Int -> VerifyDepth
data VerifyMode
- = Bounded VerifyDepth
- | Induction VerifyDepth UseRestrictedStates
data UserConf = UserConf {
- userConfInteractive :: Bool
- userConfIncreasePeriod :: Int
}
dfltUserConf :: UserConf
data VerifyConf = VerifyConf {
- verifyConfMode :: VerifyMode
- verifyConfSolverCmd :: (String, [String])
- verifyConfUser :: UserConf
- verifyConfVerbosity :: Int
}
dfltVerifyConf :: VerifyConf
genSMTScript :: VerifyConf -> Netlist -> String -> String -> IO ()
verifyWithSMT :: VerifyConf -> Netlist -> IO ()

Documentation

data VerifyDepth Source #

Type to control depth of verification

Constructors

Range Int Int	Span depths between both `Int` arguments
IncreaseFrom Int	Span all depths increasingly starting from the `Int` argument

Instances

Instances details

Show VerifyDepth #
Instance details Defined in Blarney.Backend.SMT Methods showsPrec :: Int -> VerifyDepth -> ShowS # show :: VerifyDepth -> String # showList :: [VerifyDepth] -> ShowS #

fixedDepth :: Int -> VerifyDepth Source #

Helper function to construct a VerifyDepth describing a fixed unique depth n, i.e. `Range n n`

data VerifyMode Source #

Type to specify the kind of verification desired

Constructors

Bounded VerifyDepth	property holds up to a certain depth
Induction VerifyDepth UseRestrictedStates	property holds by induction

data UserConf Source #

Configuration type for interaction with a human user

Constructors

UserConf
Fields userConfInteractive :: Bool Ask the user for confirmation or use default answer userConfIncreasePeriod :: Int For iterative deepening, period at which to ask the user for continuation

dfltUserConf :: UserConf Source #

Default UserConf: dfltUserConf = UserConf { userConfInteractive = False , userConfIncreasePeriod = 4 }

data VerifyConf Source #

Configuration type for a verification session

Constructors

VerifyConf
Fields verifyConfMode :: VerifyMode verification type to use verifyConfSolverCmd :: (String, [String]) SMT solver command verifyConfUser :: UserConf user configuration to use verifyConfVerbosity :: Int verbosity level for the interactive session

dfltVerifyConf :: VerifyConf Source #

Default VerifyConf: dfltVerifyConf = VerifyConf { verifyConfMode = Bounded (Range 1 1) , verifyConfSolverCmd = ("z3", ["-in"]) , verifyConfUser = dfltUserConf , verifyConfVerbosity = 1 }

genSMTScript Source #

Arguments

:: VerifyConf	configuration for the verification
-> Netlist	blarney netlist
-> String	script name
-> String	output directory
-> IO ()

Convert given blarney Netlist to an SMT script

verifyWithSMT Source #

Arguments

:: VerifyConf	configuration for the verification
-> Netlist	blarney property
-> IO ()

Verify given blarney Netlist predicate using an SMT solver