clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
lutsabound has joined #yosys
<awygle> nextpnr doesn't have any notion of a "target" or of "good enough", does it? it looks like it just goes until it can't go no mo
<awygle> re in the current placer but idk if that's a global expression of intent
kc5tja has joined #yosys
<ZipCPU> Correct.
<ZipCPU> At least .... that's my understanding of it.
<kc5tja> ZipCPU: Question for you -- I decided to "start over" but working on ROMA core first this time, trying to apply what I know. See http://chiselapp.com/user/kc5tja/repository/kestrel-3/artifact/c319f1224bbf23a6. It passes bmc, but fails prove. On my end at least, it starts out in a demonstrably invalid state, but unsure how to tell prove prover to rope it in a bit on its flights of fancy.
<ZipCPU> Welcome back!
<ZipCPU> I didn't think I was going to "see" you this evening.
<ZipCPU> So, "prove"ing things is ... more difficult that straight BMC, for exactly the reason you just uncovered.
<ZipCPU> The way to solve the problem is ...
<ZipCPU> to set up additional assertions. These additional assertions must be sufficient to keep your design out of all invalid states.
<ZipCPU> What happens during induction is that your assertions will be treated as though they were *assumptions* for the first N clocks.
<ZipCPU> That's why you can use them to keep your design from getting into an invalid state.
<ZipCPU> Even better, you can tell whether the problem is your assertions or your code by where in the trace the problem appears.
<ZipCPU> If the problem appears on the last timestep, or perhaps the penultimate timestep, then the problem is your code.
<ZipCPU> If it appears anywhere else on the left side of the trace, then the problem is a lack of assertions.
<kc5tja> I'll try adding assertions and see what happens then.
<ZipCPU> So, for example, you might wish to assert(bits_so_far <= 97)
<kc5tja> Yeah, in cycle 1, bits_so_far = 7'h7F, which resets to 0, which causes a fetch from flash, and thus, drives the D-channel before the A-channel gets a read request, and *that* in turn violates an assertion
<ZipCPU> You might also wish to assert((getting_data == (bits_so_far <= 96)&&(bits_so_far >= 33)));
<ZipCPU> You'll need some form of assertion for CS and MOSI as well.
<ZipCPU> But this is also one of those cases where cover() helps you to visualize what's going on vs what should be going on.
<ZipCPU> If you'd like to read more about the problems associated with induction, you might find this article valuable: http://zipcpu.com/blog/2018/03/10/induction-exercise.html
<kc5tja> I'll focus on SPI interface separately, if it's even needed.
<kc5tja> The cover statement I have now seems like black magic -- it yielded (noise on some signals notwithstanding) exactly the protocol as I envisioned it from reading the TileLink specs. Haha. :)
<ZipCPU> Easier than Verilator, no?
Eli2 has quit [Remote host closed the connection]
<kc5tja> ZipCPU: So far, no. I find using Verilator and unit tests much easier. However, it's a trade-off.
<kc5tja> With Verilator, I only concern myself with the external interface of the core under test. With formal, I have to concern myself with the deep internals as well.
<ZipCPU> Especially with "mode prove", not so much with cover.
<kc5tja> I should qualify my statement -- given a pre-existing core. I haven't tested starting a core from scratch with formal yet.
<ZipCPU> No, this is good. Starting with a pre-existing core is a perfect place to start.
<ZipCPU> It's where/how I did, and I'm glad I chose to do so.
Eli2 has joined #yosys
<kc5tja> The problem with maintaining an existing design, even one as simple as ROMA, is that I'm quickly losing focus. As I accumulate fixes, they compound like a ball of bandaids. Eventually nothing sticks, fixes interfere with each other, etc.
<kc5tja> There are too many moving parts.
kuldeep has quit [Ping timeout: 240 seconds]
kuldeep has joined #yosys
lutsabound has quit [Quit: Connection closed for inactivity]
rohitksingh_work has joined #yosys
_whitelogger has joined #yosys
azonenberg_work has quit [Ping timeout: 240 seconds]
azonenberg_work has joined #yosys
<kc5tja> ZipCPU: OK, cool, I *think* I've formally verified the ROMA core's TileLink slave ports. See http://chiselapp.com/user/kc5tja/repository/kestrel-3/info/b014c7b07f6f536a and view the diffs. Would love your thoughts on my progress here. But it passes base case and induction for 200 steps.
kc5tja has quit [Ping timeout: 252 seconds]
kc5tja has joined #yosys
rohitksingh_work has quit [Ping timeout: 240 seconds]
rohitksingh_work has joined #yosys
kc5tja has quit [Quit: leaving]
promach has joined #yosys
X-Scale has quit [Ping timeout: 252 seconds]
pie_ has quit [Ping timeout: 240 seconds]
fsasm has joined #yosys
m4ssi has joined #yosys
m4ssi has quit [Ping timeout: 272 seconds]
m4ssi has joined #yosys
gundy has joined #yosys
kraiskil has joined #yosys
gundy has quit [Ping timeout: 252 seconds]
pie_ has joined #yosys
maartenBE has quit [Ping timeout: 264 seconds]
rohitksingh_work has quit [Read error: Connection reset by peer]
mjoldfield has quit []
kraiskil has quit [Quit: Leaving]
flaviusb has quit [Ping timeout: 244 seconds]
flaviusb has joined #yosys
maartenBE has joined #yosys
AlexDaniel has quit [Ping timeout: 260 seconds]
rohitksingh has joined #yosys
rohitksingh has quit [Remote host closed the connection]
seldridge has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Client Quit]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
zino has quit [Quit: Leaving]
rohitksingh has joined #yosys
NB0X-Matt-CA has quit [Excess Flood]
NB0X-Matt-CA has joined #yosys
rohitksingh has quit [Quit: Leaving.]
fsasm has quit [Ping timeout: 244 seconds]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
zino has joined #yosys
seldridge has quit [Ping timeout: 260 seconds]
seldridge has joined #yosys
rohitksingh has joined #yosys
pie_ has quit [Ping timeout: 244 seconds]
kc5tja has joined #yosys
kuldeep has quit [Ping timeout: 245 seconds]
kuldeep has joined #yosys
seldridge has quit [Ping timeout: 246 seconds]
pie_ has joined #yosys
jer has joined #yosys
<awygle> jer: greetings :)
<jer> awygle, howdy =]
seldridge has joined #yosys
<jer> awygle, all sorted thanks for your help
<awygle> glad to hear it
<ZipCPU> kc5tja: Yosys supports two separate modes for dealing with clocks--a synchronous mode and an asynchronous mode. Processing wise, the asynchronous mode takes nearly (not quite) twice the work to process.
<ZipCPU> All that's to say that you don't need the: always #1 i_clk <= ~i_clk; statement. If you are doing a synchronous proof, this may have unintended side effects that you do not want. If this is an asynchronous proof, there are better ways to do that. If this isn't part of the proof at all, then it shouldn't be in the section on formal properties.
<awygle> ZipCPU: do you have a post on verifying UARTs? my google foo is returning a sort of diffuse mist spread throughout your blog
<ZipCPU> awygle: Not really. I have a post on UART's, but ... there's no code involved and no formal methods involved.
<ZipCPU> kc5tja: Love the constant, 64'hDEAD_BEEF_FEED_FACE :D
<ZipCPU> kc5tja: I also like your approach to the design via independent states.
<ZipCPU> awygle: Turns out, when using full SVA sequences, it becomes *REALLY* easy to formally verify a serial port.
<awygle> ZipCPU: :) but also :(
<ZipCPU> Not quite so fast.
<ZipCPU> Not sure how simpler things could get
<awygle> i was juuuust looking at that repo
<ZipCPU> That, of course is the transmitter where things are easy. (Receiver is *MUCH* harder)
<awygle> yupyup
<ZipCPU> awygle: That's my serial port repo ;)
<awygle> but i don't have verific
<awygle> and vanilla-yosys doesn't have sequences, right?
<ZipCPU> Correct.
<ZipCPU> However ....
<ZipCPU> Once you express something that way, it gets fairly easy to re-express the same logic in a state machine.
<awygle> i'm sure they desugar to something vanilla-compatible, maybe i can `define a macro or something
<ZipCPU> It's sort of like the difference between C++ and C. Anything you can do in C you can do in C++. Likewise, anything you can do in C++ you can do with a couple more words in C.
* awygle opens his copy of IEEE-1800, starts reading about sequences
<ZipCPU> You might find it easier for me to explain these to you ;)
<awygle> i mean sure, if you're willing ;)
<ZipCPU> The code consists of two sequences and one property.
<ZipCPU> The first sequence, BAUD_INTERVAL, describes all the parts of a baud interval
<ZipCPU> The key piece is the "##1" part. If you break up this sequence, it reads (state_one) ##1 (state_two)
<ZipCPU> ##1 just means a clock tick passes.
<ZipCPU> Hence, (state_one) first, then (state_two) on the second clock.
<ZipCPU> That's most of it, minus the [*(CKS-1)] part.
<ZipCPU> (A) [*COUNT] references a state (A) that must be true for COUNT cycles.
<ZipCPU> Hence, the baud cycle consists of a state which repeats for (CKS-1) cycles, and then a second state that takes place for one cycle.
<ZipCPU> Note the CKS, DAT, SR, and ST. These are "parameters" to the BAUD_INTERVAL sequence. In this code, they are the number of clocks to stay in the state, the data sent during this state, the shift register state, and the controller state.
<ZipCPU> The big thing to be concerned with when using these is that they are macro parameters. If the underlying value changes over the course of the sequence, these parameters will reference the new/updated values at that time in the sequence.
<ZipCPU> Any questions before I move to the "SEND" sequence?
<awygle> ah. so this basically _is_ a `define lol
<ZipCPU> kc5tja: Just be aware of your initial states: if you place synthesizable logic in the ifdef FORMAL method, it could render the proof invalid. I'd recommend getting rid of the initial section entirely, rather than putting it in an ifdef call.
<ZipCPU> awygle: Yes.
<awygle> that makes sense, please continue
<ZipCPU> Well, the parameters are ... the ##1's and the [*CKS-1] are not. Those are new/special.
<ZipCPU> Okay, let's talk about the SEND sequence. This is given two parameters: the number of clocks (CKS) per baud interval, and a byte of DATA
<ZipCPU> Sending this byte consists of 10 states: The start bit, 8 data bits, and the stop bit. That's what you see here. Each of these states is described by the BAUD_INTERVAL we just described above, and they are separated by a singular clock.
<ZipCPU> Hence, you have CKS clocks of the start bit (the first BAUD_INTERVAL), followed on the next clock by another CKS clocks of the first data bit, etc.
<awygle> yeah, this is dope. i totally get how this makes things way easier.
<awygle> i wonder how hard it would actually be to desugar this in yosys proper....
<ZipCPU> You would've searched the standard forever to get this.
<ZipCPU> awygle: That's why I was explaining it to you. I really don't think it'd be all that hard.
<awygle> the logic is relatively straightforward
<ZipCPU> It's just a basic state machine.
<kc5tja> awygle: My next task will be to work on the transmit side of a UART for my homebrew computer, which I plan on developing with formal verification as part of my TDD process.
<ZipCPU> kc5tja: You are here! I was expecting you wouldn't notice any of my comments till this evening!
<awygle> kc5tja: excellent! i did a bunch of work on a formally verified UART something like six months ago which i am now returning to
<kc5tja> ZipCPU: I've experimented with having it or not, and it makes no difference to the proof in practice; it's legacy from earlier experimentation, but it really helps me when deep-diving into a pile of gtkwave traces.
<ZipCPU> kc5tja: ;)
<kc5tja> ZipCPU: Benefits of working from home.
<ZipCPU> You are working from home today? (me too)
* ZipCPU enjoys the fact that he can listen to Rush and no one gets offended
* awygle is jealous
<awygle> ZipCPU: 2112?
<ZipCPU> 2112?
<awygle> the rush album
<ZipCPU> iHeart Radio, Rush Limbaugh
<awygle> (and song i suppose)
<awygle> ahhhh different rush lol
<ZipCPU> awygle: There's something else to be said about designing the states of your formal state machine
<ZipCPU> You want to make them so strict that the formal methods will never get stuck in the wrong state.
<ZipCPU> The formal method variables need to be *LOCKED* to your internal variables--leave no room for misunderstanding, or you might not pass induction.
<kc5tja> The only kind of Rush I listen to is from Canada.
<awygle> same, same
<awygle> incomparable drums
<ZipCPU> This is why my own proof includes references to the internal state of the serial port, and the shift register
<awygle> ZipCPU: yup :) understood
<ZipCPU> I'll admit ... I tried doing this with the general UART transmitter. Even the Verific enabled proof fails for that one though.
<ZipCPU> Worse, yosys won't even build it. :(
m4ssi has quit [Remote host closed the connection]
<kc5tja> ZipCPU: The state machine for the ROMA core came about because I was on the verge of giving up and was about to redesign from scratch. I got part-way through developing the new code when it all of a sudden synchronized with what's already there. I'm sure the ROMA has a lot of cruft that could be reorganized and/or removed all-together. But it works, and timing analysis says it's good for 143MHz, so I'm
<kc5tja> calling it.
<ZipCPU> :D
* ZipCPU would probably do the same
* ZipCPU doesn't like code church, though, so he might have called it earlier.
<kc5tja> Code Church?
<ZipCPU> Oop!!! Misspelling. I meant code churn
<ZipCPU> and I can't even blame it on a spell check. :(
<kc5tja> ZipCPU: regarding initial block -- without those two initial settings, it will fail formal verification. I *have* to have reset and i_a_valid set low when the verification starts.
<ZipCPU> kc5tja: No, you can get it to pass formal, you'd just need to refactor the properties a bit.
<kc5tja> It's like with Wishbone, where CYC must be low during reset.
<ZipCPU> Such a refactor would start with something like: initial assume(i_reset); You could also do always @(*) if (!past_valid) assume(i_reset);
<ZipCPU> That'll guarantee you start with a reset. (I think you have something like this already)
<ZipCPU> That's important.
<ZipCPU> Next, to prove that you never get into an invalid state, you would add either past_valid to your test, or !i_reset to the test.
<ZipCPU> At that point, you should be able to succeed without the initial values.
<kc5tja> It'll still fail induction. I've tried. Unless I assume i_a_valid to be low during reset, it *will* start with it in a high condition, and that's irreparable; I can't do anything to get out of that.
<kc5tja> note: *during* not *after* reset.
<ZipCPU> No, that can be fixed. I thought your code handled that nicely by ignoring i_a_valid during a reset?
<kc5tja> Oh wait, I'm spacing it. I did in fact remove i_a_valid from the initial. I do still need to initial my first state though.
<kc5tja> Yeah, if I remove the initial block all-together, it fails basecase *immediately*.
<kc5tja> By which I mean, cycle 0. :)
<ZipCPU> For what assertion?
<kc5tja> line 76
<kc5tja> of properties.vf
rohitksingh has quit [Quit: Leaving.]
azonenberg_work has quit [Ping timeout: 252 seconds]
<ZipCPU> You mean, always @(*) assert(state_waiting_for_flash == (bits_so_far <= 96)); ?
<kc5tja> Yes
<ZipCPU> That's what I was discussing above. You could correct this by adding a condition to the assert, such as ...
<ZipCPU> always @(*) if (past_reset) assert(state_waiting_for_flash == (bits_so_far <= 96));
<kc5tja> OK, fixed. Thanks for that!
<ZipCPU> ;)
nats` has joined #yosys
<cr1901_modern> ZipCPU: Have you used yosys' equivalence checking?
<ZipCPU> Not really. I think you and I tried to dig into it once before, tho.
lutsabound has joined #yosys
<cr1901_modern> We did, though my current use case is different
<cr1901_modern> I want to prove a 16-bit full subtractor that I'm modeling using behavioral Verilog is equivalent to the "naive" version of chaninging 1-bit full subtractors together
<ZipCPU> How many clocks does the addr take?
<ZipCPU> s/addr/subtractor/
<cr1901_modern> one, it's full combinatorial
<ZipCPU> As in ... why not just create a top level module that assumes the two have the same inputs, and asserts that they have the same outputs?
<cr1901_modern> Oh... yea I could do that
<nats`> ZipCPU you have some sort of template to chain yosis with vivado ?
<ZipCPU> That way you don't have to do anything to prove that the internal structures are equivalent.
<awygle> cr1901_modern: i've used it once as well, if you decide you want to do that
<cr1901_modern> Basically, I do (x + 65536) - y, instead of x - y, and check the 16th (0 index) bit is set. If it's not set a borrow occurred. If it is set, there was no borrow
<awygle> ZipCPU's way will totally work though
<ZipCPU> nats`: I'm pretty sure the answer is "No", but ... feel free to explain some more and maybe I may offer something else.
<cr1901_modern> Idk if that's common or not
<nats`> ZipCPU I mean a "standard" way to synthetize with yosys and then finish the work with vivado
<ZipCPU> Ahh ... Yes, there is a way to do that. I haven't tested it though.
* ZipCPU rummages for examples
<ZipCPU> Yosys hs a synth_xilinx command.
<ZipCPU> s/hs/has/
<ZipCPU> Vivado should accept an EDIF file, so you can output an edif file and then go into Vivado.
<nats`> oky will lokk in that direction :)
<jer> ZipCPU, vivado should do a lot of things it doesn't ;)
<ZipCPU> Lol!
<jer> it also does some things it shouldn't
<jer> =D
<ZipCPU> jer: In all fairness, your criticisms could validly be applied to just about every piece of software out there. This includes <GASP!> yosys. <sniff>
<mattvenn> compiling gcc for riscv32imc - exciting!
<jer> ZipCPU, indeed, apologies to anyones project i admire caught in the crossfire =]
<nats`> and TBH vivado is a big leap forward compared to ise :D
<fouric> wait, really? both of the engineers here who use xilinx parts are really unhappy about the change
<fouric> and it seems like the internet has a lot of complaints about xilinx killing ise support
<nats`> because they don't like change ?
<fouric> and also my personal experience with vivado is that it's sort of a garbage fire
<fouric> is ise worse?
<nats`> the most heard complaint is more xilinx dropping support of serie 7
<nats`> serie 6
<nats`> in my opinion vivado is way nicer to work with
<sorear> i'm not super in the loop, what happened with ise? is it no longer possible to download?
<nats`> it is but it's not supported anymore
<nats`> and you need crappy dodgy patch to make it works on newer windows
<sorear> you mean like, they no longer honor support contracts?
<fouric> (tbh vivado _also_ breaks on newer windows)
FPGA_N00b has joined #yosys
<FPGA_N00b> hello all, I have a question about ICE40 8K IO bits :
<FPGA_N00b> example code: # For the iCE40HX-8K Breakout Board set_io D1 B5 set_io D2 B4
<FPGA_N00b> for the "B5" and "B4" values, is there a way to map the code-based input/output bit to that on the schematic banks from the Lattice manufacturer?
<FPGA_N00b> for example, on the schematic, BANK1 P101_04 would be "P16"
<FPGA_N00b> could I just do : set_io D1 P16 and have it redirect my LED output to the separate pin?
X-Scale has joined #yosys
<FPGA_N00b> apparently LED0 is B5
<FPGA_N00b> and LED7 is C3
<FPGA_N00b> so is there any inherent problem with connecting an internal wire from C3 to somewhere else (such as P16)? Wouldn't that dual-illuminate an LED plugged into Bank1 Topright corner?
emeb_mac has joined #yosys
<awygle> I'm confused. You want to map your top level net names to io pads instead of to pins/balls
<awygle> ?
<FPGA_N00b> no, not map like that
<FPGA_N00b> in the .pcf file,
<FPGA_N00b> can I "dual define" such as :
<FPGA_N00b> set_io D1 C3
<FPGA_N00b> set_io D1 P16
<FPGA_N00b> or does the set_io function require a distinct individual entry per 1st variable
<awygle> Oh I see
<awygle> Good question
<awygle> You can certainly do it in the verilog, I'm not sure if it'll work in the pcf
<awygle> Try it and see?
<FPGA_N00b> I'm completely green at this so sorry if it's confusing
<FPGA_N00b> ok I'll try it out tonight
<FPGA_N00b> but I'm just scared I'm going to break something
<awygle> If it doesn't work you'll just get an error from the tools
<FPGA_N00b> ok
<awygle> Id probably just do "assign D0_again = D0" in verilog and map D0_again to P16 personally but now I'm curious lol
<FPGA_N00b> 2nd question: in the .txt file, where it goes into all of the tile information (such as RAMT,RAMB, IO,LOGIC), is the header and footer information necessary? Could I upload a completely blank tilesheet onto the FPGA without defining all of those flags at the end of the file?
<FPGA_N00b> I'm pretty sure it was IcePack or something similar which put that footer information there, but I'm wondering how raw I can get a .txtfile onto the FPGA
<FPGA_N00b> the youtube linked from 2011 https://www.youtube.com/watch?v=yUiNlmvVOq8&feature=youtu.be had the output devoid of header and footer information
<FPGA_N00b> (2015, not 2011)
<FPGA_N00b> will icepack run without that information?
<ZipCPU> Try it with blinky and see?
<ZipCPU> I've done a lot of ice40 work and never needed to adjust the header/footer information
<FPGA_N00b> ok wonderful
<FPGA_N00b> thanks a lot for your help
<FPGA_N00b> man y'all are quite helpful
<FPGA_N00b> I'll submit my code and references to the iceStorm page once it's tested
<FPGA_N00b> if anyone here has read Dr. Adrian Thompson (University of Sussex) FPGA Hardware Evolution book, that's what I'm trying to emulate
<ZipCPU> Sorry, not me. But if you are a noob, then let me recommend zipcpu.com to you.
<FPGA_N00b> yeah I've got that URL in a separate tab now.
<FPGA_N00b> RISC chipset. Nice
<FPGA_N00b> not "chipset" but likely instructionset
<ZipCPU> What, you mean the ZipCPU?
<FPGA_N00b> yeah
<ZipCPU> The ZipCPU instruction set may not look like any RISC instruction set you are familiar with. I didn't follow a pattern from that standpoint.
<FPGA_N00b> ahh
<ZipCPU> It's also more "reduced" than most RISC ISA's out there.
<ZipCPU> However, the immediate space associated with instructions tends to be larger than many RISC ISA's. Whether or not that's a good/better thing is up for debate.
<FPGA_N00b> so it might take some time before I can fully implement my Gamecube Gekko on FPGA
<sorear> if you design an out-of-order PPC32 core with similar IPC to Gekko, you will be very lucky to reach 100 MHz
<sorear> this isn't like the SNES where you can easily make something faster than the real thing
<FPGA_N00b> the FPGA gaming subreddit had a guy get Playstation and SNES going
<FPGA_N00b> 100Mhz can probably run tetris or anything from 1994
<ZipCPU> Yes, it will take some time.
<ZipCPU> That's neither a good nor bad thing, just a statement of reality.
<FPGA_N00b> FPGA SNES was on DE0-CV
<ZipCPU> FPGA_N00b: I'm running my ZipCPU on the iCE40 HX8k at 50MHz. You might struggle to go much faster. Not that it's not doable, it will just take some extra diligence to do.
AlexDaniel has joined #yosys
<awygle> you may wish to investigate the ECP5 series for your final project
<awygle> as they have a (somewhat incomplete) open source toolchain and are much bigger/faster
<awygle> or at least, can be those things
<FPGA_N00b> 50Mhz is no slouch. My 286 and 386 could run all kinds of stuff
<FPGA_N00b> I had a 486-66 too
<FPGA_N00b> but those were intel, not RISC/PowerPC
<ZipCPU> You won't fit an x86 in an HX8k board.
<FPGA_N00b> I don't doubt it
<kc5tja> Just speculation, but I think you could maybe fit an 8086 in an HX8K; the 8086 didn't have *that* many gates or transistors, as I recall. You won't be able to fit much else, though. Definitely not an 80286 or later, as instruction decode (taking protected mode into consideration) would itself be a very tight fit.
<ZipCPU> kc5tja: I was a bit too broad in my statement, wasn't I?
<awygle> well there's Next186
<awygle> could always find that out
<kc5tja> I don't know -- I'm just guessing. But the 8086 was pretty small compared to the 80286.
<kc5tja> Something like 37K transistors, IIRC?
<kc5tja> To the Interwebs!
<ZipCPU> Then again, FPGA_N00b could take kc5tja's road to building a 64-bit RISC-V on an ice40
<ZipCPU> It's novel, but it should work well.
<ZipCPU> I'm still hoping/waiting to see the result.
<ZipCPU> ;)
<cr1901_modern> 22k transistors if memory serves
<cr1901_modern> 286 was 144k?
<awygle> looks like the Next186 uses 46% of an ECP5-12k
<awygle> it does use 71% of the EBR in the case i'm looking at, which isn't ice40-compatible, but i bet a lot of that is caches
<awygle> so you could probably get a minimal build of Next186 on an HX8K
<sorear> a 686 would be much more interesting, does debian still support that?
<cr1901_modern> NetBSD still officially supports 486
<FPGA_N00b> that's awesome
<awygle> could probably fit that on an ECP5-85k
<awygle> or just buy the cyclone but that's not as cool
<cr1901_modern> 486 has over 1 million transistors
<cr1901_modern> mostly due to the FPU
<kc5tja> ZipCPU: I've already synthesized (but not tested in hardware) my KCP53000 core, and surprisingly, it fit with about 1100 LUTs left. I will not fit on a 1K though.
<awygle> oh it's hella QSys stuff, not easy to port
<sorear> you have a lot of room to trade off speed vs size with FPUs and similar
<awygle> does gcc still support -march=i486? lol
<kc5tja> Maybe some day, we can find the source code to the 68070 (aka Apollo Accelerator for the Amiga; formerly known as the 68080 during development, IIRC). That ... definitely won't fit on an HX8K. ;)
<sorear> the source is _lost_? i was under the impression it was just proprietary
<kc5tja> sorear: Yes, it's proprietary, and thus under lock and key. We're not going to see it ever, I don't think.
<FPGA_N00b> Amigas had some pretty good sound chips
<FPGA_N00b> like the SID
<kc5tja> The SID was on the Commodore 64. The Amiga only ever had the Paula chip.
<FPGA_N00b> oh yeah
<FPGA_N00b> thanks; I played on my cousin's c64 that's what I was thinking about
<FPGA_N00b> the amiga was always there in the UK computer shops
<FPGA_N00b> them and Tandy I remember
* kc5tja still has his Amiga 500; but no idea if it still boots or not. Last time I tried booting it, I had to drop the unit from 6 inches above the table to reseat all the chips at once. I should look at the RAM expansion too, and hopefully the battery hasn't leaked out all over the place.
<kc5tja> I'm sure it needs to be re-capped as well. :/
<zino> A500s does not suffer that much from bad caps yet. It's the A600 and A1200 that are pretty much all bad.
indy has quit [Quit: ZNC - http://znc.sourceforge.net]
indy has joined #yosys
lutsabound has quit [Quit: Connection closed for inactivity]
AlexDaniel has quit [Ping timeout: 245 seconds]
<jer> if i have multiple modules in multiple files, do i have to read_verilog in my .sby file for each of them in order to get my proof to run? i already have all 3 in question (my top + 2 other pieces) in files
<jer> the proof is at the top level
<awygle> you do have to read each file containing modules
<awygle> if you have multiple modules in one file, read_verilog should do the right thing
<jer> when i try and read the top level only, it complains about the other modules not being found
<jer> when i read all 3, it works, my base case passes fine
Eli2 has quit [Quit: Ex-Chat]
FPGA_N00b has quit [Ping timeout: 252 seconds]
dxld has quit [Quit: Bye]
dxld has joined #yosys
Eli2 has joined #yosys
cr1901_modern has quit [Ping timeout: 268 seconds]
cr1901_modern has joined #yosys
azonenberg_work has joined #yosys
seldridge has quit [Ping timeout: 250 seconds]
emeb has joined #yosys
seldridge has joined #yosys