Formal verification of a Clash circuit, using Yosys/SymbiYosys.

Assert.hs

{-# LANGUAGE GADTs          #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE TypeFamilies   #-}
module Assert
  ( assertProperty
  , initialAssume
  , getReset
  ) where

import           Clash.Prelude
import           Clash.Signal.Internal

-- | Assert a SystemVerilog(-ish) property over a given @'Signal'@, returning
-- another @'Signal'@.
--
-- During both simulation and synthesis, @'assertProperty' b v@ is equivalent to
-- @v@. However, during verification (with @yosys-smtbmc@ or @symbiyosys@), this
-- asserts that the given @'Bool'@ @'Signal'@ always holds @'True'@.
assertProperty
  :: Signal dom Bool
  -- ^ The assertion to check. This is a stateful @'Signal'@ which is assumed to
  -- be some property to check over a given circuit.
  -> Signal dom a
  -- ^ Input @'Signal'@. This value is simply returned.
  -> Signal dom a
  -- ^ Output @'Signal'@. Identical to the input @'Signal'@.
assertProperty = \_ x -> x
{-# NOINLINE assertProperty #-}

-- | Assume a SystemVerilog(-ish) property for the initial clock cycle, over
-- a given @'Signal'@, returning another @'Signal'@.
--
-- During both simulation and synthesis, @'initialAssume' b v@ is equivalent to
-- @v@. However, during verification (with @yosys-smtbmc@ or @symbiyosys@), this
-- introduces the necessary assumption that the @'Bool'@ holds true on the
-- initial clock cycle; i.e. it tells that the given @'Bool'@ @'Signal'@ holds
-- @'True'@ the verification tool to only consider SMT traces where this case is
-- true.
initialAssume
  :: Signal dom Bool
  -- ^ Signal to assume true on the initial clock cycle.
  -> Signal dom a
  -- ^ Input @'Signal'@. This value is simply returned.
  -> Signal dom a
  -- ^ Output @'Signal'@. Identical to the input @'Signal'@.
initialAssume = \_ x -> x
{-# NOINLINE initialAssume #-}

-- | Convert an explicit @'Reset'@ into a @'Bool'@ @'Signal'@. This is often
-- used to assert/assume things about the reset during verification (e.g.
-- @'initialAssume'@ that the given @'Reset'@ is set on the first clock cycle,
-- to initialize registers).
getReset
  :: Reset dom sync
  -- ^ @'Reset'@ to convert.
  -> Signal dom Bool
  -- ^ @'Bool'@ @'Signal'@ for the given @'Reset'@.
getReset (Async rst) = rst
getReset (Sync rst)  = rst
{-# INLINEABLE getReset #-}

Assert.json

[ { "BlackBox"    :
    { "name"      : "Assert.assertProperty"
    , "templateD" : "// assertProperty begin
`ifdef FORMAL
  assert property (~ARG[0]);
`endif
assign ~RESULT = ~ARG[1];
// assertProperty end"
    }
  },
  { "BlackBox"    :
    { "name"      : "Assert.initialAssume"
    , "templateD" : "// initialAssume begin
`ifdef FORMAL
  initial assume (~ARG[0]);
`endif
assign ~RESULT = ~ARG[1];
// initialAssume end"
    }
  }
]

Counter.hs

{-# LANGUAGE CPP               #-}
{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE ImplicitParams    #-}
{-# LANGUAGE TemplateHaskell   #-}
{-# LANGUAGE TypeApplications  #-}
{-# LANGUAGE TypeOperators     #-}

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise       #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.Extra.Solver    #-}
{-# OPTIONS_GHC -fplugin GHC.TypeLits.KnownNat.Solver #-}

module Counter
  ( top
  ) where
import           GHC.Stack
import           Clash.Prelude

import           TopGen
import           Assert


-- | Simple verification harness, for time-invariant properties over a
-- @'Signal'@, with a given @'Clock'@ and @'Reset'@ line. Given a clocked signal
-- @v@, the circuit @'verify' prop v@ asserts that @prop v@ should always be
-- @'True'@ for every clock cycle. @'verify'@ also abstracts over the
-- synchronous reset logic and properly assumes existence of the reset signal,
-- or that the property is upheld.
verify
  :: ( HasCallStack
     , HasClockReset dom gate sync
     )
  => (a -> Bool)
  -> Signal dom a
  -> Signal dom a
verify f s
  = initialAssume rst              -- assume: rst is high on clk #0
  $ assertProperty (rst .||. prop) -- assert: either rst is high, or prop is ok
  $ s
  where
    -- property: the output counter signal is always lower than the specified
    -- limit, which is 32, in this case.
    prop = fmap f s

    -- reset line, converted to a Bool, used for our verification assumptions.
    -- 'hasReset' ties the explicit reset argument to our implicit reset line.
    rst = getReset hasReset

-- | A counter circuit, that counts from 0 to 15 (inclusive) and then resets
-- to zero. This counter requires a clock and reset line to be attached.
counter
  :: ( HasCallStack                -- ^ Constraint: Contains a callstack
     , HasClockReset dom gate sync -- ^ Constraint: clock and reset lines
     )
  => Signal dom (Unsigned 6)       -- ^ Output: unsigned 6-bit number.
counter = verify prop out
  where
    -- property: the output counter signal is always lower than the specified
    -- limit, which is 32, in this case.
    prop = (< lim) where lim = 32 :: Unsigned 6

    -- the counter: counts from 0 to 15, and resets back to 0. this is defined
    -- as a feedback loop using a register, and it simply maps a pure function
    -- onto the stateful component to apply the logic.
    out = register 0 (fmap f out)
    f x | x == 15   = 0
        | otherwise = x + 1

-- | Exported @'TopEntity'@. Ties @'counter'@ to an appropriate @'Clock'@ and
-- @'Reset'@.
top
  :: "clk" ::: Clock System 'Source
  -> "rst" ::: Reset System 'Synchronous
  -> "out" ::: Signal System (Unsigned 6)
top clk rst = withClockReset clk rst counter
$(makeTopEntity 'top) -- auto generate

counter.sby

[options]
mode prove
depth 17

[engines]
smtbmc

[script]
read_verilog -formal top.v
prep -top top

[files]
verilog/Counter/top/top.v

results.txt

[nix-shell:~/src/clash-playground/src/fpga]$ clash --verilog Counter.hs && sby -f counter.sby
Loading dependencies took 2.602479004s
Compiling: Counter.top
Applied 61 transformations
Normalisation took 0.727354546s
Netlist generation took 0.002188659s
Total compilation took 3.333886118s
SBY [counter] Removing direcory 'counter'.
SBY [counter] Copy 'verilog/Counter/top/top.v' to 'counter/src/top.v'.
SBY [counter] engine_0: smtbmc
SBY [counter] script: starting process "cd counter/src; yosys -ql ../model/design.log ../model/design.ys"
SBY [counter] script: finished (returncode=0)
SBY [counter] smt2: starting process "cd counter/model; yosys -ql design_smt2.log design_smt2.ys"
SBY [counter] smt2: finished (returncode=0)
SBY [counter] engine_0.basecase: starting process "cd counter; yosys-smtbmc --noprogress  -t 17 --append 0 --dump-vcd engine_0/trace.vcd --dump-vlogtb engine_0/trace_tb.v --dump-smtc engine_0/trace.smtc model/design_smt2.smt2"
SBY [counter] engine_0.induction: starting process "cd counter; yosys-smtbmc --noprogress -i -t 17 --append 0 --dump-vcd engine_0/trace_induct.vcd --dump-vlogtb engine_0/trace_induct_tb.v --dump-smtc engine_0/trace_induct.smtc model/design_smt2.smt2"
SBY [counter] engine_0.basecase: ##      0   0:00:00  Solver: yices
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 0..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 1..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 2..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 3..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 4..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 5..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 6..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 7..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 8..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 9..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 10..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 11..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 12..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 13..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 14..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 15..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Checking assertions in step 16..
SBY [counter] engine_0.basecase: ##      0   0:00:00  Status: PASSED
SBY [counter] engine_0.induction: ##      0   0:00:00  Solver: yices
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 17..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 16..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 15..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 14..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 13..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 12..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 11..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 10..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 9..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 8..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 7..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 6..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 5..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 4..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 3..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 2..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 1..
SBY [counter] engine_0.induction: ##      0   0:00:00  Trying induction in step 0..
SBY [counter] engine_0.induction: ##      0   0:00:00  Temporal induction successful.
SBY [counter] engine_0.induction: ##      0   0:00:00  Status: PASSED
SBY [counter] engine_0.basecase: finished (returncode=0)
SBY [counter] engine_0: Status returned by engine for basecase: PASS
SBY [counter] engine_0.induction: finished (returncode=0)
SBY [counter] engine_0: Status returned by engine for induction: PASS
SBY [counter] summary: Elapsed clock time [H:MM:SS (secs)]: 0:00:00 (0)
SBY [counter] summary: Elapsed process time [H:MM:SS (secs)]: 0:00:00 (0)
SBY [counter] summary: engine_0 (smtbmc) returned PASS for basecase
SBY [counter] summary: engine_0 (smtbmc) returned PASS for induction
SBY [counter] summary: successful proof by k-induction.
SBY [counter] DONE (PASS, rc=0)

[nix-shell:~/src/clash-playground/src/fpga]$ 

TopGen.hs

{-# OPTIONS_GHC -Wall -Wno-orphans #-}

{-# LANGUAGE DataKinds          #-}
{-# LANGUAGE DeriveLift         #-}
{-# LANGUAGE LambdaCase         #-}
{-# LANGUAGE PatternSynonyms    #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeOperators      #-}
{-# LANGUAGE TemplateHaskell    #-}
{-# LANGUAGE ViewPatterns       #-}
module TopGen
  ( makeTopEntity
  ) where

-- base
import           Prelude

-- template-haskell
import           Language.Haskell.TH
import           Language.Haskell.TH.Syntax

-- clash
import           Clash.NamedTypes            ((:::))
import           Clash.Annotations.TopEntity

--
-- utilities
--

-- matches against `"nam" ::: ty` using (:::) from Clash, but we
-- can't check the type constructor here :(
pattern NamedTy :: Type -> String -> Type
pattern NamedTy con nam <-
  SigT (AppT (AppT con (LitT (StrTyLit nam))) _) _

-- matches a type `a -> b`
pattern ArrowTy :: Type -> Type -> Type
pattern ArrowTy a b = AppT (AppT ArrowT a) b

-- orphans
deriving instance Lift PortName
deriving instance Lift TopEntity

isTupT :: Type -> Bool
isTupT (AppT x _) = isTupT x
isTupT (TupleT _) = True
isTupT _          = False

collectTupT :: Type -> [Type]
collectTupT (AppT (TupleT _) v) = [v]
collectTupT (AppT f v)          = collectTupT f ++ collectTupT v
collectTupT (TupleT _)          = []
collectTupT x                   = [x]

-- | Given an multi-arity function type @f :: a -> b -> c -> ...@, get
-- the final return type.
getReturnTy :: Type -> Q Type
getReturnTy (ArrowTy _ b) = getReturnTy b
getReturnTy b             = return b

-- | Automatically create a @'TopEntity'@ for a given @Name@.
makeTopEntity :: Name -> DecsQ
makeTopEntity n = reify n >>= \case
  VarI nam typ _ -> do
    -- helpers
    let prag t = PragmaD (AnnP (valueAnnotation nam) t)

    -- get a Name for this type operator so we can check it
    -- in the ArrowTy case
    nty <- [t| (:::) |]

    -- examine the arguments
    let examine ty = go ty [] where
          go (ArrowTy (NamedTy con a) b) xs
            | con == nty
            = do { v <- go b xs; return (a:v) }

          go (ArrowTy _ _) _
            = fail $ "makeTopEntity: All types for an autogenerated "
            ++ "top-entity (both input and output) must have a name!"

          go _ xs = return xs

    ins <- map PortName <$> examine typ
    out <- getReturnTy typ >>= \case
      -- single output
      NamedTy con r | con == nty -> return $ PortName r

      -- multi output
      xs@(isTupT -> True) -> do
        let go (NamedTy con r) | con == nty = return (PortName r)
            go _ = fail $ "makeTopEntity: Output tuple must have "
                 ++ "names for all components!"

        PortField mempty <$> mapM go (collectTupT xs)

      -- invalid type
      _ -> fail "makeTopEntity: Invalid return type!"

    -- Return the annotation
    top <- lift $ TopEntity
                    { t_name   = nameBase nam
                    , t_inputs = ins
                    , t_output = out
                    }
    return [prag top]

  -- failure case: we weren't provided with the name of a binder
  _ -> fail "makeTopEntity: invalid Name, must be a top-level binding!"

Hey this is great- very informative. Your makeTopEntity is also widely applicable. Have you thought about upstreaming it? If you are busy I could do it and reference this gist.

@blaxill Yes, I have thought about upstreaming makeTopEntity, though it's incredibly ugly (IMO), and I think when I initially discussed it with Christiaan, it had a few deficiencies, I think -- this one, for example, does support tuples for the return type, but not nested tuples (which is a natural extension, IMO, but perhaps a minor use case,) nor does it support tuples for the input types. That might not matter so much in reality though, I just never got around to generalizing it for those cases. And that could always be fixed later with little API impact, too.

I'm not actively writing much Clash at the moment (beyond some spare side projects I occasionally pick up), so at the moment I don't have time to upstream it -- feel free to do so yourself. If you want to do that, I also suggest you start with this version instead -- this version of TopGen.hs in my clash-playground repository has extra docs, as well as an extra makeTopEntityWithName so you can choose the entity name, beyond just using the reified Haskell function name (this version is an evolution of the original one in this gist)

https://github.com/thoughtpolice/clash-playground/blob/master/src/TopGen.hs