| lkcl | programmerjake, the fsub proof looks good. if you do the remaining EUR 1650 from https://bugs.libre-soc.org/show_bug.cgi?id=196 on fmul we can call that one quits and move on quickly to other things | 08:30 |
|---|---|---|
| programmerjake | yeah, that's the plan, or maybe on fma (which we need anyway) | 08:31 |
| lkcl | the checking-modes for fma are 300+ lines of ultra-dense code (john hauser's expert implementation) | 08:34 |
| lkcl | fmul is a much simpler and straightforward initial target | 08:35 |
| lkcl | that doesn't require HDL to be written | 08:35 |
| programmerjake | hmm, imho i could mostly copy the fma i wrote as part of simple-soft-float -- i'm quite familiar with it and expect it to take <2 days to get a working fma with formal proof | 08:37 |
| lkcl | ok then go for it | 08:37 |
| lkcl | if it wasn't for the formal proof i'd say no way | 08:37 |
| programmerjake | note that's 2 days of my working on it, so it could likely be done by monday since i'm not usually working much on the weekend | 08:39 |
| lkcl | no problem | 08:39 |
| * lkcl just raising the bugreport and linking it... | 08:39 | |
| lkcl | i think there's some budget around somewhere for rounding modes let me check... | 08:41 |
| programmerjake | oh, i just took it from the formal proof budget | 08:47 |
| programmerjake | https://bugs.libre-soc.org/show_bug.cgi?id=874 | 08:47 |
| lkcl | yes, i was wondering if there's more (non-formal-proof) | 08:48 |
| lkcl | but i just realised, #48 is from the original core 2019-02-012 and that's done @ 50k | 08:49 |
| programmerjake | i implemented all 7 distinct rounding modes required by the openpower spec (includes ones only needed for f128 cuz I could and they weren't too hard) | 08:49 |
| lkcl | https://bugs.libre-soc.org/show_bug.cgi?id=877 | 08:49 |
| programmerjake | (there may be more than 7 if something else reads fpscr.rn when in round-to-odd mode and | 08:51 |
| programmerjake | distinguishes more than just RTN vs. not RTN) | 08:51 |
| programmerjake | for implementing fma, i'm planning on doing all rounding modes at once, no need to do just nearest-even then later add the others... | 08:54 |
| lkcl | pffh, fantastic. that's a big deal. i cannot begin to tell you how long that would have taken me | 09:11 |
| programmerjake | the vast majority of what changes when changing rounding modes is already implemented -- i added it for fadd | 09:13 |
| lkcl | programmerjake, btw you have about EUR 12,000 of RFPs outstanding! | 10:15 |
| lkcl | do put them in asap, to make sure they get considered. | 10:17 |
| programmerjake | yeah, i'll do that after the fma stuff is done. i was waiting on smtlib2 stuff getting merged in upstream yosys and sby, but it looks like that could take a while... | 10:21 |
| lkcl | don't hold back the declaration "completed". | 10:22 |
| lkcl | i've already created a repo "sby" | 10:22 |
| lkcl | we absolutely cannot wait for other people | 10:22 |
| lkcl | Veera[m], i've moved the extra image to https://bugs.libre-soc.org/show_bug.cgi?id=878 | 10:23 |
| programmerjake | yeah, i know...later i'll refactor the tasks to be defined as "write all the PRs" rather than get them merged upstream | 10:24 |
| lkcl | Veera[m], which means this one is done https://bugs.libre-soc.org/show_bug.cgi?id=839 | 10:25 |
| lkcl | Veera[m], you have about.... EUR 3,000 of RFPs outstanding, do put them in! | 10:25 |
| lkcl | holy cow there's EUR 8650 for nmutil formal proofs, and other low-level modules | 10:50 |
| lkcl | https://bugs.libre-soc.org/show_bug.cgi?id=198 | 10:51 |
| lkcl | EUR 6550 on Power ISA pipeline proofs https://bugs.libre-soc.org/show_bug.cgi?id=195 | 10:51 |
| lkcl | and EUR 5,000 for a 6600 scoreboard proof https://bugs.libre-soc.org/show_bug.cgi?id=197 | 10:51 |
| lkcl | cesar, would you like to do a formal proof of the 3-way ISSuE-READ-WRITE? | 10:52 |
| lkcl | or, didn't you do one already? | 10:52 |
| lkcl | at least, of the MultiCompUnit? | 10:53 |
| lkcl | yes you did | 10:55 |
| cesar | I was improving the unit test, to use parallel processes. I have the intention of doing a formal proof of MultiCompUnit, indeed. | 11:00 |
| cesar | I did made a formal proof of a simple ALU, used in the tests. | 11:02 |
| cesar | I'd be pleased to resume work on a MultiCompUnit formal proof, indeed. | 11:03 |
| cesar | It's coming back to me. You asked me once for an example of a FSM CompUnit. In the process of implementing it, I did a formal correctness proof of it. Nothing more. | 11:05 |
| cesar | It was a learning exercise at the time... | 11:07 |
| lkcl | it's still great, cesar, and yes that would qualify! | 11:27 |
| cesar | Nice! I'll make a point to go back and fully implement the formal proof of MultiCompUnit. | 11:30 |
| lkcl | cesar, do raise it as a separate bugreport, under https://bugs.libre-soc.org/show_bug.cgi?id=197 | 11:41 |
| cesar | Creating a new bug report "under" bug 197 means I fill its "parent task for budget allocation" field, with "197", right? Just checking. | 12:28 |
| cesar | (on the new bug, not 197 itself) | 12:29 |
| lkcl | cesar, yes. | 13:54 |
| lkcl | make sure the "NLnet milestone" drop-down field is is the right milestone "NLnet.2019.10.032.Formal" | 13:56 |
| ghostmansd | Yet another question on registers. Except for GPR/FPR/CR, do we support other registers in sv. mode? | 17:22 |
| ghostmansd | I'm kinda thinking, on register lookup, why don't we fallback to the vanilla registers and look up there, if we failed to find the register in SVP64 registers table. | 17:23 |
| ghostmansd | On the other hand, I'd like the SVP64 table to contain all possible registers for SVP64. First of all, since we decided to keep only canonical names, that'd be consistent and simple. Second, why do two binary searches in two different tables, if you can do it in one generated? | 17:25 |
| ghostmansd | Also, should we support notation with dot, like PPC does? | 17:26 |
| ghostmansd | For example, %r.10 and %r10 are the same thing. | 17:26 |
| ghostmansd | Same for %sp and %r.sp. | 17:27 |
| ghostmansd | And so on. | 17:27 |
| ghostmansd | The simplest and, perhaps, the sanest option, I guess, is falling back. | 17:40 |
| ghostmansd | That said, I still believe that we should not allow a simple 117 instead of %r117, unlike vanilla PPC, and this is my assumption for the code. | 17:49 |
| lkcl | ghostmansd, yes, at some point, SPRs will also be vectoriseable | 18:16 |
| lkcl | but *not* extended. they are system registers, there's 1024 of them. | 18:16 |
| ghostmansd | Mhm... I see aliases for a couple of these. | 18:18 |
| lkcl | yeah a fallback to vanilla would work, it would mean that the EXTRA2/3 would be zero | 18:18 |
| ghostmansd | I could count about 9 SPR aliases. | 18:18 |
| * lkcl thinks... | 18:19 | |
| ghostmansd | Ah yeah | 18:19 |
| lkcl | ah where's that register naming thing... | 18:19 |
| lkcl | <lkcl> ("r", 0, 32, "PPC_OPERAND_GPR"), | 18:19 |
| lkcl | <lkcl> ("r", 32, 128, "(PPC_OPERAND_GPR | PPC_OPERAND_SVP64)") | 18:19 |
| lkcl | i just realised | 18:19 |
| lkcl | <lkcl> ("%vr", 0, 128, "(PPC_OPERAND_GPR | PPC_OPERAND_SVP64)") | 18:20 |
| lkcl | ta-daaaa | 18:20 |
| lkcl | ya grok that? | 18:20 |
| programmerjake | vr is already used iirc | 18:20 |
| lkcl | not with "%" in front of it | 18:21 |
| programmerjake | so svp64 can't take it | 18:21 |
| ghostmansd | With % too :-) | 18:21 |
| ghostmansd | Or you mean %%? | 18:21 |
| lkcl | whatever - pick a prefix character that's unique | 18:21 |
| lkcl | any prefix character that's guaranteed to be unique | 18:22 |
| programmerjake | % is just a way to differentiate between regs and user symbols | 18:22 |
| ghostmansd | For now, we have %r0..%r127, %f0..%f127, %cr0..%cr127. In addition, we also have %v:r0..127, and so on for the rest (f and cr). | 18:23 |
| programmerjake | you mean like 😁vr23 | 18:23 |
| ghostmansd | Whoa, programmerjake made a smiley :-) | 18:23 |
| ghostmansd | Do I get correctly that we also need a specific way to alias SPRs? If so, how about %s0..%s1024, and %v:s0..%v:s1024? | 18:25 |
| programmerjake | or if we're feeling extra annoying we could do νr23 where that ν is a greek nu | 18:25 |
| ghostmansd | Sorry, ASCII-centric :-) | 18:26 |
| lkcl | yes, SPRs will need to be Vectorised. but not straight away. i haven't done any SPR-related instructions yet | 18:26 |
| ghostmansd | Actually per PPC we likely should provide variants like %v:r.127 | 18:26 |
| ghostmansd | Notice the dot | 18:26 |
| programmerjake | yeah, those two proposals with non-ascii characters are a joke | 18:27 |
| lkcl | ghostmansd, you'll likely find it's a pain in the ass _not_ to add those variants | 18:27 |
| lkcl | %v: is too many characters btw | 18:27 |
| ghostmansd | > pain in the ass | 18:28 |
| ghostmansd | Yeah that's one of the reasons I thought I'll add these | 18:28 |
| ghostmansd | > %v: is too many characters btw | 18:28 |
| ghostmansd | ideas are welcome :-) | 18:28 |
| ghostmansd | Percent sign is the way lexer works for registers in PPC. They literally use this as sign that some stuff is a register. Otherwise you have to explicitly set -mregnames. | 18:29 |
| programmerjake | vvr23 -- doubled v | 18:29 |
| ghostmansd | I'd use use t | 18:30 |
| lkcl | https://psy.swansea.ac.uk/staff/carter/vim/vim_ascii_chars.htm | 18:30 |
| ghostmansd | t for tile | 18:30 |
| lkcl | "%:" would do | 18:31 |
| programmerjake | hmm, but svp64 doesn't really use tiles... | 18:31 |
| programmerjake | iirc | 18:31 |
| ghostmansd | No, I mean, instead of v | 18:31 |
| lkcl | yes. "%:" | 18:31 |
| ghostmansd | or X as extended | 18:31 |
| ghostmansd | Hmmmm | 18:31 |
| ghostmansd | Yeah that'd do | 18:31 |
| lkcl | "%:" instead of v. short. | 18:31 |
| ghostmansd | A damn fucking strange I have to admit :-) | 18:31 |
| ghostmansd | %:r.10 | 18:32 |
| ghostmansd | Isn't it easy to miss semicolon? | 18:32 |
| ghostmansd | Hmmmmmm.... perhaps @ or $ or similar? | 18:32 |
| programmerjake | %:r5 short, imho easily missed...imho we should have a letter | 18:32 |
| lkcl | no on $. | 18:32 |
| ghostmansd | $ is part of the name in some assembler flavors | 18:33 |
| lkcl | case '$': | 18:33 |
| lkcl | if (LOCAL_LABELS_DOLLAR) | 18:33 |
| lkcl | { | 18:33 |
| ghostmansd | Yeah that's what I also had in mind | 18:33 |
| ghostmansd | So yeah, no dollars | 18:33 |
| ghostmansd | (euros? just kidding) | 18:33 |
| lkcl | case '@': | 18:33 |
| lkcl | if (! flag_m68k_mri) | 18:33 |
| lkcl | goto de_fault; | 18:33 |
| lkcl | but that's on #ifdef TC_M68K | 18:34 |
| lkcl | so is actually available | 18:34 |
| lkcl | %@5 | 18:34 |
| lkcl | %@r5 | 18:34 |
| ghostmansd | Luke, you're looking in a different part | 18:34 |
| lkcl | although... ah ok | 18:34 |
| ghostmansd | The register names on powerpc... | 18:34 |
| lkcl | i'm looking at operand() very deliberately to make sure it's not confused with any macro/operand parsing | 18:35 |
| ghostmansd | ...they handle it differently | 18:35 |
| ghostmansd | just a moment | 18:35 |
| ghostmansd | TL;DR: they don't give a fuck to pass it to operand() | 18:35 |
| ghostmansd | https://git.libre-soc.org/?p=binutils-gdb.git;a=blob;f=gas/config/tc-ppc.c#l831 | 18:35 |
| ghostmansd | https://git.libre-soc.org/?p=binutils-gdb.git;a=blob;f=gas/config/tc-ppc.c#l3414 | 18:35 |
| lkcl | if the right prefix is picked there *is* no need to look at register names | 18:36 |
| lkcl | or | 18:36 |
| lkcl | shouldn't be | 18:36 |
| ghostmansd | Not really, otherwise they wouldn't bother to do parsing on their side. | 18:36 |
| ghostmansd | I mean, they circumvent the operand. | 18:36 |
| programmerjake | borrow math vector syntax: %<r5> | 18:36 |
| ghostmansd | I guess this is related to fact that each and every platform does registers differently. | 18:36 |
| lkcl | programmerjake, that's confused with less-than and greater-than in expressions | 18:37 |
| ghostmansd | I mean, every assembly flavor gets it in their own way. | 18:37 |
| ghostmansd | So, anyway. register_name is the place we want to edit. | 18:37 |
| programmerjake | %< is unique and not confused with < | 18:37 |
| ghostmansd | Because this is what they use in PPC. | 18:37 |
| programmerjake | so, just keep parsing to the closing > | 18:37 |
| ghostmansd | The only question is what convention we'll use. | 18:38 |
| lkcl | programmerjake, this is not like normal parsers. this is binutils. speed and absolute bare minimum processing is absolutely critical | 18:38 |
| lkcl | the whole reason why this discussion is taking place is to very specifically avoid suffix-identification | 18:38 |
| lkcl | "%:" is about as trivial as it gets | 18:39 |
| ghostmansd | Yes, this is one of the issues. But it's not only about speed. | 18:39 |
| programmerjake | parsing to the closing > is trivial, looking up in the register table would be slower than that | 18:39 |
| ghostmansd | This is also about principle of least surprize. | 18:39 |
| ghostmansd | %r127 won't surprize anyone. | 18:39 |
| lkcl | 840 if (name[0] == '%' && name[1] == ':') { .... | 18:39 |
| ghostmansd | Nah even simpler. | 18:40 |
| ghostmansd | No need to adjust this code, we can just generate all entries for all registers. | 18:40 |
| lkcl | %r127 matches with line 840 | 18:40 |
| lkcl | as would %r31 | 18:40 |
| ghostmansd | Yeah but we'll have to introduce our own table | 18:41 |
| ghostmansd | cf. 847 | 18:41 |
| lkcl | which means that now %r31 is ambiguous | 18:41 |
| ghostmansd | I want to simply resort to different table for SVP64. | 18:41 |
| ghostmansd | Each instruction starting with sv. will look up the different table. | 18:42 |
| ghostmansd | This is just an additional argument to register_name function. | 18:42 |
| ghostmansd | And so it'll lookup a different table first... | 18:42 |
| lkcl | ah that would work | 18:42 |
| ghostmansd | and only then resort to table on line 847 | 18:42 |
| ghostmansd | Yep | 18:42 |
| ghostmansd | This already works :-) | 18:42 |
| ghostmansd | I mean, it's in branches, but it works | 18:43 |
| ghostmansd | The only thing is what convention to choose | 18:43 |
| lkcl | yes if it's *only* called when "sv." is active, that works | 18:43 |
| ghostmansd | Yep, only for sv. | 18:43 |
| programmerjake | how about forcing all register operands to a sv.instr to start with a prefix s or v that is stripped before lookup? | 18:43 |
| ghostmansd | It's actually simple to pass an `struct svp64_ctx *svp64` argument | 18:43 |
| ghostmansd | And it's NULL for any insn except for SV.XXX | 18:44 |
| ghostmansd | We don't even need to strip it | 18:44 |
| programmerjake | so sv.add vr30, sr40, vr50 | 18:44 |
| ghostmansd | First, these should have % | 18:45 |
| programmerjake | yeah... | 18:45 |
| ghostmansd | Because this is how they mark the regs unless one gives -mregnames option. | 18:45 |
| ghostmansd | Second... They have stuff like vs.10. | 18:45 |
| ghostmansd | Altivec registers. | 18:45 |
| ghostmansd | And third... again, why mark scalar registers? | 18:46 |
| ghostmansd | We simply extend them. | 18:46 |
| ghostmansd | I basically feel that we're going in circles. :-) | 18:46 |
| ghostmansd | My feeling is that we only need to mark vector registers somehow, that's it. | 18:46 |
| lkcl | yes. | 18:46 |
| ghostmansd | And we only need to choose the good ASCII candidate. | 18:47 |
| ghostmansd | As prefix. It's important. | 18:47 |
| lkcl | 831 register_name (expressionS *expressionP, struct svp64_ctx *svp64) | 18:47 |
| ghostmansd | Yeah | 18:47 |
| lkcl | 840 if svp64 == NULL && (name[0] == '%' && ISALPHA (name[1])) | 18:47 |
| ghostmansd | This is exactly what I have :-) | 18:47 |
| programmerjake | mark scalar registers so you explicitly have an unambiguous prefix that can be stripped, which means that sv.addi %vr5, %sr5, 5 can't conflict with any registers named vr5 or sr5 | 18:47 |
| ghostmansd | too lazy to commit | 18:48 |
| ghostmansd | https://pastebin.com/rEZ7M5LR | 18:48 |
| programmerjake | if you want to access vr5 in a sv.instr, use sv.instr %vvr5, %svr5 | 18:49 |
| ghostmansd | (this is variant for semicolon) | 18:49 |
| lkcl | ghostmansd, programmerjake has a point. if *every* register *has* to have a prefix "v" or "s" then you won't need an explicit table of svp64 registers | 18:49 |
| ghostmansd | I do, because otherwise I need to parse the integer | 18:50 |
| lkcl | okok yes. | 18:50 |
| ghostmansd | Even if it has prefix, you know, there's still not 128, but 32 registers | 18:50 |
| lkcl | yes | 18:50 |
| lkcl | doh | 18:50 |
| ghostmansd | So if we have the table anyway, for preformance... | 18:50 |
| ghostmansd | I've been thinking of making this table big and simply get the fricking registers immediately | 18:51 |
| programmerjake | how about mirroring python's *args feature and use sv.instr *%r10, %r15, *%r20 -- * first so llvm/gcc can generate the register name and you don't have to have a whole separate table of register names in gcc/llvm for vector mode | 18:54 |
| programmerjake | which means a asm template string could be `asm("sv.add *%1, %2, %%r5" : ...)` | 18:55 |
| lkcl | ghostmansd, https://ftp.libre-soc.org/regname.c | 18:55 |
| programmerjake | should be unambiguous in expressions, just like c's dereference operator is unambiguous | 18:56 |
| ghostmansd | Hm. * looks a promising candidate. | 19:00 |
| ghostmansd | https://pastebin.com/itA7QaxG | 19:03 |
| ghostmansd | {"*r119", 119, PPC_OPERAND_GPR | PPC_OPERAND_VECTOR} | 19:03 |
| ghostmansd | {"r96", 96, PPC_OPERAND_GPR} | 19:03 |
| ghostmansd | and so on, you get the idea | 19:03 |
| programmerjake | what I was thinking of is you'd be adding a new operator rather than a giant pile of vector registers | 19:03 |
| programmerjake | you'd still have %r127 but that's a scalar reg | 19:04 |
| ghostmansd | Yep, and for vectors? | 19:04 |
| ghostmansd | {"*r119", 119, PPC_OPERAND_GPR | PPC_OPERAND_VECTOR} is %*r119 | 19:04 |
| programmerjake | write *%r127 | 19:04 |
| programmerjake | where that's 2 tokens: * operator and %r127 reg name | 19:05 |
| ghostmansd | That'd break the convention that registers start with % | 19:05 |
| ghostmansd | I have no doubts that % must be first, even for vectors. | 19:05 |
| programmerjake | yes, because the * isn't a register name | 19:05 |
| ghostmansd | From lexer's perspective, it _is_. | 19:06 |
| programmerjake | iirc we'd not be the first ones to have * in the syntax | 19:06 |
| ghostmansd | I understand what you mean, though... | 19:06 |
| ghostmansd | Kinda like "dereference vector corresponding to register 127" | 19:06 |
| ghostmansd | So I like the idea, let's wait for Luke | 19:07 |
| programmerjake | well, the lexer shouldn't return reg name *%r127, it'd return * operator and %r127 reg name | 19:07 |
| ghostmansd | yehyeh | 19:07 |
| ghostmansd | I think we can just simply notice the fact we had an asterisk :-) | 19:08 |
| ghostmansd | Like how they advance input_line_ptr with % | 19:08 |
| ghostmansd | So yeah dead simple | 19:08 |
| ghostmansd | Just store the fact that it starts with asterisk, and later OR a flag or change operator type or something similar | 19:09 |
| ghostmansd | not operator, expression, I mean | 19:09 |
| ghostmansd | OK lkcl it's your turn :-) | 19:09 |
| ghostmansd | I can do whatever we agree on | 19:10 |
| programmerjake | e.g. x86_64's jmp *%rax imstruction | 19:10 |
| ghostmansd[m] | Yeah. It has nothing to do with vectors, though... | 19:28 |
| ghostmansd | Yeas the more I think about programmerjake suggestion the more I like it. I mean, it kinda logical. First, we extend the architecture with more registers; second, we give a way to act on vectors. For both of these, we just modify the mnemonics. First simply allows more registers (e.g. %r127 can now be parsed), and the second just gets a special prefix qualifier. | 21:05 |
| ghostmansd | I'm not sure of * syntax, but the idea in essense looks fine to me. | 21:05 |
| ghostmansd | I've chosen this approach for now. | 21:05 |
| cesar | tplaten: I'm also getting "Failed to find a route for arc 2 of net ddrphy_ddr3_0__a__o_fclk", for ls2.py on the OrangeCrab. | 23:17 |
| cesar | I also made an alternative version for your changes to the OrangeCrab DDR3 pinouts in nmigen-boards: https://gitlab.com/nmigen/nmigen-boards/-/merge_requests/4 | 23:30 |
| cesar | I propose to swap just DM, instead of both DQS and DQ. | 23:32 |
Generated by irclog2html.py 2.17.1 by Marius Gedminas - find it at https://mg.pov.lt/irclog2html/!