From f5881919c1f84feb8b987765768c304988d57f41 Mon Sep 17 00:00:00 2001 From: Rupert Swarbrick Date: Fri, 13 Mar 2020 17:24:11 +0000 Subject: [PATCH] Allow exclusion of Assert conversion Yosys does support some asserts nowadays. Allowing sv2v to not strip them out means that you can check formal properties without needing hierarchical references (which Yosys really doesn't cope well with!) --- src/Convert.hs | 2 +- src/Job.hs | 3 ++- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Convert.hs b/src/Convert.hs index d51ad21..065491f 100644 --- a/src/Convert.hs +++ b/src/Convert.hs @@ -55,7 +55,7 @@ phases :: [Job.Exclude] -> [Phase] phases excludes = [ Convert.AsgnOp.convert , Convert.NamedBlock.convert - , Convert.Assertion.convert + , selectExclude (Job.Assert , Convert.Assertion.convert) , Convert.BlockDecl.convert , Convert.DuplicateGenvar.convert , selectExclude (Job.Logic , Convert.Logic.convert) diff --git a/src/Job.hs b/src/Job.hs index 83d4c81..d2e6449 100644 --- a/src/Job.hs +++ b/src/Job.hs @@ -15,6 +15,7 @@ import System.Environment (getArgs, withArgs) data Exclude = Always + | Assert | Interface | Logic | Succinct @@ -45,7 +46,7 @@ defaultJob = Job , siloed = nam_ "siloed" &= help ("Lex input files separately, so" ++ " macros from earlier files are not defined in later files") , exclude = nam_ "exclude" &= name "E" &= typ "CONV" - &= help "Exclude a particular conversion (always, interface, or logic)" + &= help "Exclude a particular conversion (always, assert, interface, or logic)" &= groupname "Conversion" , verbose = nam "verbose" &= help "Retain certain conversion artifacts" }