Skip to content
Permalink
Browse files

added minimal example for qualifiers

  • Loading branch information
gokhankici committed Jun 18, 2019
1 parent c769cd8 commit 186e418fb785646aef0cd8c097ff9004135622fe
@@ -46,6 +46,7 @@ library:
source-dirs: src
exposed-modules:
- Iodine.Runner
- Iodine.Utils
ghc-options:
- -Werror
- -O2
@@ -9,6 +9,7 @@ module Iodine.Runner ( IodineArgs(..)
, main
) where

import Iodine.Utils (silence)
import qualified Iodine.Abduction.Runner as VAR
import Iodine.Language.Parser
import Iodine.Language.Types
@@ -79,6 +80,7 @@ data IodineArgs =
, time :: Bool
, noFPOutput :: Bool
, annotFile :: FilePath
, verbose :: Bool
}
deriving (Show, Data, Typeable)

@@ -117,6 +119,9 @@ verylogArgs = IodineArgs { fileName = def
, noFPOutput = def
&= explicit &= name "no-output"
&= help "disable the output from fixpoint"
, verbose = def
&= explicit &= name "verbose"
&= help "enable verbose output"
}
&= program programName
&= summary summaryText
@@ -221,14 +226,13 @@ checkIR IodineArgs{..} = do
fileContents <- readFile fileName
let pipelineInput = ((fileName, fileContents), annotContents)
fpst = pipeline pipelineInput
withSilence = if verbose then id else silence

if | vcgen -> saveQuery cfg (toFqFormat fpst) >> return True
| abduction -> do let i = pipeline' pipelineInput
-- let input = VAR.runner' $ i
-- (safe, _) <- solve cfg $ toFpSt input
VAR.runner3 i
return True
| otherwise -> fmap fst (solve cfg fpst)
| otherwise -> fmap fst (withSilence $ solve cfg fpst)

where
cfg = defConfig { eliminate = Some
@@ -96,16 +96,15 @@ toFqFormat fpst =

custom2 n vs =
[ mkQual
(symbol $ "Custom2_" ++ show n ++ "_" ++ show n2)
(symbol $ "Custom2_" ++ show n)
[ QP (symbol "v") PatNone FInt
, QP (symbol x1) (PatExact (symbol $ prefix ++ x1)) (FTC boolFTyCon)
, QP (symbol x2) (PatExact (symbol $ prefix ++ x2)) (FTC boolFTyCon)
]
(FQT.PImp (eVar x1) (eVar x2))
(FQT.PIff (eVar x1) (eVar x2))
(dummyPos "")
| (n2',(x1',x2')) <- zip ([1,3..] :: [Int]) (twoPairs vs)
, (n2, (x1,x2)) <- [(n2',(x1',x2')), (n2' + 1, (x2',x1'))]
, prefix <- ["VLT_", "VRT_"]
| (x1,x2) <- twoPairs vs
, prefix <- ["VLT_"]
]

custom3 n l rs =
@@ -7,7 +7,6 @@ import Iodine.Language.Types
import Iodine.Solver.Common
import Iodine.Solver.FP.Types
import Iodine.Solver.FP.FQ
import Iodine.Utils

import qualified Language.Fixpoint.Solver as F
import qualified Language.Fixpoint.Types as FT
@@ -28,10 +27,7 @@ solve :: FC.Config -> FPSt -> IO (Bool, FT.FixSolution)
-- -----------------------------------------------------------------------------
solve cfg fpst = do
let finfo = toFqFormat fpst
wSilence = if FC.minimize cfg
then id
else silence
res <- wSilence $ F.solve cfg finfo
res <- F.solve cfg finfo
let stat = FT.resStatus res
withColor (getColor stat) $ putStr (render $ FT.resultDoc $ fmap fst stat)
putStrLn ""
@@ -6,6 +6,7 @@

module Main (main) where

import Iodine.Utils (silence)
import qualified Iodine.Runner as R

import Control.Lens hiding (simple, (<.>))
@@ -130,6 +131,7 @@ simple runner testDir =
, "tr-test-11"
, "merge-02"
, "merge03"
, "merge04-1"
, "merge04"
, "secverilog-01"
]
@@ -316,8 +318,9 @@ runUnitTest :: TestArgs -> R.IodineArgs -> Runner
runUnitTest ta va UnitTest{..} =
if ta ^. dryRun
then it testName (printf "iodine %s %s %s\n" verilogFile moduleName af :: IO ())
else it testName $ R.run va' `shouldReturn` (testType == Succ)
else it testName $ (withSilence $ R.run va') `shouldReturn` (testType == Succ)
where
withSilence = if ta ^. verbose then id else silence
af = case annotFile of
Nothing -> let dir = takeDirectory verilogFile
name = dropExtension $ takeBaseName verilogFile
@@ -327,4 +330,5 @@ runUnitTest ta va UnitTest{..} =
, R.moduleName = moduleName
, R.annotFile = af
, R.noSave = True
, R.verbose = ta ^. verbose
}
@@ -0,0 +1,27 @@
{
"annotations": [
{
"type": "source",
"variables": [
"in1",
"in2",
"in3"
]
},
{
"type": "sink",
"variables": [
"out"
]
}
],
"qualifiers": [
{
"type": "pairs",
"variables": [
"in1_r",
"in2_r"
]
}
]
}
@@ -0,0 +1,17 @@
module test(clk, in1, in2, in3, out);
input wire clk, in1, in2, in3;
output reg out;

reg in1_r, in2_r, in3_r;

always @(posedge clk) begin
in1_r <= in1;
in2_r <= in2;
in3_r <= in3;
if (in3_r)
out <= in1_r;
else
out <= in1_r + in2_r;
end

endmodule

0 comments on commit 186e418

Please sign in to comment.
You can’t perform that action at this time.