Tuesday, 2018-05-15

*** tpb has joined #yosys00:00
*** X-Scale has quit IRC00:19
*** dys has quit IRC00:28
*** X-Scale has joined #yosys00:32
*** emeb_mac has joined #yosys00:36
*** promach__ has joined #yosys00:40
*** cemerick_ has joined #yosys00:42
*** cemerick has joined #yosys00:48
*** cemerick_ has quit IRC00:51
*** sklv has quit IRC00:53
*** sklv has joined #yosys00:53
*** emeb has quit IRC00:56
*** leviathan has joined #yosys01:19
*** ZipCPU|Laptop has joined #yosys01:19
*** leviathan has quit IRC01:19
*** leviathan has joined #yosys01:19
*** cemerick has quit IRC01:22
*** pthomas has joined #yosys01:25
pthomasso 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
pthomasnow that there is risc-v we just need an open source eFPGA01:42
*** promach__ has quit IRC01:44
awyglepthomas: 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 IRC01:53
pthomasyeah I was looking through the ice40 datasheet, it's not all that complex02:26
*** proteusguy has quit IRC02:30
awyglewell, it is and it isn't lol. simple but lots of details.03:11
*** cr1901_modern has quit IRC03:11
awyglepthomas: you may also find this interesting03:12
tpbTitle: openfpga/hdl/xc2c-model at master · azonenberg/openfpga · GitHub (at github.com)03:12
awygleIt's a model of a cool runner II cpld03:12
sorearconversely 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 design03:16
*** cr1901_modern has joined #yosys03:17
*** seldridge has joined #yosys03:20
*** promach_ has quit IRC03:41
*** promach_ has joined #yosys03:48
*** proteusguy has joined #yosys04:20
*** promach_ has quit IRC04:31
*** promach_ has joined #yosys04:33
*** seldridge has quit IRC04:48
*** seldridge has joined #yosys04:52
*** seldridge has quit IRC05:11
*** dys has joined #yosys05:34
*** proteus-guy has quit IRC05:59
*** proteus-guy has joined #yosys06:00
*** promach_ has quit IRC06:29
*** emeb_mac has quit IRC06:32
*** GuzTech has joined #yosys07:03
*** GuzTech has quit IRC07:14
*** maartenBE has quit IRC07:33
*** maartenBE has joined #yosys07:34
*** dxld has quit IRC07:37
*** dxld has joined #yosys07:51
*** dmin7 has joined #yosys08:17
*** GuzTech has joined #yosys08:19
*** jwhitmore has joined #yosys08:33
*** promach_ has joined #yosys08:49
*** cemerick has joined #yosys09:08
*** ZipCPU|Laptop has quit IRC09:18
*** ZipCPU has joined #yosys09:26
*** ZipCPU|Alt has joined #yosys09:27
*** ZipCPU has quit IRC09:40
*** ZipCPU has joined #yosys09:41
*** ZipCPU has quit IRC09:46
*** ZipCPU has joined #yosys09:48
*** promach_ has quit IRC09:51
*** ZipCPU has quit IRC09:53
*** ZipCPU has joined #yosys09:55
*** promach_ has joined #yosys09:57
*** ZipCPU has quit IRC10:10
*** ZipCPU has joined #yosys10:10
*** ZipCPU|Laptop has joined #yosys10:30
*** ZipCPU|Alt has quit IRC10:50
*** jwhitmore has quit IRC11:12
*** jwhitmore has joined #yosys11:16
promach_ZipCPU, awygle: what kind of cover() do you guys have for UART ?11:30
*** jwhitmore has quit IRC11:42
*** jwhitmore has joined #yosys11:46
promach_what is the purpose of using cover() when we have induction ?11:47
*** digshadow has quit IRC11:48
ZipCPUpromach: I've found more than one bug by using cover in code that had already passed induction12:24
promach_I do not understand12:24
promach_Why would that happen ?12:24
ZipCPUThere are a couple reasons why it might happen.  For example, you might have made a careless assumption somewhere.12:25
ZipCPUSuch 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
ZipCPUIt can also catch bad logic as well.12:26
promach_how so ? induction and BMC should catch them all12:27
ZipCPUIn 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
ZipCPUI never caught it, since the bus would be in a perpetual stalled state.12:27
promach_huh ?12:27
*** dys has quit IRC12:27
ZipCPUIt 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
ZipCPUWhen I tried it on a DE10-nano, the device hung and hung hard on any attempted write.12:28
ZipCPUThe design had passed induction.12:28
promach_what ?12:28
ZipCPUIt didn't fail any assertions.12:28
ZipCPUIt just .... didn't work.12:28
promach_is your induction depth not suitable in that case ??12:29
ZipCPUIf 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 now12:30
promach_ok, cover() is to test whether what your logic coding really does what you had planned it to12:31
promach_I mean missing logic12:31
ZipCPUSo, there's a big difference between "safety" and "liveness" properties.12:31
promach_what ?12:31
promach_huh /12:31
ZipCPUassert/assume are "safety" properties.12:31
ZipCPUThe goal of the solver is to prove you wrong.  It can do this by finding one counter example.12:31
ZipCPUIf no counter example can be found, then your design must meet the safety properties.12:32
ZipCPUcover 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
ZipCPUAs 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
ZipCPUFor 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 #yosys12:34
promach_you mean cover() for my UART coding ?12:34
ZipCPUYes.  You don't remember that discussion?12:35
promach_I do12:35
promach_ZipCPU: https://github.com/ZipCPU/wbuart32/search?utf8=%E2%9C%93&q=cover&type=12:35
tpbTitle: Search · cover · GitHub (at github.com)12:36
*** webchat221 has joined #yosys12:37
promach_you didn't use cover() in your UART coding ?12:38
*** xrexeon has joined #yosys12:38
*** jwhitmore has quit IRC12:54
*** cr1901_modern1 has joined #yosys12:54
*** cemerick has quit IRC12:55
*** cemerick has joined #yosys12:56
*** cr1901_modern has quit IRC12:56
*** cr1901_modern1 has quit IRC12:58
*** cr1901_modern has joined #yosys12:59
*** jwhitmore has joined #yosys13:11
*** cr1901_modern has quit IRC13:46
*** cr1901_modern has joined #yosys13:49
*** dmin7 has quit IRC13:50
*** dmin7 has joined #yosys14:00
*** cemerick_ has joined #yosys14:13
*** cemerick has quit IRC14:17
*** seldridge has joined #yosys14:25
*** cemerick has joined #yosys14:39
*** dmin7 has quit IRC14:41
*** cemerick_ has quit IRC14:41
*** dmin7 has joined #yosys14:41
*** dmin7 has quit IRC14:47
*** dmin7 has joined #yosys15:00
*** dmin7 has quit IRC15:05
*** seldridge has quit IRC15:09
*** jwhitmore has quit IRC15:42
*** jwhitmore has joined #yosys15:49
*** dmin7 has joined #yosys15:53
*** seldridge has joined #yosys15:54
*** GuzTech has quit IRC16:04
*** quigonjinn has joined #yosys16:13
*** Ahadnagy has joined #yosys16:24
*** Ahadnagy has quit IRC16:24
*** emeb has joined #yosys16:52
*** m_w has quit IRC16:56
*** digshadow has joined #yosys17:14
*** clifford has quit IRC17:18
*** jwhitmore has quit IRC17:22
*** GuzTech has joined #yosys17:27
*** dys has joined #yosys17:38
*** ZipCPU|Laptop has quit IRC17:48
*** digshadow has quit IRC18:26
*** digshadow has joined #yosys18:31
*** leviathan has quit IRC18:31
*** digshadow has quit IRC18:32
shapry0 y0 y0sys!18:37
* shapr hops randomly18:37
shaprI had WAY more caffeine today.18:37
*** jwhitmore has joined #yosys18:41
awyglemmm.... caffeine.18:41
shapr1.5 grams18:42
shaprwell, 1374mg if the packaging is accurate18:42
awyglei have zero idea but that sounds like a lot18:42
shaprI've read the average cup of coffee is 180-200mg18:43
awyglei feel like "the average cup of coffee" is reported at 8oz which is comically small18:43
awygle"The average caffeine content of an 8-oz, brewed cup of coffee is 95 mg" ok so 200mg seems reasonable then18:44
awyglein which case i am at about 300 mg, maybe a bit more, and working on the next hundred18:44
shaprso, only ~six cups of coffee18:44
*** digshadow has joined #yosys18:46
shaprawygle: I learned much from your livestream, looking forward to the next one18:46
awygleshapr: thanks! i meant to do one on sunday but i got sick :(18:47
shaprone of my coworkers did motherboard power design for Sun Microsystem for a few years18:47
shaprI was describing what I learned about 'stacking' and then he wanted to see your saved livestream18:48
shaprbut they're not saved, are you planning on saving them in the future?18:48
shapror does that cost money or something?18:48
awyglei sort of thought they automatically saved!18:48
awyglei will look at the twitch settings18:48
shaprhm, I couldn't find them, might be user error18:49
shaprI don't see them on the page: https://www.twitch.tv/awygle18:49
tpbTitle: Twitch (at www.twitch.tv)18:49
awyglenow i'm all paranoid your coworker is gonna flame me for not talking about inductance lol18:49
shapryou did talk about inductance18:49
shaprinductance = reactance + resistance18:50
shaprand changes in inductance cause signal reflection or other problems18:50
shaprand that's why the changes in stackup between dirtypcbs and oshpark are important to keep in mind18:50
awyglethat's impedance :)18:51
awyglebut 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 mentioned18:51
shaprI 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
awyglethat sounds like fun18:53
shapryeah, a neon relaxation oscillator is a very simple circuit18:53
awyglegotta take nominal precautions against high voltage18:54
shaprthey're pretty: https://twitter.com/shapr/status/70338010843073331218:59
qu1j0t3how big is that pile? ;-)18:59
shaprI think I have twenty or thirty, five different colors?19:01
qu1j0t3i didn't even know they came in all those colours19:02
awygleshapr: i found the checkbox! future streams will be stored19:15
*** dmin7 has quit IRC19:40
shaprawygle: hurrah!19:51
*** frystr is now known as strfry20:11
*** cr1901_modern has quit IRC20:29
*** cr1901_modern has joined #yosys20:30
*** mirage335 has quit IRC20:49
*** dxld has quit IRC20:50
*** dxld has joined #yosys20:51
*** mirage335 has joined #yosys21:14
*** ahadnagy has joined #yosys21:25
*** webchat221 has quit IRC21:25
*** cr1901_modern has quit IRC22:13
*** jwhitmore has quit IRC22:23
*** ahadnagy has quit IRC22:54
*** GuzTech has quit IRC23:09
*** digshadow has quit IRC23:11
*** cr1901_modern has joined #yosys23:28
*** emeb_mac has joined #yosys23:59

Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!