<sorear>
coq (which I'm using as a metonym for classical proof assistants, I don't actually use coq per se) uses the axioms of logic to prove possibly infinitary statements
<sorear>
SMT solvers use clever heuristics to check finitary statements faster than brute force
<cr1901_modern>
It's also much more daunting to get started w/ coq and friends than SMT
<cr1901_modern>
I can't do it at present anyway
<sorear>
I've used them, but only for infinitary mathematics
<ZipCPU>
Care for my exciting news tonight? I finally managed to formally verify an SDRAM controller. ;)
<cr1901_modern>
I've never built an SDRAM contoller. I know I know, it's a rite of passage
<ZipCPU>
Nah ... the UART is the right of passage. The SDRAM controller you build 'cause you need it.
pie__ has joined #yosys
<Kooda>
Hi there! Noob question here: is it possible to use a PLL with the IceStorm toolchain? I can’t find any documentation about that appart from icepll. I use a HX8K CT256 chip.
<ZipCPU>
icepll is the only way I know of to do it.
<ZipCPU>
It is possible to do.
<Kooda>
Well it doesn’t do anything, it just calculates values.
<ZipCPU>
Actually, I was doing it before icepll ... just doing it wrong. ;)
<ZipCPU>
Want an example?
<Kooda>
I can’t find documentation on how to use them.
<Kooda>
(I’m a Verilog and FPGA noob)
<ZipCPU>
Much of it is within the iCE40 family handbook.
<ZipCPU>
... at least ... that's the documentation I had managed to find.
<Kooda>
I tried dividing my clock manually, but it’s not precise enough apparently.
<ZipCPU>
Ah ... ok, ahm, ... uh oh ...
<ZipCPU>
there is a bug/restriction in some of the iCE40 boards.
<ZipCPU>
It's a strange bug that has caught several by surprise.
<ZipCPU>
It has to do with certain pins that cannot be placed in an I/O mode when the PLL is used.
<ZipCPU>
Dividing manually in those circumstances is actually better.
<Kooda>
Hm
<ZipCPU>
What clock rate do you need?
<Kooda>
25.175 MHz (VGA)
<ZipCPU>
yeah, okay ... I think I've been successful before at 25MHz, but you will need the PLL to get that exactly.
<Kooda>
I divided my 100 MHz clock to 25 MHz, but the monitors just blink on and off all the time
<ZipCPU>
Yeah, okay, that's a good reason to go for the "right" frequency.
<Kooda>
The PLL would be closer yep
<cr1901_modern>
Most monitors will tolerate 25MHz
<cr1901_modern>
I suspect your problem is elsewhere, tbh
<ZipCPU>
I debugged my last VGA controller using Verilator. I found it very valuable. I could write a C++ routine to verify and assert() that the timings were done properly, as well as to display what I wanted to place onto the screen in a nice X-Window on my desktop.
<ZipCPU>
If I had to do it again, that's where I'd start.
<Kooda>
cr1901_modern: I tried some code from other people, and it does the same.
<cr1901_modern>
hmmm
<awygle>
Kooda: did you get icepll working?
<Kooda>
Trying it out now
<Kooda>
I had to tidy up my desk a little x)
<awygle>
You should be able to use -fm to get a verilog module you can just drop into your project
<Kooda>
My own program works as well \o/
<Kooda>
I’m so happy ^_^
<awygle>
Excellent :-D congratulations
<Kooda>
I feel silly, I didn’t find out about the -f and -m options earlier. x)
sklv has quit [Quit: quit]
captain_morgan has quit [Remote host closed the connection]
captain_morgan has joined #yosys
digshadow has quit [Quit: Leaving.]
digshadow1 has joined #yosys
TFKyle has quit [Quit: :q!]
_whitelogger has joined #yosys
digshadow1 has quit [Quit: Leaving.]
digshadow has joined #yosys
m_t has joined #yosys
gnufan has joined #yosys
_whitelogger has joined #yosys
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 256 seconds]
sklv has joined #yosys
danieljabailey has quit [Ping timeout: 272 seconds]
danieljabailey has joined #yosys
danieljabailey has quit [Ping timeout: 264 seconds]
danieljabailey has joined #yosys
danieljabailey has quit [Ping timeout: 252 seconds]