Copyright	(c) Victor Miquel 2024
License	MIT
Stability	experimental
Safe Haskell	Safe-Inferred
Language	GHC2021

Blarney.Backend.NewSMT

Description

Verify circuit properties using SMT solver.

'checkAuto Info' is the one-size-fits-all verification procedure (or 'checkAuto Verbose' to get progress reports).
`checkFixed depth Info` is the same for fixed-depth (therefore more efficient).
'debugAuto Info' is not focusing on speed, but on producing minimal counter-examples.
'debugFixed depth Info' is the same for fixed-depth (therefore more efficient).

Synopsis

data Verbosity
- = Verbose
- | Info
- | Quiet
data VerifyResult
data OutputType
type Writer = OutputType -> Doc -> IO ()
write_nothing :: Writer
write_screen :: Writer
data VerifConf = VerifConf {
- write :: Writer
- giveModel :: Bool
}
vconfQuiet :: VerifConf
vconfDefault :: VerifConf
vconfDebug :: VerifConf
data FixedConf = FixedConf {
- depth :: Int
}
fconfCombinational :: FixedConf
data IncrementalConf = IncrementalConf {
- limit :: Maybe Int
}
iconfDefault :: IncrementalConf
verifyOfflineFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> String -> String -> IO ()
verifyOfflineQIFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> String -> String -> IO ()
verifyLiveBounded :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> IO ()
verifyLiveFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> IO ()
verifyLiveQIFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> IO ()
verifyLiveIncremental :: Modular a => (Verbosity, VerifConf, IncrementalConf) -> a -> IO ()
checkBounded :: ProofPartRunner
checkRestrInd :: ProofPartRunner
checkQuantInd :: ProofPartRunner
incrSeq :: Int -> Int -> [Int]
proofPartGenerator :: [Int] -> Int -> ProofPartRunner -> AssertProofPartGenerator
verifyCircuit :: Modular a => AssertProofPartGenerator -> (Verbosity, VerifConf) -> a -> IO ()
checkAuto :: Modular a => Verbosity -> a -> IO ()
checkFixed :: Modular a => Int -> Verbosity -> a -> IO ()
debugAuto :: Modular a => Verbosity -> a -> IO ()
debugFixed :: Modular a => Int -> Verbosity -> a -> IO ()

Documentation

data Verbosity Source #

Verbosity level

Constructors

Verbose
Info
Quiet

data VerifyResult Source #

Outcome of verification

data OutputType Source #

Output kinds, used for filtering out unwanted parts

type Writer = OutputType -> Doc -> IO () Source #

Signature of functions that perform output depending on the output type

write_nothing :: Writer Source #

Writer that never writes

write_screen :: Writer Source #

Writer that always writes

data VerifConf Source #

Generic Verification Config

Constructors

VerifConf
Fields write :: Writer giveModel :: Bool

vconfQuiet :: VerifConf Source #

vconfDefault :: VerifConf Source #

vconfDebug :: VerifConf Source #

data FixedConf Source #

Verification Config for fixed depth

Constructors

FixedConf
Fields depth :: Int

fconfCombinational :: FixedConf Source #

data IncrementalConf Source #

Verification Config for incremental depth

Constructors

IncrementalConf
Fields limit :: Maybe Int

iconfDefault :: IncrementalConf Source #

verifyOfflineFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> String -> String -> IO () Source #

Write SMT script to file for offline, fixed depth, verification

verifyOfflineQIFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> String -> String -> IO () Source #

verifyLiveBounded :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> IO () Source #

Perform live bounded verification

verifyLiveFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> IO () Source #

Perform live fixed depth verification

verifyLiveQIFixed :: Modular a => (Verbosity, VerifConf, FixedConf) -> a -> IO () Source #

verifyLiveIncremental :: Modular a => (Verbosity, VerifConf, IncrementalConf) -> a -> IO () Source #

Perform live incremental depth verification

checkBounded :: ProofPartRunner Source #

Run bounded verification

checkRestrInd :: ProofPartRunner Source #

Run restricted states induction verification

checkQuantInd :: ProofPartRunner Source #

Run quantified induction verification

incrSeq :: Int -> Int -> [Int] Source #

A stricty increasing sequence. n (strictly positive) controls growth rate, the bigger the slower. curr is the initial value.

proofPartGenerator :: [Int] -> Int -> ProofPartRunner -> AssertProofPartGenerator Source #

Parametric proof part generator depths is a sequence of depths count is the number of concurrent jobs runner is the proof part runner

verifyCircuit :: Modular a => AssertProofPartGenerator -> (Verbosity, VerifConf) -> a -> IO () Source #

Concurrent verification

checkAuto :: Modular a => Verbosity -> a -> IO () Source #

Automatic verification procedure Aimed at giving a result as soon as possible

checkFixed :: Modular a => Int -> Verbosity -> a -> IO () Source #

Fixed depth verification procedure Aimed at giving a result as soon as possible

debugAuto :: Modular a => Verbosity -> a -> IO () Source #

Automatic minimal depth counterexample generation Note: Will run forever if there are no counterexamples TODO: Compare performance with incremental solution

debugFixed :: Modular a => Int -> Verbosity -> a -> IO () Source #

Fixed depth counterexample generation Note: Returns Unknown if there is no such counterexample