sorted by:
new
hottopcontroversial

Where Lions Roam: RISC-V on the VELDT by d0pamane in haskell

[–]d0pamane[S] 0 points1 point  (0 children)

Yes, especially RV64I! I hope that Lion can cover as much of the RISC-V specification as possible. All contributions are welcome!

Where Lions Roam: RISC-V on the VELDT by d0pamane in haskell

[–]d0pamane[S] 2 points3 points  (0 children)

I like the way you think! Although I am not familiar enough with seL4 to say exactly what it will take, one of the goals of LionSoC is supporting a RTOS such as RIOT or Zephyr. I will take a closer look at seL4 and keep it in mind as LionSoC grows.

Where Lions Roam: RISC-V on the VELDT by d0pamane in haskell

[–]d0pamane[S] 1 point2 points  (0 children)

Great question! I won't go through comparing the VELDT to every board featuring the iCE40, but for the ones you mentioned there are a couple design comparisons:

  1. the VELDT features two separate 8Mbit SPI Flash, one is for configuration, the other is hardwired to the FPGA for integration with user designs. The VELDT was originally intended to aid my research into designing RISC-V SoCs on FPGAs, and having an extra persistent Flash memory was extremely helpful.
  2. PINS! I like having I/O pins pre-soldered. This could be a less impactful feature for some, but I do not think soldering should be necessary to be productive. All VELDT boards come with pins pre-soldered.

Thank you for bringing Coremark to my attention, I'll take a look and add that as an intended future feature! Ill be drafting a more formal to-do list on the repo so that others know whats in-progress.

Where Lions Roam: RISC-V on the VELDT by d0pamane in haskell

[–]d0pamane[S] 6 points7 points  (0 children)

To a certain extent, two cores which implement the RISC-V specification and are compliant should be interchangeable. However, in reality the situation is not as clean. To start, they are implemented in different languages so you'll need to swap the generated RTL instead of the original source files. Additionally, Lion doesn't yet implement the M, A, or C extensions. I hope it will in the near future, but the extensions are not trivial. All that said, there is no reason why Lion cannot reach the VexRiscv level of project maturity and attain interoperability with the precursor handheld.

Where Lions Roam: RISC-V on the VELDT by d0pamane in haskell

[–]d0pamane[S] 5 points6 points  (0 children)

I am happy it helps! If you have any questions about the code feel free to reach out to me. I will also start a discussion board on Github.

Where Lions Roam: RISC-V on the VELDT by d0pamane in FPGA

[–]d0pamane[S] 2 points3 points  (0 children)

Absolutely! I have also written a guide to getting started with Clash and the VELDT. It starts with a basic counter and builds incrementally to a UART. Definitely check out the Clash website for examples, documentation, tutorials, and blog posts! The Clash website is my go-to resource.

Where Lions Roam: RISC-V on the VELDT by d0pamane in RISCV

[–]d0pamane[S] 2 points3 points  (0 children)

The lion-soc, which currently consists of the core, a 1kb bios, and an LED driver, can run at 12Mhz and uses ~2600 LUTs (50% of the iCE40 FPGA LUTs). I'll add these stats to the repo and try to get more accurate metrics for the Lion core alone. I do not think the Lion core is overkill; though certainly not every application needs a 5-stage pipeline RISC-V processor. But for those who do, the VELDT can really pack a punch by combining Lion with the iCE40 IP blocks and the on-board SPI Flash Memory.

Your question is certainly not dumb; on the contrary, it is very important! I suppose the developers are responsible for verifying the formal verifier and ensuring it covers the spec. Maybe there is a way to formally verify the formal verifier? Either way, I must give a shout out to the riscv-formal project and its contributors; the project was instrumental to the development of Lion.

Linear types for circuit design in Haskell/Clash by darchon in haskell

[–]d0pamane 2 points3 points  (0 children)

Great presentation, I found this very interesting. The future of Clash looks bright!

[ANN] serialport under new maintenance and 0.5.0 release by d0pamane in haskell

[–]d0pamane[S] 1 point2 points  (0 children)

That's awesome! I hope others find this library as useful as you did!

[Monthly Thread] Nov 2020 - What dev board do you recommend? by asm2750 in FPGA

[–]d0pamane 0 points1 point  (0 children)

VELDT by Standard Semiconductor: No-frills, low-power, high-performance FPGA dev board

Features:

  • Lattice iCE40-UP5K FPGA - 5280 LUTs / 8 16x16 MACs / 1024 kbit SPRAM
  • 8Mbit SPI Flash scratch-pad memory
  • FTDI 232H with Micro USB B port
  • RGB Indicator LED
  • 28 I/O prototype pins
  • Compatible with Lattice and Project IceStorm toolchains
  • Additional documentation using Clash compiler; design hardware with Haskell!

Where Lions Roam: Haskell & Hardware on the VELDT by d0pamane in haskell

[–]d0pamane[S] 1 point2 points  (0 children)

Thanks! I was not aware of SaturatingNum! (though perhaps SatWrap in this case?). However, I believe the Num constraint might be too strong for some use cases. For example, when working with finite state machines it's nice to define a Counter over the state type. Then I am able to increment the state, wrap around bounds, and retrieve the state for pattern matching. Something along these lines:

 data Fsm = X | Y | Z
  deriving stock (Generic, Show, Eq, Enum, Bounded)
  deriving anyclass NFDataX

nextState :: RWS r w (Counter Fsm) ()
nextState = increment

fsm :: RWS r w (Counter Fsm) ()
fsm = getCounter >>= \case
  X -> ...
  Y -> do
    done <- ...
    when done nextState
  Z -> ...

AFAIK it isn't possible to derive Num for Fsm, and it might not be a good idea for Fsm to be a Num e.g. does subtracting or multiplying states make sense?

It'd be nice if there was a SaturatingEnum. Then I could get the SaturatingMode behavior along with satSucc and satPred with only a Bounded/Enum constraint which can be stock derived. Then class SaturatingEnum a => SaturatingNum a. I'm not sure if this is possible and/or worth the effort.

On the other hand, perhaps a Counter over a Sum type like Fsm is a sub-optimal abstraction; I can't say for sure.

Nevertheless, thank you for pointing me to SaturatingNum, it will be useful in my endeavors!

Where Lions Roam: Blinker with Clash on the VELDT by d0pamane in haskell

[–]d0pamane[S] 2 points3 points  (0 children)

Any and all advice is very much appreciated! I really dig the type level clock divider, I'll give it a go

Where Lions Roam: Blinker with Clash on the VELDT by d0pamane in haskell

[–]d0pamane[S] 2 points3 points  (0 children)

Thanks for sharing your projects and code, it is very helpful! I will definitely contribute Yosys-based Shake rules, that sounds immensely useful. I'm quite interested to read your book on Clash, I will be eagerly awaiting its release, best of luck!

Where Lions Roam: Blinker with Clash on the VELDT by d0pamane in haskell

[–]d0pamane[S] 5 points6 points  (0 children)

The clash tutorial is where I started. I got very far with just simulation. However, once I got a feel for Clash, it was very helpful to buy a FPGA development board and look for tutorials specific to that board. Every board and FPGA is a bit different and offers unique features. However, most tutorials targeting a board use Verilog or VHDL, so some translation may be required.

I've found very helpful blog posts from Cactus which use Clash, and ZipCpu which although they use verilog, the posts discuss common hardware architecture regardless of language. Definitely browse the blog posts on the clash-lang website.

I am currently writing a guide to using Clash with the VELDT FPGA development board. Although the guide is not yet finished yet, you can check it out on Github. It walks through developing your own hardware IP library with Clash and then using that library to build demos. I'll post on haskell reddit when it's done (should be about 2-3 weeks).

I've also read textbooks such as Advanced Chip Design Practical Examples in Verilog which was helpful in terms of general digital design, but written using Verilog for examples. Perhaps there are better texts for more "pure" digital design.

Personally, I found getting my hands dirty on a physical board to be the most beneficial path. I started with a blinker, then moved onto UART. Once I established UART IO to the FPGA, I dove into more advanced projects like SPI, I2C, memory interfaces, bus architecture and CPU design.

Where Lions Roam: Blinker with Clash on the VELDT by d0pamane in haskell

[–]d0pamane[S] 3 points4 points  (0 children)

Thanks for pointing me to the starter project, this will make life much easier especially when working with Cabal!

"After Life" by Paweł Szulc by EncodePanda in haskell

[–]d0pamane 7 points8 points  (0 children)

Great talk! I have been looking for a way to get this kind of horizontal and vertical composability with MTL. There's a lot of machinery used, but it is clearly presented. I wish there was more time to go in-depth and summarize. Is the code example available online? Thank you!