blarney-lang / blarney Goto Github PK

I think it would be nice to have when work as a when :: Bit 1 -> Action () -> Module () on top of just when :: Bit 1 -> Action () -> Action (). I'd like to write something like

top = do
  cycleCount :: Reg (Bit 8) <- makeReg 0
  -- Increment cycleCount on every cycle
  always do
    cycleCount <== cycleCount.val + 1
  -- Terminate simulation when count reaches 20
  when (cycleCount.val .==. 20) do
    display "Finished"
    finish

instead of

top = do
  cycleCount :: Reg (Bit 8) <- makeReg 0
  always do
    -- Increment cycleCount on every cycle
    cycleCount <== cycleCount.val + 1
    -- Terminate simulation when count reaches 20
    when (cycleCount.val .==. 20) do
      display "Finished"
      finish

or

top = do
  cycleCount :: Reg (Bit 8) <- makeReg 0
  -- Increment cycleCount on every cycle
  always do
    cycleCount <== cycleCount.val + 1
  -- Terminate simulation when count reaches 20
  always do
    when (cycleCount.val .==. 20) do
      display "Finished"
      finish

More a suggestion than an issue: we recently implemented packing of sum(-of-product) types in Clash by separating the process of packing fields from packing the constructor. See:

1. The default methods for the Pack class: https://github.com/clash-lang/clash-compiler/blob/6422262599ebf53b4bf97d44a5b063c92d3ff81b/clash-prelude/src/Clash/Class/BitPack.hs#L73-L131

2. The Generic GBitpack class: https://github.com/clash-lang/clash-compiler/blob/6422262599ebf53b4bf97d44a5b063c92d3ff81b/clash-prelude/src/Clash/Class/BitPack.hs#L273-L300

3. The generic instances for sum types: https://github.com/clash-lang/clash-compiler/blob/6422262599ebf53b4bf97d44a5b063c92d3ff81b/clash-prelude/src/Clash/Class/BitPack.hs#L309-L338

Perhaps/hopefully these ideas can be easily converted to blarney. Although you would then also need first-class patterns (as in e.g. http://hackage.haskell.org/package/first-class-patterns) for sum-types to be useful in EDSLs (otherwise you can't "eliminate" sum types). However, with GHC 8.8 you'll get source plugins, by which perhaps you can convert Haskell case-statements to first-class patterns.

Motivation: fewer nonsense names in generated verilog. In particular, don't name literals.

Basic idea:

• Make WireId a sum type: one constructor for wires, and one for literals
• In flatten, return literal constructor for literals
• In Verilog.hs, generate code for literal inputs, inlined

Motivation: fewer nonsense names in generated verilog. In particular, don't name literals.

Basic idea:

• Make WireId a sum type: one constructor for wires, and one for literals
• In flatten, return literal constructor for literals
• In Verilog.hs, generate code for literal inputs, inlined

Q: I was hoping to use the NamBits example to influence signal names to simplify debugging .vcd files. Unfortunately, the "AAA" and "BBB" strings used in the example do not show up in the top.v file.

Is this intentional? Is there maybe an option I need to enable to influence the signal naming via hints.

After dicussing with @gameboo , we think that x > 0 in line 523 in Haskell/Blarney/Core/Prim.hs should be a x >= 0 in order to cover the zero case. What would you think @mn416 ?

I get the following error when --enable-simplifier is on when building SIMTight.

unsupported InputTree (SelectBits 3 1 0) [InputWire (34,Nothing)] for SelectBits in Verilog generation

There seems to be an issue with (at least) the restricted state verification.
Using the following file (in a template-project context):

import Blarney

notId :: Bit 1 -> Bit 1
notId x = s
  where
    s = x .^. c
    p = delay 0 $ delay 1 p
    c = delay 0 (p .&. s)

prop :: Bit 1 -> Action ()
prop x = assert (notId x === x) "notId === id"

main :: IO ()
main = do
  verifyWith cnfNoRestr prop
  verifyWith cnfRestr prop
  where
    cnfRestr = dfltVerifyConf { verifyConfMode = Induction (IncreaseFrom 1) True }
    cnfNoRestr = dfltVerifyConf { verifyConfMode = Induction (IncreaseFrom 1) False }

I get:

Assertion: notId === id
restricted states: disabled
(depth 1) bounded ............ valid
(depth 1) induction step ..... falsifiable
(depth 2) bounded ............ valid
(depth 2) induction step ..... falsifiable
(depth 3) bounded ............ falsifiable
not verified
Assertion: notId === id
restricted states: enabled
(depth 1) bounded ............ valid
(depth 1) induction step ..... falsifiable
(depth 2) bounded ............ valid
(depth 2) induction step ..... valid
verified

The restricted state: disabled result is correct, but the restricted state: enabled is incorrect.

The issue might also be happening with non-restricted states induction, since on this example it is bounded that rejects the property.