_mouvantsillage

I think that you could check Sozi: https://sozi.baierouge.fr A big rewrite of its documentation is in progress at: http://sozi.guide

I have been developing it since 2009 and I think it has become a nice and fun tool to use, but not always easy.

From the "About" section (http://sozi.guide/en/about-sozi.html):

Sozi is a piece of software for creating animated presentations. It is generally used to make visual aids for lectures or meetings. With Sozi, a presentation is not organized as a sequence of slides, but rather as a succession of viewpoints on a map that you explore. Sozi is quite versatile. Some creators have already used it for other purposes, for example to make animated infographics, websites, or interactive fiction.

Because Jupyter originates from the IPython project, hence the ipynb (IPython NoteBook) extension.

IPython initially was a monolithic project that offered the notebook interface and the Python kernel in a single release. When the notebook interface was moved to a separate project, I suppose they kept the file extension for backwards compatibility.

Changing username is allowed. You just need to ask by e-mail (see https://news.ycombinator.com/newsfaq.html).

I did it a few weeks ago and the change was effective a few hours later.

Now I think I understand what you mean.

For many hardware engineers, I think that the message-passing semantics is a conceptual framework for explaining how simulators work. It is considered as a "necessary evil" that must be taken into account when writing HDL code.

When I write VHDL, I don't think in terms of communicating processes. I think in terms of combinational and sequential circuits that I describe with processes. The description is written in a way that makes the synthesizer generate the hardware that I had in mind.

I see a possible explanation for this mindset: since only a subset of VHDL or Verilog is actually synthesizable, we cannot rely only on the language semantics to write code that will map to functional hardware.

While simulation is a well-established practice among digital hardware developers, I have the impression that formal verification is still largely ignored. I hope it changes as free tools are emerging such as SymbiYosys https://symbiyosys.readthedocs.io

While this is still a long-term goal, I am planning to experiment how formal verification can be used in Racket-based hardware tools.

My experience in the lower-level aspects of hardware synthesis is limited but I would love to explore this topic.

I use proprietary synthesis tools for FPGAs everyday but I do not develop them. My situation is similar to that of a software engineer who uses compilers and who could only explain how they work in general terms.

Author here.

This post is part of an ongoing experiment to use Racket as a platform for hardware description languages. Describing a RISC-V core in Racket is a step in this direction, but the ultimate goal is neither to use Racket itself as an HDL, nor to define an embedded hardware description DSL in Racket. The long-term goal is to create an HDL that would benefit from Racket's "language-oriented programming" facilities, with the ability to simulate digital hardware, but also to generate standard Verilog or VHDL.