Friday, 2022-07-01

lkclprogrammerjake, the fsub proof looks good. if you do the remaining EUR 1650 from on fmul we can call that one quits and move on quickly to other things08:30
programmerjakeyeah, that's the plan, or maybe on fma (which we need anyway)08:31
lkclthe checking-modes for fma are 300+ lines of ultra-dense code (john hauser's expert implementation)08:34
lkclfmul is a much simpler and straightforward initial target08:35
lkclthat doesn't require HDL to be written08:35
programmerjakehmm, 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 proof08:37
lkclok then go for it08:37
lkclif it wasn't for the formal proof i'd say no way08:37
programmerjakenote 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 weekend08:39
lkclno problem08:39
* lkcl just raising the bugreport and linking it...08:39
lkcli think there's some budget around somewhere for rounding modes let me check...08:41
programmerjakeoh, i just took it from the formal proof budget08:47
lkclyes, i was wondering if there's more (non-formal-proof)08:48
lkclbut i just realised, #48 is from the original core 2019-02-012 and that's done @ 50k08:49
programmerjakei 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
programmerjake(there may be more than 7 if something else reads fpscr.rn when in round-to-odd mode and08:51
programmerjakedistinguishes more than just RTN vs. not RTN)08:51
programmerjakefor 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
lkclpffh, fantastic. that's a big deal. i cannot begin to tell you how long that would have taken me09:11
programmerjakethe vast majority of what changes when changing rounding modes is already implemented -- i added it for fadd09:13
lkclprogrammerjake, btw you have about EUR 12,000 of RFPs outstanding!10:15
lkcldo put them in asap, to make sure they get considered.10:17
programmerjakeyeah, 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
lkcldon't hold back the declaration "completed".10:22
lkcli've already created a repo "sby"10:22
lkclwe absolutely cannot wait for other people10:22
lkclVeera[m], i've moved the extra image to
programmerjakeyeah, i know...later i'll refactor the tasks to be defined as "write all the PRs" rather than get them merged upstream10:24
lkclVeera[m], which means this one is done
lkclVeera[m], you have about.... EUR 3,000 of RFPs outstanding, do put them in!10:25
lkclholy cow there's EUR 8650 for nmutil formal proofs, and other low-level modules10:50
lkclEUR 6550 on Power ISA pipeline proofs
lkcland EUR 5,000 for a 6600 scoreboard proof
lkclcesar, would you like to do a formal proof of the 3-way ISSuE-READ-WRITE?10:52
lkclor, didn't you do one already?10:52
lkclat least, of the MultiCompUnit?10:53
lkclyes you did10:55
cesarI was improving the unit test, to use parallel processes. I have the intention of doing a formal proof of MultiCompUnit, indeed.11:00
cesarI did made a formal proof of a simple ALU, used in the tests.11:02
cesarI'd be pleased to resume work on a MultiCompUnit formal proof, indeed.11:03
cesarIt'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
cesarIt was a learning exercise at the time...11:07
lkclit's still great, cesar, and yes that would qualify!11:27
cesarNice! I'll make a point to go back and fully implement the formal proof of MultiCompUnit.11:30
lkclcesar, do raise it as a separate bugreport, under
cesarCreating 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
lkclcesar, yes.13:54
lkclmake sure the "NLnet milestone" drop-down field is is the right milestone "NLnet.2019.10.032.Formal"13:56
ghostmansdYet another question on registers. Except for GPR/FPR/CR, do we support other registers in sv. mode?17:22
ghostmansdI'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
ghostmansdOn 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
ghostmansdAlso, should we support notation with dot, like PPC does?17:26
ghostmansdFor example, %r.10 and %r10 are the same thing.17:26
ghostmansdSame for %sp and %r.sp.17:27
ghostmansdAnd so on.17:27
ghostmansdThe simplest and, perhaps, the sanest option, I guess, is falling back.17:40
ghostmansdThat 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
lkclghostmansd, yes, at some point, SPRs will also be vectoriseable18:16
lkclbut *not* extended.  they are system registers, there's 1024 of them.18:16
ghostmansdMhm... I see aliases for a couple of these.18:18
lkclyeah a fallback to vanilla would work, it would mean that the EXTRA2/3 would be zero18:18
ghostmansdI could count about 9 SPR aliases.18:18
* lkcl thinks...18:19
ghostmansdAh yeah18:19
lkclah 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
lkcli just realised18:19
lkcl<lkcl>                 ("%vr", 0, 128, "(PPC_OPERAND_GPR | PPC_OPERAND_SVP64)")18:20
lkclya grok that?18:20
programmerjakevr is already used iirc18:20
lkclnot with "%" in front of it18:21
programmerjakeso svp64 can't take it18:21
ghostmansdWith % too :-)18:21
ghostmansdOr you mean %%?18:21
lkclwhatever - pick a prefix character that's unique18:21
lkclany prefix character that's guaranteed to be unique18:22
programmerjake% is just a way to differentiate between regs and user symbols18:22
ghostmansdFor 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
programmerjakeyou mean like 😁vr2318:23
ghostmansdWhoa, programmerjake made a smiley :-)18:23
ghostmansdDo 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
programmerjakeor if we're feeling extra annoying we could do νr23 where that ν is a greek nu18:25
ghostmansdSorry, ASCII-centric :-)18:26
lkclyes, SPRs will need to be Vectorised. but not straight away. i haven't done any SPR-related instructions yet18:26
ghostmansdActually per PPC we likely should provide variants like %v:r.12718:26
ghostmansdNotice the dot18:26
programmerjakeyeah, those two proposals with non-ascii characters are a joke18:27
lkclghostmansd, you'll likely find it's a pain in the ass _not_ to add those variants18:27
lkcl%v: is too many characters btw18:27
ghostmansd> pain in the ass18:28
ghostmansdYeah that's one of the reasons I thought I'll add these18:28
ghostmansd> %v: is too many characters btw18:28
ghostmansdideas are welcome :-)18:28
ghostmansdPercent 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
programmerjakevvr23 -- doubled v18:29
ghostmansdI'd use use t18:30
ghostmansdt for tile18:30
lkcl"%:" would do18:31
programmerjakehmm, but svp64 doesn't really use tiles...18:31
ghostmansdNo, I mean, instead of v18:31
lkclyes. "%:"18:31
ghostmansdor X as extended18:31
ghostmansdYeah that'd do18:31
lkcl"%:" instead of v.  short.18:31
ghostmansdA damn fucking strange I have to admit :-)18:31
ghostmansdIsn't it easy to miss semicolon?18:32
ghostmansdHmmmmmm.... perhaps @ or $ or similar?18:32
programmerjake%:r5 short, imho easily missed...imho we should have a letter18:32
lkclno on $.18:32
ghostmansd$ is part of the name in some assembler flavors18:33
lkcl    case '$':18:33
lkcl      if (LOCAL_LABELS_DOLLAR)18:33
lkcl        {18:33
ghostmansdYeah that's what I also had in mind18:33
ghostmansdSo yeah, no dollars18:33
ghostmansd(euros? just kidding)18:33
lkcl    case '@':18:33
lkcl      if (! flag_m68k_mri)18:33
lkcl    goto de_fault;18:33
lkclbut that's on #ifdef TC_M68K18:34
lkclso is actually available18:34
ghostmansdLuke, you're looking in a different part18:34
lkclalthough... ah ok18:34
ghostmansdThe register names on powerpc...18:34
lkcli'm looking at operand() very deliberately to make sure it's not confused with any macro/operand parsing18:35
ghostmansd...they handle it differently18:35
ghostmansdjust a moment18:35
ghostmansdTL;DR: they don't give a fuck to pass it to operand()18:35
lkclif the right prefix is picked there *is* no need to look at register names18:36
lkclshouldn't be18:36
ghostmansdNot really, otherwise they wouldn't bother to do parsing on their side.18:36
ghostmansdI mean, they circumvent the operand.18:36
programmerjakeborrow math vector syntax: %<r5>18:36
ghostmansdI guess this is related to fact that each and every platform does registers differently.18:36
lkclprogrammerjake, that's confused with less-than and greater-than in expressions18:37
ghostmansdI mean, every assembly flavor gets it in their own way.18:37
ghostmansdSo, anyway. register_name is the place we want to edit.18:37
programmerjake%< is unique and not confused with <18:37
ghostmansdBecause this is what they use in PPC.18:37
programmerjakeso, just keep parsing to the closing >18:37
ghostmansdThe only question is what convention we'll use.18:38
lkclprogrammerjake, this is not like normal parsers.  this is binutils.  speed and absolute bare minimum processing is absolutely critical18:38
lkclthe whole reason why this discussion is taking place is to very specifically avoid suffix-identification18:38
lkcl"%:" is about as trivial as it gets18:39
ghostmansdYes, this is one of the issues. But it's not only about speed.18:39
programmerjakeparsing to the closing > is trivial, looking up in the register table would be slower than that18:39
ghostmansdThis is also about principle of least surprize.18:39
ghostmansd%r127 won't surprize anyone.18:39
lkcl840   if (name[0] == '%' && name[1] == ':') { ....18:39
ghostmansdNah even simpler.18:40
ghostmansdNo need to adjust this code, we can just generate all entries for all registers.18:40
lkcl%r127 matches with line 84018:40
lkclas would %r3118:40
ghostmansdYeah but we'll have to introduce our own table18:41
ghostmansdcf. 84718:41
lkclwhich means that now %r31 is ambiguous18:41
ghostmansdI want to simply resort to different table for SVP64.18:41
ghostmansdEach instruction starting with sv. will look up the different table.18:42
ghostmansdThis is just an additional argument to register_name function.18:42
ghostmansdAnd so it'll lookup a different table first...18:42
lkclah that would work18:42
ghostmansdand only then resort to table on line 84718:42
ghostmansdThis already works :-)18:42
ghostmansdI mean, it's in branches, but it works18:43
ghostmansdThe only thing is what convention to choose18:43
lkclyes if it's *only* called when "sv." is active, that works18:43
ghostmansdYep, only for sv.18:43
programmerjakehow about forcing all register operands to a sv.instr to start with a prefix s or v that is stripped before lookup?18:43
ghostmansdIt's actually simple to pass an `struct svp64_ctx *svp64` argument18:43
ghostmansdAnd it's NULL for any insn except for SV.XXX18:44
ghostmansdWe don't even need to strip it18:44
programmerjakeso sv.add vr30, sr40, vr5018:44
ghostmansdFirst, these should have %18:45
ghostmansdBecause this is how they mark the regs unless one gives -mregnames option.18:45
ghostmansdSecond... They have stuff like vs.10.18:45
ghostmansdAltivec registers.18:45
ghostmansdAnd third... again, why mark scalar registers?18:46
ghostmansdWe simply extend them.18:46
ghostmansdI basically feel that we're going in circles. :-)18:46
ghostmansdMy feeling is that we only need to mark vector registers somehow, that's it.18:46
ghostmansdAnd we only need to choose the good ASCII candidate.18:47
ghostmansdAs prefix. It's important.18:47
lkcl 831 register_name (expressionS *expressionP, struct svp64_ctx *svp64)18:47
lkcl840   if svp64 == NULL && (name[0] == '%' && ISALPHA (name[1]))18:47
ghostmansdThis is exactly what I have :-)18:47
programmerjakemark 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 sr518:47
ghostmansdtoo lazy to commit18:48
programmerjakeif you want to access vr5 in a sv.instr, use sv.instr %vvr5, %svr518:49
ghostmansd(this is variant for semicolon)18:49
lkclghostmansd, 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 registers18:49
ghostmansdI do, because otherwise I need to parse the integer18:50
lkclokok yes.18:50
ghostmansdEven if it has prefix, you know, there's still not 128, but 32 registers18:50
ghostmansdSo if we have the table anyway, for preformance...18:50
ghostmansdI've been thinking of making this table big and simply get the fricking registers immediately18:51
programmerjakehow 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 mode18:54
programmerjakewhich means a asm template string could be `asm("sv.add *%1, %2, %%r5" : ...)`18:55
programmerjakeshould be unambiguous in expressions, just like c's dereference operator is unambiguous18:56
ghostmansdHm. * looks a promising candidate.19:00
ghostmansd{"*r119", 119, PPC_OPERAND_GPR | PPC_OPERAND_VECTOR}19:03
ghostmansd{"r96", 96, PPC_OPERAND_GPR}19:03
ghostmansdand so on, you get the idea19:03
programmerjakewhat I was thinking of is you'd be adding a new operator rather than a giant pile of vector registers19:03
programmerjakeyou'd still have %r127 but that's a scalar reg19:04
ghostmansdYep, and for vectors?19:04
ghostmansd{"*r119", 119, PPC_OPERAND_GPR | PPC_OPERAND_VECTOR} is %*r11919:04
programmerjakewrite *%r12719:04
programmerjakewhere that's 2 tokens: * operator and %r127 reg name19:05
ghostmansdThat'd break the convention that registers start with %19:05
ghostmansdI have no doubts that % must be first, even for vectors.19:05
programmerjakeyes, because the * isn't a register name19:05
ghostmansdFrom lexer's perspective, it _is_.19:06
programmerjakeiirc we'd not be the first ones to have * in the syntax19:06
ghostmansdI understand what you mean, though...19:06
ghostmansdKinda like "dereference vector corresponding to register 127"19:06
ghostmansdSo I like the idea, let's wait for Luke19:07
programmerjakewell, the lexer shouldn't return reg name *%r127, it'd return * operator and %r127 reg name19:07
ghostmansdI think we can just simply notice the fact we had an asterisk :-)19:08
ghostmansdLike how they advance input_line_ptr with %19:08
ghostmansdSo yeah dead simple19:08
ghostmansdJust store the fact that it starts with asterisk, and later OR a flag or change operator type or something similar19:09
ghostmansdnot operator, expression, I mean19:09
ghostmansdOK lkcl it's your turn :-)19:09
ghostmansdI can do whatever we agree on19:10
programmerjakee.g. x86_64's jmp *%rax imstruction19:10
ghostmansd[m]Yeah. It has nothing to do with vectors, though...19:28
ghostmansdYeas 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
ghostmansdI'm not sure of * syntax, but the idea in essense looks fine to me.21:05
ghostmansdI've chosen this approach for now.21:05
cesartplaten: I'm also getting "Failed to find a route for arc 2 of net ddrphy_ddr3_0__a__o_fclk", for on the OrangeCrab.23:17
cesarI also made an alternative version for your changes to the OrangeCrab DDR3 pinouts in nmigen-boards:
cesarI propose to swap just DM, instead of both DQS and DQ.23:32

Generated by 2.17.1 by Marius Gedminas - find it at!