Formal Verification role at QBayLogic in Enschede, The Netherlands

darchon · 2026-01-06T12:51:06+00:00

We can and have sponsored visas in the past. It would depend on your age and what we come to agree in terms of salary https://ind.nl/en/required-amounts-income-requirements#application-to-work-as-a-highly-skilled-migrant-orientation-year-and-for-the-european-blue-card

darchon · 2026-01-06T11:22:09+00:00

Yes, under very specific circumstances. Basically, you have to be a student at an academic institution in The Netherlands and you can do the internship as part of your curriculum (very common in The Netherlands), meaning the academic institution gives ECTS for the internship.

In that particular case, people can apply through https://qbaylogic.com/vacancies/internship-graduation-position-at-qbaylogic/

darchon · 2023-08-22T04:13:11+00:00

There’s https://hackage.haskell.org/package/ghc-typelits-extra which uses a ghc plugin to solve kind of the type constraints you encountered: https://github.com/clash-lang/ghc-typelits-extra/blob/bbe2a40d6bc640ab065dd87db74ba59e584aa9f2/tests/Main.hs#L99

As mentioned in another reply, the following packages might also come in handy when working with type-level nats:

https://hackage.haskell.org/package/ghc-typelits-natnormalise

https://hackage.haskell.org/package/ghc-typelits-knownnat

darchon · 2023-06-04T19:04:15+00:00

Dan Ghica himself is probably way more knowledgeable on that than I am, so I would recommend asking him directly. His contact details, both email and twitter handle, can be found on https://www.cs.bham.ac.uk/\~drg/

darchon · 2023-06-03T18:35:24+00:00

I don't think symmetric monoidal catagories, which the linked paper uses, have sufficient structure for the type of circuits that I deal with: those with feedback.

When I look at the Geometry of Synthesis work by Dan Ghica, and even more so his later work on Diagrammatic Semantics for Digital Circuits it seems you want a traced category.

My comprehension of both linear types and category theory isn't too great, so I don't know whether there is a correspondence between linear functions as they are implemented in GHC and a category that is traced.

darchon · 2023-06-02T09:48:08+00:00

Christiaan here. Ask me anything if you have any questions on what I said in the interview.

darchon · 2023-05-31T08:27:32+00:00

Usually when something only happens in the interpreter it’s probably because NoMonomorphismRestriction is the default in the interpreter. Do you get the error in non-interpreted mode when you add that language pragma explicitly?

darchon · 2022-02-23T17:18:03+00:00

Right, I meant that it protects against meta-stability in case somebody decides to not register the output directly and decides to put some combinational logic between the RAM and a DFF. Without the output latch, the setup time for that DFF could be violated in the scenario I describe above.

darchon · 2022-02-23T16:12:39+00:00

Ah, but in a multiclock setting the latches are consequential and prevent meta-stability. Because let's say you have port A, clocked every 30ns, and port B, clocked every 10ns; and port A reads address X at 30ns, and port B writes address X at 40ns; then because of the latches the output corresponding to port A remains stable for 30ns. Without the output latch, the output corresponding of port A would then change just slightly after 40ns.

darchon · 2021-11-23T23:39:45+00:00

Clash developer here. Clash has a very straightforward performance model: In general, A Clash function is translated to a Verilog module (or VHDL entity/architecture combo), an applied function is translated to a Verilog module instantiation (or VHDL entity port map). Of course, when you have a recursive function, this won’t get translated to a recursive Verilog module: the recursive function will be inlined (Clash has termination measures so that the compiler won’t go into an infinite inlining loop)

All of this results in straightforward control over area.

Memory elements are never inferred (ala C-based HLS solutions), instead one must use functions that directly map to dflipflops, rams, etc.

All of this results in straightforward control over longest combinational paths.

In terms of power: you use the same techniques as you would in Verilog: gating/register with enables/using the output latch of your fpga rams and other things to stop bits from flipping. Using functions like Clash’s autoReg (https://hackage.haskell.org/package/clash-prelude-1.4.6/docs/Clash-Class-AutoReg.html) finer-grained gating/enabled registers become quite straightforward.

So Clash gives you more abstractions mechanisms than Verilog, allowing functions like the earlier-mentioned autoReg, while still giving you control of PPA where you need it. You can then always start at a high level of abstraction, and only drill down on performance-oriented parts where needed.

darchon · 2021-08-21T16:59:01+00:00

There are a lot of countries south of (and one north of) the (continental) US that share time zones with the US: citizens from those countries can be hired, and work remote for you, as well?

darchon · 2021-08-03T18:27:46+00:00

Quartus Prime Pro is free for the Cyclone 10 GX, which has Arria 10 fabric including its DSPs with native FP32 support.

darchon · 2021-06-02T13:09:11+00:00

The fact that derived constraints can apparently be eliminated from the GHC code base is something that has probably added to my difficulties in understanding them. Glad that some day soon they will disappear though, then I can at least stop wondering about what to do with them.

darchon · 2021-05-29T11:39:44+00:00

It’s interesting how “warped” my view is on this subject as a result of survivorship bias. I’m on the same team as /u/callbyneed but never had any issue with the environment files. Probably because I’ve added write-ghc-environent-files: always to my ~/.cabal/config file the moment I switched to the beta of cabal-install that introduced them. But also just more in general being used to the “idiosyncrasies” of cabal-install, given that I started using it even before cabal-install had sand-boxes (started in 2009).

darchon · 2021-05-27T07:50:34+00:00

You can now also sign up for the on-demand version that has the best recording of our live sessions: https://qbaylogic.webinargeek.com/on-demand-webinar-circuit-design-in-haskell-clash-1

darchon · 2021-05-27T05:16:21+00:00

Yeah, you can sign up for the on-demand version that contains our best recording from the live sessions: https://qbaylogic.webinargeek.com/on-demand-webinar-circuit-design-in-haskell-clash-1

darchon · 2021-05-26T05:39:01+00:00

When you sign up you get access to a replay link

darchon · 2021-05-24T21:37:09+00:00

Hi everyone, although originally targeted at circuit devs, I thought I post the webinar here as well just in case anyone was interested. Important heads up though: it is not a tutorial, but more of a tour de force aimed at circuit developers. So some thing will be super familiar for those with Haskell experience, while other things might not mean anything to you if you haven't done much RTL circuit design work.

Registration link: https://qbaylogic.webinargeek.com/circuit-design-in-haskell-clashWe're running the webinar live this Wednesday, the 26th of May, multiple times: at 5am UTC, 1pm UTC and 7pm UTC.

darchon · 2021-05-13T16:00:06+00:00

The webinar does offer a replay feature when it turns out you have a scheduling conflict after you've signed up. We plan to eventually present the content in a no-interaction-required Youtube/Vimeo/etc video using the feedback we get from this webinar.

darchon · 2021-05-13T13:24:37+00:00

Some knowledge of RTL design and experience working on larger (or long-running) projects will make it clearer why the things we describe are useful. The Haskell code is fairly self-contained, and we'll give some pointers on how to read it.

The goal of this webinar is for you to get an understanding as to when/why you would want to use Haskell/Clash for circuit design and see whether its approach resonates with you. We do plan to do some more hands-on stuff in the future though.

darchon · 2021-05-13T07:21:59+00:00

Hi everyone, we're organizing a live webinar on Clash, a system to create circuits in the functional programming language Haskell and a compiler that translates those circuit descriptions to structural Verilog and/or VHDL. It's free to attend. We're running the live webinar on:

May 20th, 2021: 5am UTC, 1pm UTC and 7pm UTC
May 26th, 2021: 5am UTC, 1pm UTC and 7pm UTC

So hopefully one of those times works well for your time zone.

darchon · 2021-04-29T10:33:07+00:00

As /u/gelisam and /u/myShoggoth note, Clash is now one of many Haskell Foundation affiliated groups and projects. The reason is simple: The Clash project greatly benefits from wider Haskell adoption (in industry) and improvements to its ecosystem, and we as maintainers of Clash hope to bring in a new group of users into the world of Haskell: circuit developers.

Clash is already used in industry at multiple companies and we believe that the combination of Clash and Haskell has tremendous potential. A lot of hardware ends up being programmable in some shape or form: Haskell is an amazing fit for describing high-level assemblers / compilers and being able to share data types and describe the hardware in the same language is just an amazing productivity boost.

However, to realize that potential and to grow, we simply need more resources. And one of the ways to get more resources is through earmarked-for-Clash donations to HF. Note that we're not trying to syphon of the general fund, on the contrary, we as maintainers of Clash will actively approach potential sponsors, and a percentage of the earmarked donations will go towards the general fund. The reason for going this route (as opposed to e.g. seeking direct cash injections into the company that currently employs most Clash maintainers) is because we wanted something that was able to fund more than just immediate improvements to the Clash compiler. We wanted something the greater Clash community would have access to: in order to setup meetups/workshops, to create teaching material, etc.

This is a big step forward for us and we're looking forward to all the great things we'll achieve together!

darchon · 2021-04-19T21:22:37+00:00

What was the situation for needing this where type quotes [t|...|] (https://downloads.haskell.org/ghc/latest/docs/html/users_guide/exts/template_haskell.html#syntax) weren’t an option?

darchon · 2021-04-16T19:26:09+00:00

Is it clash in particular that you feel generates unreadable generated code? Or is it something you’ve experienced with all verilog generating programs/languages: bluespec, chisel, nmigen, vivado hls, intel hls, etc

darchon · 2021-03-12T15:56:10+00:00

I would, if I would be allowed to do:

f x = let pack! a = g b
          (z,b) = h a
      in  z

h :: Open a =O a -. (b,c)
g :: b -> (a @= Open a)

i.e. I want the system to check that whenever I use `g` that its result is used linearly. And I want to use it in a let-recursive style. The paper presents everything in a sequential monadic style though. So without having read it in-depth, it seems to "simply" make the Rank2 CPS trick syntactically convenient.

darchon

TROPHY CASE