| *** tpb has joined #yosys | 00:00 | |
| *** svenn has quit IRC | 00:00 | |
| *** svenn has joined #yosys | 00:01 | |
| *** weatherhead has joined #yosys | 00:29 | |
| ZipCPU | ZirconiumX: What's the struggle? Anything I can help explain? | 00:30 |
|---|---|---|
| *** weatherhead has quit IRC | 00:39 | |
| *** weatherhead has joined #yosys | 00:41 | |
| *** gsi__ has joined #yosys | 00:58 | |
| *** ktemkin has quit IRC | 01:00 | |
| *** ktemkin has joined #yosys | 01:00 | |
| *** tannewt has quit IRC | 01:00 | |
| *** ZipCPU has quit IRC | 01:00 | |
| *** gsi_ has quit IRC | 01:01 | |
| *** ZipCPU has joined #yosys | 01:01 | |
| *** tannewt has joined #yosys | 01:02 | |
| *** citypw has joined #yosys | 02:39 | |
| *** citypw has quit IRC | 02:45 | |
| *** PyroPeter has quit IRC | 02:49 | |
| *** PyroPeter has joined #yosys | 03:02 | |
| *** azonenberg_mobil has joined #yosys | 03:24 | |
| *** proteusguy has quit IRC | 04:32 | |
| ZirconiumX | ZipCPU: I find it difficult to think of useful properties to prove about something. I can come up with some assertions to test preconditions (for example, two pipelines writing to the same register breaks the LVT, so it must be prohibited) | 04:32 |
| *** lutsabound has quit IRC | 04:32 | |
| ZirconiumX | But I have no clue about postconditions; more specifically, *useful* postconditions. I feel like trying to prove what the code explicitly states is a tautology, such as proving you can read from a register. | 04:36 |
| ZirconiumX | For useful things like the instruction decoder, trying to prove that only legal instructions are accepted requires something like a giant table of legal instructions for the test bench to work on. | 04:40 |
| sorear | ZirconiumX: have you read through riscv-formal? | 04:43 |
| ZirconiumX | I have, yes | 04:43 |
| *** proteusguy has joined #yosys | 04:47 | |
| sorear | I thnk the same methodology could be applied to sh? | 04:48 |
| ZirconiumX | Sure, but first I need to grok the methodology | 04:49 |
| ZirconiumX | I was given my rough task for the summer: I need to run a 256 byte Dreamcast demo. | 04:49 |
| ZirconiumX | It's only 34 instructions | 04:50 |
| sorear | 1. local correctness: for each retired instruction, does it read the correct registers, does it write the right register to the right place, does it make the correct memory access? | 04:50 |
| sorear | 2. consistency: given a sequence of instructions, if instruction A writes register or memory location X, and instruction B reads it, and there are no intervening writes, B reads the value A wrote | 04:51 |
| ZirconiumX | But some of those instructions include fun things like IEEE 754 division .-. | 04:51 |
| sorear | 3. forward progress: in any N cycle period, at least one instruction is retired | 04:51 |
| ZirconiumX | Okay, that makes sense | 04:53 |
| sorear | food for thought: https://github.com/SymbioticEDA/riscv-formal/blob/master/docs/rvfi.md#alternative-arithmetic-operations | 04:55 |
| tpb | Title: riscv-formal/rvfi.md at master · SymbioticEDA/riscv-formal · GitHub (at github.com) | 04:55 |
| sorear | verifying a FPU is a bit different from verifying a pipeline | 04:57 |
| sorear | pipelines are extremely complicated but have relatively few actual state bits and sparse coupling between them, so model checkers work well | 04:58 |
| sorear | (modern) FPUs are close to combinatorial, so pipeline verification is simple, but "was the correct operation computed" is far beyond what model checkers can work with | 04:58 |
| ZirconiumX | It doesn't help that 754 arithmetic is perhaps a little vague; you don't have to be accurate, just accurate enough. | 05:00 |
| sorear | you said "division" though, division is required to be correctly rounded | 05:02 |
| sorear | there's some ambiguity around subnormals handling (unclear if the spec actually allows multiple results or people just think it does because it's not clear enough) but for finite results there's only one allowed | 05:03 |
| sorear | even if it weren't, you have a goal of giving the same results as sh4 and sh4 hopefully documents what it does | 05:04 |
| sorear | "accurate enough" is for functions like sin() | 05:05 |
| * sorear stares at FPSCR.PR | 05:08 | |
| *** rohitksingh_work has joined #yosys | 05:14 | |
| *** rohitksingh has joined #yosys | 05:49 | |
| *** emeb_mac has quit IRC | 06:14 | |
| *** tecepe_ has joined #yosys | 06:16 | |
| *** edmoore_ has joined #yosys | 06:16 | |
| *** elms_ has joined #yosys | 06:16 | |
| *** thoughtpolice_ has joined #yosys | 06:17 | |
| *** pepijndevos_ has joined #yosys | 06:23 | |
| *** sorear has quit IRC | 06:24 | |
| *** flaviusb has quit IRC | 06:24 | |
| *** edmoore has quit IRC | 06:24 | |
| *** elms has quit IRC | 06:24 | |
| *** tecepe has quit IRC | 06:24 | |
| *** thoughtpolice has quit IRC | 06:24 | |
| *** pepijndevos has quit IRC | 06:24 | |
| *** edmoore_ is now known as edmoore | 06:24 | |
| *** tecepe_ is now known as tecepe | 06:24 | |
| *** elms_ is now known as elms | 06:24 | |
| *** thoughtpolice_ is now known as thoughtpolice | 06:24 | |
| *** sorear has joined #yosys | 06:29 | |
| *** flaviusb has joined #yosys | 06:30 | |
| *** dys has quit IRC | 06:55 | |
| *** jakobwenzel has joined #yosys | 07:10 | |
| *** rohitksingh has quit IRC | 07:37 | |
| *** m4ssi has joined #yosys | 08:04 | |
| *** rohitksingh has joined #yosys | 08:20 | |
| *** azonenberg_mobil has quit IRC | 08:39 | |
| *** vup has quit IRC | 08:54 | |
| *** vup has joined #yosys | 08:54 | |
| *** rqou has quit IRC | 09:27 | |
| *** rohitksingh_work has quit IRC | 09:59 | |
| *** rohitksingh_work has joined #yosys | 10:01 | |
| *** rohitksingh has quit IRC | 10:04 | |
| *** rohitksingh has joined #yosys | 10:05 | |
| *** alexhw has joined #yosys | 10:17 | |
| *** rqou has joined #yosys | 10:23 | |
| *** rohitksingh_work has quit IRC | 10:44 | |
| *** rohitksingh_work has joined #yosys | 10:45 | |
| *** rohitksingh has quit IRC | 10:46 | |
| *** Kitlith has quit IRC | 10:49 | |
| *** Kitlith has joined #yosys | 10:53 | |
| *** nurelin_ has quit IRC | 10:55 | |
| *** nurelin_ has joined #yosys | 10:55 | |
| *** GoldRin has joined #yosys | 11:07 | |
| *** proteusguy has quit IRC | 11:57 | |
| *** GoldRin has quit IRC | 12:15 | |
| *** proteusguy has joined #yosys | 12:36 | |
| pepijndevos_ | ZirconiumX, looking at bit-serial architecture now... | 12:48 |
| pepijndevos_ | ZirconiumX, another question: did you look at part availability when chosing the AC variations and particular chips? | 12:48 |
| pepijndevos_ | Wow...that's a short wikipedia page right there. | 12:49 |
| pepijndevos_ | Sad story: Kicad includes a whole 74xx library, but no AC parts | 12:49 |
| ZirconiumX | pepijndevos_: I did look at part availability; AC is still manufactured by TI and ON Semi | 12:50 |
| ZirconiumX | And for KiCad, remember that 74 series parts are *mostly* pin compatible | 12:50 |
| ZirconiumX | Though they don't have the AC11 series | 12:50 |
| pepijndevos_ | Yea... I figured I could probably get away with any of the variations they might have. | 12:51 |
| ZirconiumX | And AC11 is pretty important | 12:51 |
| pepijndevos_ | AC11 is the 16 bit stuff? | 12:51 |
| ZirconiumX | No, that's AC16 | 12:51 |
| ZirconiumX | AC11 is an alternative layout that puts VCC and GND in the middle of the chip | 12:51 |
| pepijndevos_ | ... why is that important? | 12:52 |
| pepijndevos_ | Speed and ground bounce and stuff? | 12:52 |
| ZirconiumX | Ground bounce, yeah | 12:52 |
| ZirconiumX | Having VCC and GND in the corners of the chip means that for gates on the opposite sides of the pins have longer voltage path | 12:53 |
| ZirconiumX | Add that to the very fast switching time of AC logic, and you end up with something that can bounce while switching | 12:54 |
| pepijndevos_ | Right... I agree it makes sense... it's just not very convenient for generating KiCad netlists. | 12:55 |
| pepijndevos_ | I guess I'll have to hunt for or make library parts or switch to more impractical parts. | 12:55 |
| ZirconiumX | Making KiCad libraries is easy | 12:56 |
| ZirconiumX | Getting them merged is harder | 12:56 |
| ZirconiumX | :P | 12:56 |
| pepijndevos_ | I guess. Well, I'll just start playing with the parts that are there. Last time I tried to do anything in KiCad it was a nightmare. | 12:58 |
| * ZipCPU gets up, starts reading ZirconiumX's backlog | 12:59 | |
| pepijndevos_ | I found skidl, which can programmatically make netlists, saving me a lot of trouble. | 13:00 |
| ZirconiumX | Morning, ZipCPU | 13:00 |
| ZipCPU | Morning! | 13:02 |
| ZipCPU | I remember when I verified a pipelined CPU (my own), I was concerned that instructions would be dropped or duplicated as they went through the pipeline | 13:03 |
| ZipCPU | Since then, I've added another worry: that the pipeline doesn't get stuck | 13:03 |
| ZipCPU | The CPU pipeline logic was complex enough as it is/was so these were important criteria for me | 13:04 |
| ZipCPU | As for the reset, have you thought of: if ($past(i_reset)) assert(issue_instruction_request && request_address == RESET_ADDRESS); ? | 13:04 |
| ZirconiumX | I have not, no | 13:06 |
| ZipCPU | Here's another one: if ($past(i_reset)) assert(pipeline_stage_is_valid == 0); | 13:07 |
| ZipCPU | Or, ... if ($past(pipeline_stage_advances)) assert(pipeline_stage_data == $past(previous_pipeline_stage_data || pipeline_stage_valid == 0); | 13:08 |
| ZipCPU | Since the ZipCPU has multiple pipeline stages, I did that for each | 13:09 |
| pepijndevos_ | sigh, no 74xx16xxx parts either... | 13:09 |
| ZipCPU | Or, here's another: if ($past(pipeline_stage_valid)) assert($stable(pipeline_stage_data) || next_pipeline_stage_has_the_new_data); | 13:10 |
| ZirconiumX | Huh, that's interesting | 13:13 |
| ZirconiumX | sorear will be pleased to know that me and $employer have agreed on me having to implement only a subset of SH4 | 13:13 |
| ZirconiumX | Unfortunately this subset is still fairly complex | 13:14 |
| ZirconiumX | ZipCPU: I get the feeling your general philosophy is to build the pipeline and then prove it correct, rather than worry about that as you go | 13:14 |
| ZipCPU | Perhaps because I had the pipeline already built when I discovered formal | 13:15 |
| ZipCPU | Were I to do it again, I might start with something closer to riscv-formal | 13:15 |
| ZipCPU | That's a nice end-to-end approach, vs my own which was more internals based | 13:15 |
| sorear | Roughly what’s the subset? | 13:19 |
| *** rohitksingh_work has quit IRC | 13:19 | |
| ZirconiumX | sorear: Boolean logic operations, addition/subtraction, some immediate operations, an integer fused multiply-accumulate unit, plus a basic floating-point unit with addition, subtraction, multiply and divide | 13:23 |
| ZirconiumX | Plus sine/cosine approximation | 13:24 |
| ZirconiumX | https://github.com/emudev-org/fpgadc/blob/master/cmodel/main.cpp#L142-L884 <-- anything in this block which has an sh4impl | 13:24 |
| tpb | Title: fpgadc/main.cpp at master · emudev-org/fpgadc · GitHub (at github.com) | 13:24 |
| sorear | sh4 has sine/cosine? I only have a document for sh2a | 13:24 |
| ZirconiumX | sorear: it's an approximation, but yeah | 13:25 |
| ZirconiumX | https://hwdocs.webs.com/dreamcast | 13:25 |
| tpb | Title: Hardware Docs - Dreamcast (at hwdocs.webs.com) | 13:25 |
| * ZirconiumX whistles innocently | 13:25 | |
| sorear | what significant things does that *exclude*? the MMU? | 13:25 |
| ZirconiumX | MMU, the concept of instruction privilege, and quite a lot of the status registers | 13:26 |
| ZirconiumX | ZipCPU: When should you use a bounded model check and when should you use induction? | 13:35 |
| ZipCPU | A bounded model check can find assertion failures, and can often be done with basic "white-box" testing approaches | 13:36 |
| ZipCPU | Induction can prove that there are no assertion failures within a design ... ever, but it's a much more intrusive "white-box" approach | 13:37 |
| ZipCPU | Sorry, BMC is "black box" not white box | 13:38 |
| * ZipCPU looks for the editing button on IRC, to edit his prior comment | 13:38 | |
| ZipCPU | I tend to do everything via induction if possible, but ... it's not always possible | 13:38 |
| *** vonnieda has quit IRC | 13:56 | |
| *** rohitksingh has joined #yosys | 14:05 | |
| *** emeb has joined #yosys | 14:07 | |
| *** vonnieda has joined #yosys | 14:10 | |
| *** maikmerten has joined #yosys | 14:38 | |
| pepijndevos_ | ZirconiumX, why are you using a 373 transparent latch as a dff rather than a 374 rising edge triggered flip-flop? Not sure it matters too much, just checking... | 14:56 |
| pepijndevos_ | And I noticed that adding a reset to my simple counter adds a lot of logic. I wonder if a resettable flip-flop could get rid of a lot of that. | 14:57 |
| *** m4ssi has quit IRC | 15:11 | |
| *** gsi__ is now known as gsi_ | 15:15 | |
| ZirconiumX | pepijndevos_: That must be a typo; I meant the 374 | 15:25 |
| *** rohitksingh has quit IRC | 15:38 | |
| pepijndevos_ | Lol... it turns out kicad does not have an autorouter at all. I found a forum thread that argued that it's not needed as much these days as back when people made stacks of 74xx boards. | 15:44 |
| ZirconiumX | pepijndevos_: Google FreeRouting | 15:46 |
| ZirconiumX | The KiCad built-in autorouter was terrible, so they binned it | 15:47 |
| pepijndevos_ | Yea, from what I can tell freerouting is some old java applet that's been open sourced | 15:48 |
| pepijndevos_ | Maybe it's not as bad as it seems... | 15:49 |
| *** rohitksingh has joined #yosys | 16:01 | |
| *** dys has joined #yosys | 16:05 | |
| pepijndevos_ | ZirconiumX, OMG, it works https://imgur.com/a/kPE78JB | 16:07 |
| tpb | Title: Verilog to PCB - Album on Imgur (at imgur.com) | 16:07 |
| ZirconiumX | pepijndevos_: Now *you're* using 373s :P | 16:07 |
| pepijndevos_ | But uuh, yea, will change that to 374 haha | 16:08 |
| *** fsasm has joined #yosys | 16:34 | |
| pepijndevos_ | wat... I no git. | 17:04 |
| ZirconiumX | pepijndevos_: ? | 17:14 |
| pepijndevos_ | ZirconiumX, you merged the pr in a way that when I pulled it it said my branch was 8 commits ahead. So I did some magic from stack overflow and now I'm on a fresh branch with my KiCad work. PR sent :) | 17:24 |
| pepijndevos_ | Verry WIP | 17:25 |
| ZirconiumX | I don't merge PRs | 17:25 |
| ZirconiumX | I rebase | 17:25 |
| pepijndevos_ | Right. I always struggle with a rebase workflow and end up force pushing a lot *facepalm* | 17:26 |
| pepijndevos_ | 74AC11074 seems to be barely used, and does not have an area set | 17:39 |
| maikmerten | verilog to PCB... huh? Is that really a thing? | 17:40 |
| pepijndevos_ | Almost kinda hahaha | 17:40 |
| ZipCPU | I've heard of it from the standpoint of formal | 17:40 |
| ZipCPU | ... as in, formally verify your PCB traces before sending the design out for manufacture | 17:41 |
| maikmerten | "designing logical circuits with NORs and 555s exclusively" | 17:41 |
| pepijndevos_ | maikmerten, kinda... ZirconiumX made a yosys liberty cell library for 74xx logic chips | 17:44 |
| *** rohitksingh has quit IRC | 17:44 | |
| pepijndevos_ | and I'm currently trying to generate a kicad netlist from it | 17:44 |
| maikmerten | excellent! :-) | 17:45 |
| pepijndevos_ | https://github.com/ZirconiumX/74xx-liberty | 17:45 |
| ZirconiumX | I'm not crazy | 17:45 |
| tpb | Title: GitHub - ZirconiumX/74xx-liberty (at github.com) | 17:45 |
| ZirconiumX | I think | 17:45 |
| pepijndevos_ | There is a thin line betwee genius and crazy, and you might be just on the right side... I think, maybe. | 17:45 |
| *** rohitksingh has joined #yosys | 17:48 | |
| pepijndevos_ | I'm wondering what would be a good balance of size and complexity for a first PCB to order. Preferrably something with only a hand full of chips with as much variety as possible. It'd be a bit sad to order your risc-V board and find all the flip-flops have their footrpint backwards. | 17:49 |
| maikmerten | hmmm... perhaps something like an IR decoder (e.g. NEC protocol) or a SPI controller? | 17:52 |
| maikmerten | something like "shift 8 bits in, transmit via SPI, shift received bits out" | 17:53 |
| pepijndevos_ | Ehhhh, the number of chips grows rather quick even for simple stuff. This currently needs 20 chips https://github.com/ZirconiumX/74xx-liberty/blob/master/benchmarks/pwm256.v | 17:56 |
| tpb | Title: 74xx-liberty/pwm256.v at master · ZirconiumX/74xx-liberty · GitHub (at github.com) | 17:56 |
| pepijndevos_ | And it uses like 10 different chips, so that might in fact be a good candidate. | 17:57 |
| maikmerten | right. I forget how awesome highly-integrated ICs are. | 17:58 |
| pepijndevos_ | But stuff like the Gigagron uses very few chips for what it can do, so maybe there is still room for improvement. Or it requires very dedicated verilog compared to random code from the web. | 18:00 |
| maikmerten | (I also forget how awesome nextpnr vs. arachne-pnr is. Currently building picoSOC with the traditional toolchain and arachne-pnr takes three minutes to route) | 18:00 |
| maikmerten | I assume you'd need to be very 74xx-minded to get compact results | 18:01 |
| pepijndevos_ | Reset? Who needs it... | 18:04 |
| pepijndevos_ | ugh... 74xx chips are so complicated... why not do something simple like relay logic | 18:09 |
| ZirconiumX | maikmerten: It helps that 74xx chips are generally tri-state | 18:13 |
| ZirconiumX | Which Yosys tends not to handle wel | 18:14 |
| ZirconiumX | l | 18:14 |
| maikmerten | oh, right | 18:14 |
| ZirconiumX | I remember seeing a chip list for the PDP-11/45 | 18:14 |
| ZirconiumX | But I can't find it | 18:15 |
| *** rohitksingh has quit IRC | 18:49 | |
| *** dys has quit IRC | 19:45 | |
| *** lutsabound has joined #yosys | 19:55 | |
| pepijndevos_ | ZirconiumX, "Implement the Knight processor in FPGA and then convert into TTL." https://github.com/oriansj/stage0 | 20:11 |
| tpb | Title: GitHub - oriansj/stage0: A set of minimal dependency bootstrap binaries (at github.com) | 20:11 |
| *** dys has joined #yosys | 20:25 | |
| *** maikmerten has quit IRC | 20:28 | |
| *** adjtm_ has joined #yosys | 20:44 | |
| *** adjtm has quit IRC | 20:47 | |
| *** awordnot has quit IRC | 21:36 | |
| *** nurelin_ has quit IRC | 21:36 | |
| *** awordnot has joined #yosys | 21:37 | |
| *** nurelin_ has joined #yosys | 21:50 | |
| *** lutsabound has quit IRC | 22:04 | |
| *** fsasm has quit IRC | 22:33 | |
| *** vonnieda has quit IRC | 22:56 | |
| *** lutsabound has joined #yosys | 23:01 | |
| *** m_hackerfoo has joined #yosys | 23:06 | |
| *** hackerfoo has joined #yosys | 23:07 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!