From 849522b730c204473efa93818c5729c291d2e7f3 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 11 Nov 2022 19:25:42 +0000 Subject: Add twitter archive --- content.org | 453 +++++++++++++++++++++ .../1318551572889194496-EkxrsAfXUAA1IQT.png | Bin 0 -> 120111 bytes .../1318551579151245322-Ekxs1bmXIAUQhbZ.png | Bin 0 -> 113883 bytes themes/ymherklotz/static/css/default.css | 1 - 4 files changed, 453 insertions(+), 1 deletion(-) create mode 100644 static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png create mode 100644 static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png diff --git a/content.org b/content.org index acea238..4c2ba15 100644 --- a/content.org +++ b/content.org @@ -1735,6 +1735,459 @@ The following is a non-exhaustive list of books I've read. - /Why We Sleep/, by Mathew Walker - /On Writing Well/, by William Zinsser +* Twitter +:PROPERTIES: +:EXPORT_FILE_NAME: _index +:EXPORT_HUGO_SECTION: twitter +:END: + +*@watislaw* *@notypes* Yep that's very fair + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532392678100455424][Thu Jun 02 16:04:19 +0000 2022]]) + +-------------- + +*@watislaw* *@notypes* But this +https://twitter.com/watislaw/status/1532380177254187009?s=20&t=FI55wZOiaasTGO7ezfp11Q +does explain why assign can be modelled as ~always_comb~ and not ~always @*~. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532391377207758850][Thu Jun 02 15:59:09 +0000 2022]]) + +-------------- + +*@watislaw* *@notypes* Yeah OK, I just took their word but it would have been +better with a reference! But OK, I really need to look more at ~always_comb~ vs +~always @*~, because I thought that even with no multidriven and no delays, +~assign != always @*~. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532390966572769283][Thu Jun 02 15:57:31 +0000 2022]]) + +-------------- + +*@watislaw* *@notypes* What's not quite right? That ~assign~ can be modelled as +~always @*~? Because I think they agree with that in the paper. They really only +say that the standard says that this should be done, but even without +multidriven nets it has inconsistencies. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532385129020153857][Thu Jun 02 15:34:19 +0000 2022]]) + +-------------- + +*@notypes* This assumes using blocking assignment inside of the combinational +always block though. Also *@watislaw* might be able to add a better explanation! + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532382576362528769][Thu Jun 02 15:24:11 +0000 2022]]) + +-------------- + +*@notypes* Meredith et +al. (https://ieeexplore.ieee.org/abstract/document/5558634) try to address +this. They state the Verilog standard basically says that the semantics of +src_verilog[:exports code]{assign x = y;} should be handled like +src_verilog[:exports code]{always @* x = y;} But say that this can lead to +inconsistencies between the "hardware semantics" and simulation + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1532381674851409921][Thu Jun 02 15:20:36 +0000 2022]]) + +-------------- + +I have also now created a poster for *@splashcon* about our paper on "Formal +Verification High-Level Synthesis" that we are presenting on Friday 22nd at +20:05 BST at OOPLSA'21! Here is a summary thread about the paper. 1/7 + +https://yannherklotz.com/docs/splash21/poster.pdf + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063840343887873][Mon Oct 18 11:38:55 +0000 2021]]) + +-------------- + +FPGAs are a great alternative to CPUs for many low-power applications, because +the circuit can be specialised to each application. An FPGA is traditionally +programmed using a logic synthesis tool by writing in a hardware description +language like Verilog. 2/7 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063842554298368][Mon Oct 18 11:38:55 +0000 2021]]) + +-------------- + +However, writing Verilog can be quite daunting if one doesn't have hardware +design experience, and it can also take a long time to test and get right. + +One alternative to this is high-level synthesis (HLS), allowing you to write C +which will get translated into Verilog. 3/7 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063844253093896][Mon Oct 18 11:38:56 +0000 2021]]) + +-------------- + +Current HLS tools focus on generating optimal Verilog, however, they can be +quite unreliable because of that, negating any testing that was done on the C +code. This means the generated Verilog needs to be thoroughly tested again. 4/7 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063845918224384][Mon Oct 18 11:38:56 +0000 2021]]) + +-------------- + +Our solution is Vericert, a formally verified HLS tool, so that any guarantees +made in C also automatically translate to the Verilog code. Vericert is based +on the CompCert C compiler, so that it can translate C code into Verilog. 5/7 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063847587467267][Mon Oct 18 11:38:56 +0000 2021]]) + +-------------- + +The bad news is that we are 27x slower than an existing optimised HLS tools when +divisions are present, as we implement divisions naïvely in Verilog. + +However, the better news is, with division implemented as an iterative +algorithm, we are only 2x slower. 6/7 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063849231638529][Mon Oct 18 11:38:57 +0000 2021]]) + +-------------- + +If you are interested in knowing more, I have added links to a blog post, our +paper, and our GitHub repository: 7/7 + +- https://vericert.ymhg.org/2021/10/a-first-look-at-vericert/ +- https://doi.org/10.1145/3485494 +- https://github.com/ymherklotz/vericert + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1450063850963968006][Mon Oct 18 11:38:57 +0000 2021]]) + +-------------- + +*@jinxmirror13* *@CamlisOrg* *@kaixhin* *@LboroVC* Congrats!!! Enjoy attending +in person! 🎉 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446958594835075072][Sat Oct 09 21:59:46 +0000 2021]]) + +-------------- + +*@lorisdanto* Thanks! + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446958086678319107][Sat Oct 09 21:57:45 +0000 2021]]) + +-------------- + +*@jinxmirror13* Thank youu!! + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446958044462686212][Sat Oct 09 21:57:35 +0000 2021]]) + +-------------- + +I have finally gotten around to writing an introductory blog post about +Vericert, our formally verified HLS tool that we will be presenting on Friday +22nd at OOPSLA'21! + +https://vericert.ymhg.org/2021/09/a-first-look-at-vericert/ + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1446828476833619968][Sat Oct 09 13:22:44 +0000 2021]]) + +-------------- + +*@watislaw* *@jfdm* That sounds really interesting actually. I have realised +that I don't really know too much about the details of synthesis myself, so +might try building a simple one using Lutsig as an example. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437437352809488391][Mon Sep 13 15:25:45 +0000 2021]]) + +-------------- + +*@jfdm* Which parts did you find hand wavy? + +I hope it does, but the main overlap between this and Lutsig is the Verilog +semantics, and we only really go into details about the differences. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437384017293291520][Mon Sep 13 11:53:49 +0000 2021]]) + +-------------- + +Just finished the camera ready version of our (with *@wicko3*, *@nadeshr5* and +James Pollard) paper "Formal Verification of High-Level Synthesis", which will +be presented at OOPSLA'21 *@splashcon*! + +Stay tuned for a blog post about this paper soon. + +https://yannherklotz.com/papers/fvhls_oopsla21.pdf + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437358477119270916][Mon Sep 13 +10:12:20 +0000 2021]]) + +-------------- + +Although my supervisor *@wicko3* has already written a great summary of the +paper! + +https://johnwickerson.wordpress.com/2021/08/27/vericert/ + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1437358478734118915][Mon Sep 13 10:12:20 +0000 2021]]) + +-------------- + +*@gabeusse* *@gconstantinides* *@imperialcas* @jianyi_cheng* *@Stanford* *@UCLA* +**@Penn* Yep, our short paper preprint is available here: + +https://yannherklotz.com/papers/esrhls_fccm2021.pdf + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1392202613769244678][Tue May 11 19:39:03 +0000 2021]]) + +-------------- + +RT *@wicko3*: Here is a short blog post about an #FCCM2021 paper that will be +presented next week by *@ymherklotz* about our work (with Zewei D... + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1390670893798629382][Fri May 07 14:12:33 +0000 2021]]) + +-------------- + +*@wicko3* I'll have to read that then, it seems like it is a very nice +introduction to concurrent computation as well. + +Bigraphs seem really interesting though because such a visual representation can +describe distributed computations. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1341516552500359168][Tue Dec 22 22:50:44 +0000 2020]]) + +-------------- + +*@wicko3* Oh interesting! I haven't heard of those before, but it makes sense +that there is a formalisation. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1341512000984281088][Tue Dec 22 22:32:39 +0000 2020]]) + +-------------- + +Decided to write a bit about a note-taking method that finally seems to work for +me, following closely how Niklas Luhmann took his notes in his famous +Zettelkasten. Currently using #emacs with #orgmode which works perfectly for it. + +https://yannherklotz.com/blog/2020-12-21-introduction-to-luhmanns-zettelkasten.html + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1341145333083107328][Mon Dec 21 22:15:39 +0000 2020]]) + +-------------- + +*@gconstantinides* Thank you! Glad to have had such a great discussion. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1328760838900113408][Tue Nov 17 18:04:05 +0000 2020]]) + +-------------- + +*@watislaw* I was actually doing the same which is why I came across this weird +behaviour. I think this is a similar example to the one I gave, where single +always blocks never recurse, and therefore don't update signals again. Here when +they are separated they never reach a steady state. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318852927814045696][Wed Oct 21 09:53:35 +0000 2020]]) + +-------------- + +*@watislaw* Yes that's true, and I think in this case they do actually follow +the standard correctly, even though I would expect them to recurse in the same +always block when signals in the sensitivity list change and maybe reach some +steady state, although I don't know how feasible that is. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318561007770488832][Tue Oct 20 14:33:36 +0000 2020]]) + +-------------- + +*@watislaw* That's exactly what I was looking for actually, I must have missed +it in the standard, thanks! I was looking in the combinational circuits part. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318560200673140746][Tue Oct 20 14:30:24 +0000 2020]]) + +-------------- + +However, synthesis tools will produce the following netlist, where the input is +directly connected to the output. Is this a bug in the simulator or the +synthesis tool? Or is this mismatch correct and should that be the case? + +[[file:./static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png]] + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318551579151245322][Tue Oct 20 13:56:08 +0000 2020]]) + +-------------- + +What should the following Verilog design produce? + +Should it be a latched shift register, where the output is equal to the previous +input? + +Or should it be a direct assignment from input to output? + +[[file:./static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png]] + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318551572889194496][Tue Oct 20 13:56:07 +0000 2020]]) + +-------------- + +Even this simple piece of Verilog has ambiguities in Simulation and Synthesis. + +Simulators will just execute the always block when the input changes, and the +output will therefore be set to the previous value of the input. + +The whole testbench is here: + +https://gist.github.com/ymherklotz/e8600f8c2e1564f4679fe3a99146a874 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1318551574793359360][Tue Oct 20 13:56:07 +0000 2020]]) + +-------------- + +Vericert is written in Coq and will allow for a trustworthy, verified +translation from C to Verilog using CompCert as the front end. + +This eliminates the need to manually verify the correctness of the generated +hardware, which is tedious and expensive. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1286616989583265792][Fri Jul 24 10:59:29 +0000 2020]]) + +-------------- + +We just made our (James Pollard, *@nadeshr5*, *@wicko3*) work-in-progress +formally verified high-level synthesis tool Vericert public! + +https://github.com/ymherklotz/vericert + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1286616987871981568][Fri Jul 24 10:59:28 +0000 2020]]) + +-------------- + +*@kumastz* *@wicko3* Thanks!! + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1273726889367080963][Thu Jun 18 21:18:49 +0000 2020]]) + +-------------- + +*@Helidcotor22* *@wicko3* Thank you! + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1273726579697483777][Thu Jun 18 21:17:35 +0000 2020]]) + +-------------- + +I really enjoyed the student research competition at #PLDI2020 enjoyed talking +to everyone who came by my poster and also got great feedback from the judges! +https://twitter.com/wicko3/status/1273710075966885889 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1273723966046318593][Thu Jun 18 21:07:12 +0000 2020]]) + +-------------- + +Really enjoyed presenting our work on fuzzing synthesis tools at #FPGA2020 +https://twitter.com/gconstantinides/status/1232464094659104768 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1232466970500456449][Wed Feb 26 00:46:38 +0000 2020]]) + +-------------- + +*@wicko3* I'm guessing because it's a package manager for *nix systems. Makes it +really hard to google for errors though because it just comes up with linux +search results. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1229156715637223424][Sun Feb 16 21:32:52 +0000 2020]]) + +-------------- + +Been using Coq with OCaml extraction lately, with various dependencies for both +and have found Nix really useful to build the project reliably and on different +platforms. + +Wrote a post on how to set up a quick derivation for Coq. + +https://yannherklotz.com/blog/2020-02-15-nix-for-coq-development.html + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1229149071790747649][Sun Feb 16 21:02:29 +0000 2020]]) + +-------------- + +Congratulations Dr. He Li !!!! + +https://twitter.com/DrHelicopter2/status/1228018755072073729 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1228095080105435136][Thu Feb 13 23:14:18 +0000 2020]]) + +-------------- + +*@fangyi_zhou_* You could try out Nix, been working great for me for Coq and +Ocaml. + +https://nixos.org/nix/ + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1224983007406317568][Wed Feb 05 09:08:02 +0000 2020]]) + +-------------- + +*@jianyi_cheng* Looking forward to the presentation! + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1206378185027411971][Mon Dec 16 00:59:07 +0000 2019]]) + +-------------- + +The final version of our FPGA '20 paper "Finding and Understanding Bugs in FPGA +Synthesis Tools" is now ready. + +We added many more runs for various Yosys versions and have now managed to +properly test Quartus. + +https://yannherklotz.com/papers/fubfst_fpga2020.pdf + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1206300348656291842][Sun Dec 15 19:49:49 +0000 2019]]) + +-------------- + +Congrats Sina!! + +https://twitter.com/sinaxs/status/1205115213411950595 + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1205952393038446592][Sat Dec 14 20:47:10 +0000 2019]]) + +-------------- + +*@tom_verbeure* *@johnregehr* *@whitequark* @oe1cxw* Most of the bugs found in +*Yosys were in the optimisation passes, which I don't think are applied when +*Yosys passes the design to ABC or an SMT solver, so these were not affected. We +*are looking into using multiple equivalence checkers so that these are tested +*at the same time. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193947458621116419][Mon Nov 11 17:43:51 +0000 2019]]) + +-------------- + +*@johnregehr* *@whitequark* *@oe1cxw* Link to VlogHammer: + +http://www.clifford.at/yosys/vloghammer.html + +There is also a random Verilog generation tool called VERGEN from 2003, but I +don't think it was used to fuzz existing tools properly. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193940002637590528][Mon Nov 11 17:14:13 +0000 2019]]) + +-------------- + +*@johnregehr* *@whitequark* *@oe1cxw* has written a tool called VlogHammer which +focused on fuzzing expressions in synthesis tools and also reported many bugs to +these vendors. However, these took a long time to fix in commercial tools and +some still are not fixed. + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193938897560121344][Mon Nov 11 17:09:50 +0000 2019]]) + +-------------- + +*@jrenauardevol* *@johnregehr* *@mithro* Yes, currently hosted on github: + +https://github.com/ymherklotz/verismith + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1193922618388340741][Mon Nov 11 16:05:08 +0000 2019]]) + +-------------- + +Currently working on my Entity Component System for my game engine! More info at + +https://github.com/ymherklotz/YAGE + +(Originally on Twitter: [[https://twitter.com/ymherklotz/status/1008858830216880128][Mon Jun 18 23:47:43 +0000 2018]]) + * Photos :PROPERTIES: :EXPORT_FILE_NAME: _index diff --git a/static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png b/static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png new file mode 100644 index 0000000..cc6e4ea Binary files /dev/null and b/static/images/twitter/1318551572889194496-EkxrsAfXUAA1IQT.png differ diff --git a/static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png b/static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png new file mode 100644 index 0000000..72a0f61 Binary files /dev/null and b/static/images/twitter/1318551579151245322-Ekxs1bmXIAUQhbZ.png differ diff --git a/themes/ymherklotz/static/css/default.css b/themes/ymherklotz/static/css/default.css index f9e7ef3..0aa1b1f 100644 --- a/themes/ymherklotz/static/css/default.css +++ b/themes/ymherklotz/static/css/default.css @@ -170,7 +170,6 @@ body { p { margin-top: 0.5em; - text-align: justify; hyphens: auto; } -- cgit