<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)
<pthomas>
now that there is risc-v we just need an open source eFPGA
promach__ has quit [Quit: WeeChat 2.1]
<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)
AlexDaniel has quit [Ping timeout: 260 seconds]
<pthomas>
yeah I was looking through the ice40 datasheet, it's not all that complex
proteusguy has quit [Ping timeout: 255 seconds]
<awygle>
well, it is and it isn't lol. simple but lots of details.
cr1901_modern has quit [Read error: Connection reset by peer]
<awygle>
pthomas: you may also find this interesting
<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
cr1901_modern has joined #yosys
seldridge has joined #yosys
promach_ has quit [Quit: WeeChat 2.1-dev]
promach_ has joined #yosys
proteusguy has joined #yosys
promach_ has quit [Quit: WeeChat 2.1-dev]
promach_ has joined #yosys
seldridge has quit [Ping timeout: 265 seconds]
seldridge has joined #yosys
seldridge has quit [Ping timeout: 240 seconds]
dys has joined #yosys
proteus-guy has quit [Read error: Connection reset by peer]
proteus-guy has joined #yosys
promach_ has quit [Quit: WeeChat 2.1-dev]
emeb_mac has quit [Quit: Leaving.]
GuzTech has joined #yosys
GuzTech has quit [Ping timeout: 248 seconds]
maartenBE has quit [Ping timeout: 240 seconds]
maartenBE has joined #yosys
dxld has quit [Remote host closed the connection]
dxld has joined #yosys
dmin7 has joined #yosys
GuzTech has joined #yosys
jwhitmore has joined #yosys
promach_ has joined #yosys
cemerick has joined #yosys
ZipCPU|Laptop has quit [Read error: Connection reset by peer]
ZipCPU has joined #yosys
ZipCPU|Alt has joined #yosys
ZipCPU has quit [Ping timeout: 256 seconds]
ZipCPU has joined #yosys
ZipCPU has quit [Ping timeout: 260 seconds]
ZipCPU has joined #yosys
promach_ has quit [Quit: WeeChat 2.1-dev]
ZipCPU has quit [Ping timeout: 264 seconds]
ZipCPU has joined #yosys
promach_ has joined #yosys
ZipCPU has quit [Ping timeout: 240 seconds]
ZipCPU has joined #yosys
ZipCPU|Laptop has joined #yosys
ZipCPU|Alt has quit [Quit: Cap'n! The dilithium crystals are ...]
jwhitmore has quit [Ping timeout: 256 seconds]
jwhitmore has joined #yosys
<promach_>
ZipCPU, awygle: what kind of cover() do you guys have for UART ?
jwhitmore has quit [Ping timeout: 265 seconds]
jwhitmore has joined #yosys
<promach_>
what is the purpose of using cover() when we have induction ?
digshadow has quit [Quit: Leaving.]
<ZipCPU>
LOL!
<promach_>
?
<ZipCPU>
promach: I've found more than one bug by using cover in code that had already passed induction
<promach_>
I do not understand
<promach_>
Why would that happen ?
<ZipCPU>
There are a couple reasons why it might happen. For example, you might have made a careless assumption somewhere.
<ZipCPU>
Such an assumption would render the proof nearly meaningless. A cover statement can help find it.
<promach_>
so, cover() helps to catch wrong assume() statement ?
<ZipCPU>
It can also catch bad logic as well.
<promach_>
how so ? induction and BMC should catch them all
<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.
<ZipCPU>
I never caught it, since the bus would be in a perpetual stalled state.
<promach_>
huh ?
dys has quit [Ping timeout: 240 seconds]
<ZipCPU>
It would be stalled waiting to switch from the read state to the write state.
<promach_>
why wouldn't induction help in this case ?
<ZipCPU>
When I tried it on a DE10-nano, the device hung and hung hard on any attempted write.
<ZipCPU>
The design had passed induction.
<promach_>
what ?
<ZipCPU>
It didn't fail any assertions.
<ZipCPU>
It just .... didn't work.
<promach_>
is your induction depth not suitable in that case ??
<ZipCPU>
If the induction round passes, the depth is sufficient. There's not much more going on there. My induction depth was sufficient.
<promach_>
I got it now
<promach_>
ok, cover() is to test whether what your logic coding really does what you had planned it to
<promach_>
I mean missing logic
<ZipCPU>
So, there's a big difference between "safety" and "liveness" properties.
<promach_>
what ?
<promach_>
huh /
<ZipCPU>
assert/assume are "safety" properties.
<ZipCPU>
The goal of the solver is to prove you wrong. It can do this by finding one counter example.
<ZipCPU>
If no counter example can be found, then your design must meet the safety properties.
<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.
<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.
<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.
<awygle>
now i'm all paranoid your coworker is gonna flame me for not talking about inductance lol
<shapr>
you did talk about inductance
<shapr>
inductance = reactance + resistance
<shapr>
and changes in inductance cause signal reflection or other problems
<shapr>
and that's why the changes in stackup between dirtypcbs and oshpark are important to keep in mind
<awygle>
that's impedance :)
<shapr>
whoops
<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
<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.
<awygle>
that sounds like fun
<shapr>
yeah, a neon relaxation oscillator is a very simple circuit
<awygle>
gotta take nominal precautions against high voltage