| *** tpb has joined #yosys | 00:00 | |
| *** X-Scale has quit IRC | 00:19 | |
| *** dys has quit IRC | 00:28 | |
| *** X-Scale has joined #yosys | 00:32 | |
| *** emeb_mac has joined #yosys | 00:36 | |
| *** promach__ has joined #yosys | 00:40 | |
| *** cemerick_ has joined #yosys | 00:42 | |
| *** cemerick has joined #yosys | 00:48 | |
| *** cemerick_ has quit IRC | 00:51 | |
| *** sklv has quit IRC | 00:53 | |
| *** sklv has joined #yosys | 00:53 | |
| *** emeb has quit IRC | 00:56 | |
| *** leviathan has joined #yosys | 01:19 | |
| *** ZipCPU|Laptop has joined #yosys | 01:19 | |
| *** leviathan has quit IRC | 01:19 | |
| *** leviathan has joined #yosys | 01:19 | |
| *** cemerick has quit IRC | 01:22 | |
| *** pthomas has joined #yosys | 01:25 | |
| pthomas | so what would it look like to design an FPGA in verilog? I know that seems backwards (which also makes it very hard to search for) | 01:38 |
|---|---|---|
| pthomas | now that there is risc-v we just need an open source eFPGA | 01:42 |
| *** promach__ has quit IRC | 01:44 | |
| awygle | pthomas: I recommend looking at project icestorm to get an idea of the internal layout of a real fpga. beyond that, it's verilog like any other (although it's probably auto-generated as FPGAs have a very regular structure) | 01:49 |
| *** AlexDaniel has quit IRC | 01:53 | |
| pthomas | yeah I was looking through the ice40 datasheet, it's not all that complex | 02:26 |
| *** proteusguy has quit IRC | 02:30 | |
| awygle | well, it is and it isn't lol. simple but lots of details. | 03:11 |
| *** cr1901_modern has quit IRC | 03:11 | |
| awygle | pthomas: you may also find this interesting | 03:12 |
| awygle | https://github.com/azonenberg/openfpga/tree/master/hdl/xc2c-model | 03:12 |
| tpb | Title: openfpga/hdl/xc2c-model at master · azonenberg/openfpga · GitHub (at github.com) | 03:12 |
| awygle | It's a model of a cool runner II cpld | 03:12 |
| sorear | conversely fpgas are simple enough and have enough weird subunits (very small async-read sync-write RAMs in Xilinx parts, individual flash transistors not part of storage arrays in Microsemi parts) that they're ideal candidates for non-synthesized design | 03:16 |
| *** cr1901_modern has joined #yosys | 03:17 | |
| *** seldridge has joined #yosys | 03:20 | |
| *** promach_ has quit IRC | 03:41 | |
| *** promach_ has joined #yosys | 03:48 | |
| *** proteusguy has joined #yosys | 04:20 | |
| *** promach_ has quit IRC | 04:31 | |
| *** promach_ has joined #yosys | 04:33 | |
| *** seldridge has quit IRC | 04:48 | |
| *** seldridge has joined #yosys | 04:52 | |
| *** seldridge has quit IRC | 05:11 | |
| *** dys has joined #yosys | 05:34 | |
| *** proteus-guy has quit IRC | 05:59 | |
| *** proteus-guy has joined #yosys | 06:00 | |
| *** promach_ has quit IRC | 06:29 | |
| *** emeb_mac has quit IRC | 06:32 | |
| *** GuzTech has joined #yosys | 07:03 | |
| *** GuzTech has quit IRC | 07:14 | |
| *** maartenBE has quit IRC | 07:33 | |
| *** maartenBE has joined #yosys | 07:34 | |
| *** dxld has quit IRC | 07:37 | |
| *** dxld has joined #yosys | 07:51 | |
| *** dmin7 has joined #yosys | 08:17 | |
| *** GuzTech has joined #yosys | 08:19 | |
| *** jwhitmore has joined #yosys | 08:33 | |
| *** promach_ has joined #yosys | 08:49 | |
| *** cemerick has joined #yosys | 09:08 | |
| *** ZipCPU|Laptop has quit IRC | 09:18 | |
| *** ZipCPU has joined #yosys | 09:26 | |
| *** ZipCPU|Alt has joined #yosys | 09:27 | |
| *** ZipCPU has quit IRC | 09:40 | |
| *** ZipCPU has joined #yosys | 09:41 | |
| *** ZipCPU has quit IRC | 09:46 | |
| *** ZipCPU has joined #yosys | 09:48 | |
| *** promach_ has quit IRC | 09:51 | |
| *** ZipCPU has quit IRC | 09:53 | |
| *** ZipCPU has joined #yosys | 09:55 | |
| *** promach_ has joined #yosys | 09:57 | |
| *** ZipCPU has quit IRC | 10:10 | |
| *** ZipCPU has joined #yosys | 10:10 | |
| *** ZipCPU|Laptop has joined #yosys | 10:30 | |
| *** ZipCPU|Alt has quit IRC | 10:50 | |
| *** jwhitmore has quit IRC | 11:12 | |
| *** jwhitmore has joined #yosys | 11:16 | |
| promach_ | ZipCPU, awygle: what kind of cover() do you guys have for UART ? | 11:30 |
| *** jwhitmore has quit IRC | 11:42 | |
| *** jwhitmore has joined #yosys | 11:46 | |
| promach_ | what is the purpose of using cover() when we have induction ? | 11:47 |
| *** digshadow has quit IRC | 11:48 | |
| ZipCPU | LOL! | 12:14 |
| promach_ | ? | 12:24 |
| ZipCPU | promach: I've found more than one bug by using cover in code that had already passed induction | 12:24 |
| promach_ | I do not understand | 12:24 |
| promach_ | Why would that happen ? | 12:24 |
| ZipCPU | There are a couple reasons why it might happen. For example, you might have made a careless assumption somewhere. | 12:25 |
| ZipCPU | Such an assumption would render the proof nearly meaningless. A cover statement can help find it. | 12:25 |
| promach_ | so, cover() helps to catch wrong assume() statement ? | 12:26 |
| ZipCPU | It can also catch bad logic as well. | 12:26 |
| promach_ | how so ? induction and BMC should catch them all | 12:27 |
| ZipCPU | In one case, I built an Avalon to WB bus bridge. I messed up the logic, and in the process prevented the converter from ever entering into the write state. | 12:27 |
| ZipCPU | I never caught it, since the bus would be in a perpetual stalled state. | 12:27 |
| promach_ | huh ? | 12:27 |
| *** dys has quit IRC | 12:27 | |
| ZipCPU | It would be stalled waiting to switch from the read state to the write state. | 12:28 |
| promach_ | why wouldn't induction help in this case ? | 12:28 |
| ZipCPU | When I tried it on a DE10-nano, the device hung and hung hard on any attempted write. | 12:28 |
| ZipCPU | The design had passed induction. | 12:28 |
| promach_ | what ? | 12:28 |
| ZipCPU | It didn't fail any assertions. | 12:28 |
| ZipCPU | It just .... didn't work. | 12:28 |
| promach_ | is your induction depth not suitable in that case ?? | 12:29 |
| ZipCPU | If the induction round passes, the depth is sufficient. There's not much more going on there. My induction depth was sufficient. | 12:29 |
| promach_ | I got it now | 12:30 |
| promach_ | ok, cover() is to test whether what your logic coding really does what you had planned it to | 12:31 |
| promach_ | I mean missing logic | 12:31 |
| ZipCPU | So, there's a big difference between "safety" and "liveness" properties. | 12:31 |
| promach_ | what ? | 12:31 |
| promach_ | huh / | 12:31 |
| ZipCPU | assert/assume are "safety" properties. | 12:31 |
| ZipCPU | The goal of the solver is to prove you wrong. It can do this by finding one counter example. | 12:31 |
| ZipCPU | If no counter example can be found, then your design must meet the safety properties. | 12:32 |
| ZipCPU | cover is a "liveness" property. The goal of the solver here is to find one example to show that it is possible to be right. | 12:32 |
| ZipCPU | As I understand things, there's a healthy debate regarding whether or not liveness properties are necessary. Mathematically, as I recall, they are not. Practically, they often help find things you would otherwise miss. | 12:33 |
| ZipCPU | For example, when I was trying to debug your design, I added some cover properties at one point so that I could "see" what was (or in this case wasn't) going on. | 12:33 |
| *** AlexDaniel has joined #yosys | 12:34 | |
| promach_ | you mean cover() for my UART coding ? | 12:34 |
| ZipCPU | Yes. You don't remember that discussion? | 12:35 |
| promach_ | I do | 12:35 |
| promach_ | ZipCPU: https://github.com/ZipCPU/wbuart32/search?utf8=%E2%9C%93&q=cover&type= | 12:35 |
| tpb | Title: Search · cover · GitHub (at github.com) | 12:36 |
| *** webchat221 has joined #yosys | 12:37 | |
| promach_ | you didn't use cover() in your UART coding ? | 12:38 |
| *** xrexeon has joined #yosys | 12:38 | |
| *** jwhitmore has quit IRC | 12:54 | |
| *** cr1901_modern1 has joined #yosys | 12:54 | |
| *** cemerick has quit IRC | 12:55 | |
| *** cemerick has joined #yosys | 12:56 | |
| *** cr1901_modern has quit IRC | 12:56 | |
| *** cr1901_modern1 has quit IRC | 12:58 | |
| *** cr1901_modern has joined #yosys | 12:59 | |
| *** jwhitmore has joined #yosys | 13:11 | |
| *** cr1901_modern has quit IRC | 13:46 | |
| *** cr1901_modern has joined #yosys | 13:49 | |
| *** dmin7 has quit IRC | 13:50 | |
| *** dmin7 has joined #yosys | 14:00 | |
| *** cemerick_ has joined #yosys | 14:13 | |
| *** cemerick has quit IRC | 14:17 | |
| *** seldridge has joined #yosys | 14:25 | |
| *** cemerick has joined #yosys | 14:39 | |
| *** dmin7 has quit IRC | 14:41 | |
| *** cemerick_ has quit IRC | 14:41 | |
| *** dmin7 has joined #yosys | 14:41 | |
| *** dmin7 has quit IRC | 14:47 | |
| *** dmin7 has joined #yosys | 15:00 | |
| *** dmin7 has quit IRC | 15:05 | |
| *** seldridge has quit IRC | 15:09 | |
| *** jwhitmore has quit IRC | 15:42 | |
| *** jwhitmore has joined #yosys | 15:49 | |
| *** dmin7 has joined #yosys | 15:53 | |
| *** seldridge has joined #yosys | 15:54 | |
| *** GuzTech has quit IRC | 16:04 | |
| *** quigonjinn has joined #yosys | 16:13 | |
| *** Ahadnagy has joined #yosys | 16:24 | |
| *** Ahadnagy has quit IRC | 16:24 | |
| *** emeb has joined #yosys | 16:52 | |
| *** m_w has quit IRC | 16:56 | |
| *** digshadow has joined #yosys | 17:14 | |
| *** clifford has quit IRC | 17:18 | |
| *** jwhitmore has quit IRC | 17:22 | |
| *** GuzTech has joined #yosys | 17:27 | |
| *** dys has joined #yosys | 17:38 | |
| *** ZipCPU|Laptop has quit IRC | 17:48 | |
| *** digshadow has quit IRC | 18:26 | |
| *** digshadow has joined #yosys | 18:31 | |
| *** leviathan has quit IRC | 18:31 | |
| *** digshadow has quit IRC | 18:32 | |
| shapr | y0 y0 y0sys! | 18:37 |
| * shapr hops randomly | 18:37 | |
| shapr | I had WAY more caffeine today. | 18:37 |
| *** jwhitmore has joined #yosys | 18:41 | |
| awygle | mmm.... caffeine. | 18:41 |
| shapr | 1.5 grams | 18:42 |
| shapr | well, 1374mg if the packaging is accurate | 18:42 |
| awygle | i have zero idea but that sounds like a lot | 18:42 |
| shapr | I've read the average cup of coffee is 180-200mg | 18:43 |
| awygle | i feel like "the average cup of coffee" is reported at 8oz which is comically small | 18:43 |
| awygle | "The average caffeine content of an 8-oz, brewed cup of coffee is 95 mg" ok so 200mg seems reasonable then | 18:44 |
| awygle | in which case i am at about 300 mg, maybe a bit more, and working on the next hundred | 18:44 |
| shapr | so, only ~six cups of coffee | 18:44 |
| *** digshadow has joined #yosys | 18:46 | |
| shapr | awygle: I learned much from your livestream, looking forward to the next one | 18:46 |
| awygle | shapr: thanks! i meant to do one on sunday but i got sick :( | 18:47 |
| shapr | one of my coworkers did motherboard power design for Sun Microsystem for a few years | 18:47 |
| shapr | I was describing what I learned about 'stacking' and then he wanted to see your saved livestream | 18:48 |
| shapr | but they're not saved, are you planning on saving them in the future? | 18:48 |
| shapr | or does that cost money or something? | 18:48 |
| awygle | i sort of thought they automatically saved! | 18:48 |
| awygle | i will look at the twitch settings | 18:48 |
| shapr | hm, I couldn't find them, might be user error | 18:49 |
| shapr | I don't see them on the page: https://www.twitch.tv/awygle | 18:49 |
| tpb | Title: Twitch (at www.twitch.tv) | 18:49 |
| awygle | now i'm all paranoid your coworker is gonna flame me for not talking about inductance lol | 18:49 |
| shapr | you did talk about inductance | 18:49 |
| shapr | inductance = reactance + resistance | 18:50 |
| shapr | and changes in inductance cause signal reflection or other problems | 18:50 |
| shapr | and that's why the changes in stackup between dirtypcbs and oshpark are important to keep in mind | 18:50 |
| awygle | that's impedance :) | 18:51 |
| shapr | whoops | 18:51 |
| awygle | but i talked about capacitance between trance and plane without talking about trace inductance. which is super in the weeds and not actually that important (i wasn't giving you the _math_ after all) but technically should have been mentioned | 18:51 |
| shapr | I have a big pile of fingertip sized neon bulbs that want 110V, I've wanted to make a PCB to wear them as pendants. | 18:51 |
| awygle | that sounds like fun | 18:53 |
| shapr | yeah, a neon relaxation oscillator is a very simple circuit | 18:53 |
| awygle | gotta take nominal precautions against high voltage | 18:54 |
| shapr | they're pretty: https://twitter.com/shapr/status/703380108430733312 | 18:59 |
| qu1j0t3 | yeah! | 18:59 |
| qu1j0t3 | lovely! | 18:59 |
| qu1j0t3 | how big is that pile? ;-) | 18:59 |
| shapr | I think I have twenty or thirty, five different colors? | 19:01 |
| qu1j0t3 | i didn't even know they came in all those colours | 19:02 |
| awygle | shapr: i found the checkbox! future streams will be stored | 19:15 |
| *** dmin7 has quit IRC | 19:40 | |
| shapr | awygle: hurrah! | 19:51 |
| *** frystr is now known as strfry | 20:11 | |
| *** cr1901_modern has quit IRC | 20:29 | |
| *** cr1901_modern has joined #yosys | 20:30 | |
| *** mirage335 has quit IRC | 20:49 | |
| *** dxld has quit IRC | 20:50 | |
| *** dxld has joined #yosys | 20:51 | |
| *** mirage335 has joined #yosys | 21:14 | |
| *** ahadnagy has joined #yosys | 21:25 | |
| *** webchat221 has quit IRC | 21:25 | |
| *** cr1901_modern has quit IRC | 22:13 | |
| *** jwhitmore has quit IRC | 22:23 | |
| *** ahadnagy has quit IRC | 22:54 | |
| *** GuzTech has quit IRC | 23:09 | |
| *** digshadow has quit IRC | 23:11 | |
| *** cr1901_modern has joined #yosys | 23:28 | |
| *** emeb_mac has joined #yosys | 23:59 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!