ZipCPU|Laptop has quit [Ping timeout: 260 seconds]
<ZipCPU>
cr1901_modern: About 90 billable hours to get something that started to work.
<ZipCPU>
After that it's the never ending fuss to "find the last bug"--you know, the bit that takes forever.
<ZipCPU>
adityaP: 1. The FIFO size should be a parameter for maintenance sake. 2. Line 157 should be depending upon $past(wr) and $past(rd), not wr and rd. 3. Same with line 175. 4. You have no underflow checking.
<promach>
sorry to interupt, where could I find the "detailed" smtc file format description ?
<cr1901_modern>
ZipCPU: I'm sorry did you say "only" 90 hours?
<cr1901_modern>
To get through that autoconf hell and find the files you needed?
sklv has joined #yosys
<cr1901_modern>
to modify*
ZipCPU|Laptop has joined #yosys
dys has quit [Ping timeout: 258 seconds]
mbuf has joined #yosys
<awygle>
shapr: sometimes you get off work at 5, sometimes at 9 :( i dumped some stuff here https://gist.github.com/awygle/5dfb9a2fab25bbb1386af014cca8f112 it assumes you know about keyboards generally, if you want more info on that stuff /r/mechanicalkeyboards is pretty great
<awygle>
happy to talk keyboards anytime but probably not in #yosys :)
<awygle>
i'll put up pcb designs once i'm done with them, i'm using this project to learn kicad and it's slow going
proteusguy has quit [Remote host closed the connection]
indy has quit [Ping timeout: 240 seconds]
indy has joined #yosys
pmezydlo has joined #yosys
pmezydlo has quit [Ping timeout: 255 seconds]
nrossi has joined #yosys
FabM has quit [Ping timeout: 240 seconds]
LongHairedHacker has quit [Remote host closed the connection]
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 240 seconds]
AlexDaniel` has quit [Ping timeout: 255 seconds]
rmarko is now known as srk
waylon531 has joined #yosys
adj__2 has joined #yosys
uelen has quit [Quit: No Ping reply in 180 seconds.]
indy has quit [Ping timeout: 248 seconds]
adj__ has quit [Ping timeout: 248 seconds]
kuldeep has quit [Ping timeout: 240 seconds]
indy has joined #yosys
kuldeep has joined #yosys
leviathanch has joined #yosys
AlexDaniel` has joined #yosys
proteusguy has joined #yosys
sklv has quit [Ping timeout: 248 seconds]
<ZipCPU>
cr1901_moderrn: That's what I said, 90 hours. I had a patch available which added support for another CPU that I could work from to know where all the autoconf, etc, changes needed to be made.
<ZipCPU>
shapr: Remember, the difference between a horse and a camel is that the camel was designed by committee. The same applies to RISC-V.
<shapr>
:-(
<shapr>
I have high hopes for risc-v
<ZipCPU>
It's rather bloated, IMHO. They should've kept it simpler.
<ZipCPU>
You know .... simpler like the ZipCPU. Although, in all seriousness, the ZipCPU doesn't really answer the market need of the RISC-V--the two are in separate classes of processors.
<ZipCPU>
Now, Zip64 or the ZoomCPU on the other hand ... ;)
<shapr>
is there a zip64?
<ZipCPU>
Only in my notes. ;)
<shapr>
ah
<shapr>
one day maybe
<ZipCPU>
Well ... would you expect much interest for it?
<shapr>
yeah, I could
<shapr>
risc-v is gaining a bunch of traction
<shapr>
but design by committee often goes badly
<shapr>
or perhaps, rarely goes well
<ZipCPU>
See ... the one thing RISC-V has that the ZipCPU doesn't is $M+
<shapr>
what's that?
<ZipCPU>
The ZipCPU has been built on a shoe-string budget, although my hourly costs are probably > $0.5M by now.
<ZipCPU>
The RISC-V on the other hand has been designed for ASICs.
<ZipCPU>
You can't test an ASIC, though, without many $M's. ($M = millions of dollars, US)
mbuf has joined #yosys
proteusguy has quit [Ping timeout: 252 seconds]
FabM has joined #yosys
<shapr>
so if I wanted to have an equivalent to the teensy 3.1/3.2 chip in the ergodox, I'd guess I'd need some ram in addition to an ice40?
<ZipCPU>
I'd suggest both some SRAM and some flash
<ZipCPU>
Don't forget a clock and an LED or two.
<shapr>
the teensy 3.{1,2} has 64k ram and 256k flash, but the ergodox uses the same chip, not sure about ram/flash
<ZipCPU>
Not to mention a means of sending SPI commands to the FPGA to initially load it up, and some other means of talking with it as well.
<shapr>
ah, I plan on adding way too many LEDs
<ZipCPU>
Remember ... the flash is for more than just program instructions and data, but also for the FPGA's configuration.
<shapr>
ah right
proteusguy has joined #yosys
dys has quit [Ping timeout: 255 seconds]
proteusguy has quit [Ping timeout: 260 seconds]
sklv has quit [Ping timeout: 248 seconds]
sklv has joined #yosys
<adityaP>
ZipCPU: Thank you very much for the feedback on my FIFO code.
<ZipCPU>
;)
<ZipCPU>
Did it help?
<adityaP>
Yes Sir :)
<ZipCPU>
Good. Glad I helped then.
proteusguy has joined #yosys
<adityaP>
ZipCPU: but I have a question. For line 157 I am checking that he full output should remain 1, even after the FIFO is full and a write is attempted without read. The write and read is happening in current clock cycle. So what happens if I check in current clock cycle and not in past cycle?
<ZipCPU>
So ... if you want to make certain that full is '1' *after* a write and not a read, the you need to test for the write and not read in the last cycle.
<ZipCPU>
if (past_full_flag && $past(full) && $past(wr) && (!$past(rd))) assert(full)
sklv has quit [Ping timeout: 248 seconds]
sklv has joined #yosys
<adityaP>
ZipCPU: Thank you again.
mbuf has quit [Quit: Leaving]
<awygle>
shapr: probably don't need ram. Probably do need flash or other nonvolatile storage. Not necessarily a ton of it though
<awygle>
I would expect you'd be able to get away with the on chip BRAM for RAM
<awygle>
ZipCPU: AXI/WB correctness proof would be very interesting
<ZipCPU>
awygle: Making lots of progress ...
<awygle>
Hoping to dig into the SPI proof you uploaded tonight.
<awygle>
Just curious, have you shown Clifford or someone else who does this for a living your work so far?
<ZipCPU>
awygle: Actually, clifford and his team asked me to post "how to's", so that kind of requires that I understand how to do it in order to write about it.
<thoughtpolice>
ZipCPU: FWIW, if you haven't seen SymbiYosys yet -- it would probably make several of your 'formal' examples in your repository clearer.
<thoughtpolice>
It's mostly a convenient tool to wrap up yosys-smtbmc based flows
<ZipCPU>
thoughtpolice: Thanks. It's not a piece of anything I've looked at yet, though.
<thoughtpolice>
(Well, right now it is. In the future it'll do more exotic stuff, I think)
<ZipCPU>
I guess that's coming.
<thoughtpolice>
I've been using it for my own stuff and it's quite nice. (One nice clarity thing is it just keeps all of the necessary options to yosys and yosys-smtbmc in one place, vs a separate .ys script + Makefile rules to run yosys-smtbmc, which I like)
eduardo_ has quit [Ping timeout: 240 seconds]
eduardo_ has joined #yosys
clifford has quit [Ping timeout: 240 seconds]
clifford has joined #yosys
nrossi has quit [Quit: Connection closed for inactivity]
* cr1901_modern
grumbles upon finding the repo of symbiyosys... I didn't want to learn a new tool today...
<ZipCPU>
;) o/
<cr1901_modern>
And I might not... I might just mark it as an open issue for migen formal methods wrapper depending on how I'm feeling
<ZipCPU>
Are you working on migen?
<cr1901_modern>
Well, I've contributed a number of things to it at least; two platforms, and the icestorm backend
<cr1901_modern>
A few bug fixes...
<ZipCPU>
Ok.
<thoughtpolice>
I mean, if you already know how to use yosys-smtbmc, SymbiYosys is really not a lot to learn FWIW. It almost literally just runs yosys-smtbmc and yosys in an automated, convenient way on a set of verilog files, for all intents and purposes. (For example, it makes copies of all the design files, logs the solver output and traces, has a nice little .ini syntax to set yosys-smtbmc options, etc so you can reproduce it all later,
<thoughtpolice>
and all the stuff you'd do anyway.)
<thoughtpolice>
I literally use it just as a 'nicer' version of yosys-smtbmc
<thoughtpolice>
And it has some convenient features like being able to write 'inline' verilog in a .sby file.
leviathanch has quit [Remote host closed the connection]
<thoughtpolice>
(And if it's meaningful, SymbiYosys is what drives the model checks inside riscv-formal, although its usage is a bit more roundabout in the riscv-formal repository, because a Python script generates the SymbiYosys .sby files automatically from a set of existing checks
<ZipCPU>
Hey, I've almost got the first 12-clocks worth of WB/AXI bridge formally proven ... it's a start at least.
<ZipCPU>
BMC Works!
* ZipCPU
thinks z3 is slow.
<thoughtpolice>
:) I'll have to write a Wishbone interface for this side project at the moment eventually, so I'd be interested to see how it shakes out!
stoopkid has quit [Quit: Connection closed for inactivity]
dys has joined #yosys
<ZipCPU>
Ooo ... so close. Failed on the last clock of the induction step.
<cr1901_modern>
Any failure will be on the last clock of the induction step :P
<ZipCPU>
You mean like the item you are looking for will always be found in the last place you look?
<cr1901_modern>
Not quite :D. More referring to "counterexamples where no matter how long I make the induction length, the solver just holds all outputs constant until the nth state and then makes the design fail"
<thoughtpolice>
ZipCPU: Another feature SymbiYosys has is it can run multiple solvers in parallel if you want to see if any of them are faster ;) For some other work I did boolector was very fast in some cases, but unfortunately it's non-commercial.
<thoughtpolice>
(Non FPGA related, but it did involve ABC/hardware tools, in fact)