| Copyright | (c) 2021 Yann Herklotz |
|---|---|
| License | GPL-3 |
| Maintainer | yann [at] yannherklotz [dot] com |
| Stability | experimental |
| Portability | POSIX |
| Safe Haskell | None |
| Language | Haskell2010 |
Verismith.EMI
Description
Equivalence modulo inputs (EMI) testing. This file should get an existing design, and spit out a modified design that is equivalent under some specific values of the extra inputs.
Synopsis
- data EMIInputs a
- = EMIInputs [Identifier]
- | EMIOrig a
- newPort' :: Identifier -> StateGen a Port
- nstatementEMI :: StateGen a (Maybe (Statement a))
- statementEMI :: Statement a -> StateGen a (Statement a)
- moditemEMI :: ModItem a -> StateGen a (ModItem a)
- moddeclEMI :: ModDecl a -> StateGen a (ModDecl (EMIInputs a))
- sourceEMI :: SourceInfo a -> StateGen a (SourceInfo (EMIInputs a))
- initNewRegs :: [Port] -> ModDecl a -> ModDecl a
- initNewInnerRegs :: [Port] -> ModDecl a -> ModDecl a
- proceduralEMI :: SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a))
- proceduralEMIIO :: SourceInfo a -> Config -> IO (SourceInfo (EMIInputs a))
- makeTopEMI :: Int -> ModDecl (EMIInputs ann) -> (ModDecl (EMIInputs ann), [Identifier])
- createProperty :: Identifier -> ModItem a
- createAssignment :: Identifier -> Statement a
- addAssumesEMI :: (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier])
- addAssignmentsEMI :: (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier])
- makeTopAssertEMI :: Bool -> ModDecl (EMIInputs ann) -> (ModDecl (EMIInputs ann), [Identifier])
- initModEMI :: (ModDecl ann, [Identifier]) -> ModDecl ann
- getTopEMIIdent :: SourceInfo (EMIInputs a) -> [Identifier]
- m :: SourceInfo ()
- p :: Show a => ModDecl a -> IO ()
- p2 :: Show a => SourceInfo a -> IO ()
- customConfig :: Config
- top :: IO ()
- top2 :: IO ()
Documentation
Constructors
| EMIInputs [Identifier] | |
| EMIOrig a |
Instances
| Show a => Show (EMIInputs a) Source # | |
| Eq a => Eq (EMIInputs a) Source # | |
| Ord a => Ord (EMIInputs a) Source # | |
Defined in Verismith.EMI | |
sourceEMI :: SourceInfo a -> StateGen a (SourceInfo (EMIInputs a)) Source #
proceduralEMI :: SourceInfo a -> Config -> Gen (SourceInfo (EMIInputs a)) Source #
proceduralEMIIO :: SourceInfo a -> Config -> IO (SourceInfo (EMIInputs a)) Source #
makeTopEMI :: Int -> ModDecl (EMIInputs ann) -> (ModDecl (EMIInputs ann), [Identifier]) Source #
Make top level module for equivalence verification. Also takes in how many modules to instantiate.
createProperty :: Identifier -> ModItem a Source #
createAssignment :: Identifier -> Statement a Source #
addAssumesEMI :: (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier]) Source #
addAssignmentsEMI :: (ModDecl a, [Identifier]) -> (ModDecl a, [Identifier]) Source #
makeTopAssertEMI :: Bool -> ModDecl (EMIInputs ann) -> (ModDecl (EMIInputs ann), [Identifier]) Source #
Make a top module with an assert that requires y_1 to always be equal to
y_2, which can then be proven using a formal verification tool.
initModEMI :: (ModDecl ann, [Identifier]) -> ModDecl ann Source #
getTopEMIIdent :: SourceInfo (EMIInputs a) -> [Identifier] Source #
m :: SourceInfo () Source #