*** tpb has joined #yosys | 00:00 | |
*** emeb has quit IRC | 00:23 | |
*** emeb_mac has joined #yosys | 00:29 | |
*** gsi__ has joined #yosys | 00:53 | |
*** gsi_ has quit IRC | 00:56 | |
*** AlexDaniel has quit IRC | 01:18 | |
*** FL4SHK has quit IRC | 01:23 | |
*** FL4SHK has joined #yosys | 01:27 | |
*** fevv8[m] has joined #yosys | 01:40 | |
*** citypw has joined #yosys | 02:20 | |
*** vonnieda has joined #yosys | 02:27 | |
*** PyroPeter has quit IRC | 02:47 | |
*** PyroPeter has joined #yosys | 03:00 | |
*** emeb_mac has left #yosys | 03:20 | |
*** emeb_mac has joined #yosys | 03:21 | |
*** mirage335 has quit IRC | 03:53 | |
*** mirage335 has joined #yosys | 04:03 | |
*** proteusguy has quit IRC | 04:17 | |
*** rohitksingh_work has joined #yosys | 04:31 | |
*** knielsen has joined #yosys | 04:49 | |
*** proteusguy has joined #yosys | 05:34 | |
*** dys has quit IRC | 05:35 | |
*** vonnieda_ has joined #yosys | 05:46 | |
*** vonnieda has quit IRC | 05:48 | |
*** gsi__ is now known as gsi_ | 06:18 | |
*** kraiskil has joined #yosys | 06:26 | |
*** emeb_mac has quit IRC | 06:32 | |
*** Jybz has joined #yosys | 06:40 | |
*** citypw has quit IRC | 07:18 | |
*** kraiskil has quit IRC | 07:34 | |
*** m4ssi has joined #yosys | 07:52 | |
*** citypw has joined #yosys | 07:58 | |
*** kraiskil has joined #yosys | 08:00 | |
pepijndevos_ | This is so weird... with async reset Yosys breaks my multiplication and then optimizes it away. | 08:20 |
---|---|---|
*** fsasm has joined #yosys | 08:24 | |
*** proteusguy has quit IRC | 09:17 | |
pepijndevos_ | ZirconiumX, any chance you could commit that comparator pass for me to play with? | 09:30 |
ZirconiumX | pepijndevos_: yeah, give me a bit | 09:31 |
pepijndevos_ | I think that if that works, the PWM benchmark should be quite compact. | 09:31 |
pepijndevos_ | If I can get that down to a reasonable amout of chips, I think it'd be a good PoC to order that on PCB for the most elaborate fading LED thing ever. | 09:33 |
ZirconiumX | pepijndevos_: I think the 181 is available in the LS family, but I can't quite tell | 09:35 |
pepijndevos_ | https://nl.mouser.com/Search/Refine?Keyword=74ls181 they know it exists, but don't actually have any in stock | 09:38 |
pepijndevos_ | It also exists in the HC family, but no stock either. | 09:39 |
*** proteusguy has joined #yosys | 09:53 | |
*** pie_ has quit IRC | 09:56 | |
*** fsasm has quit IRC | 10:02 | |
*** fsasm has joined #yosys | 10:16 | |
ZirconiumX | pepijndevos_: I pushed my comparator pass in the `cmp` branch | 10:35 |
*** adjtm_ has quit IRC | 10:39 | |
*** adjtm_ has joined #yosys | 10:39 | |
pepijndevos_ | thanks | 11:07 |
*** fsasm has quit IRC | 11:09 | |
*** proteusguy has quit IRC | 11:20 | |
pepijndevos_ | ehhhhh, something is messed up | 11:24 |
pepijndevos_ | The upper bits of my counter just synthesize to xxxx | 11:25 |
*** proteusguy has joined #yosys | 11:29 | |
pepijndevos_ | ZirconiumX, why did you use the 74HC688_1x1EQ8 for equality but 74HC85_1x1CMP4 for gt/lt? How much did you test this? Output seems pretty wrong. Have to do some actual exam work now, will look another time. | 11:39 |
pepijndevos_ | Oh nvm, the 8 bit does *onl* eq, the 4 bit has more outputs | 11:40 |
ZirconiumX | pepijndevos_: Because the '688 is an 8-bit equality comparator, while the '85 is 4-bit, but also does greater-than/less-than | 11:40 |
pepijndevos_ | cool | 11:40 |
pepijndevos_ | I read the datasheet title and they both said magnitude comparator. | 11:40 |
pepijndevos_ | Seems like for my 8 bit word, only 1 4 bit comparator gets generated :/ | 11:41 |
ZirconiumX | pepijndevos_: ABC is pretty good at optimising equality operations, so I don't actually use it | 11:41 |
ZirconiumX | Use the '688 | 11:41 |
ZirconiumX | Bleh, you can figure out what I meant | 11:41 |
pepijndevos_ | right | 11:42 |
pepijndevos_ | ZirconiumX, ahhhh, I think WIDTH is incorrect? Y_WIDTH is always 1. Can you do something like max(A_WIDTH, B_WIDTH)? I'll have to think about how to handle uneven lenghts... | 11:47 |
pepijndevos_ | (what does this magic $pos line do) | 11:48 |
ZirconiumX | Upconverts a smaller signal into a bigger signal | 11:48 |
ZirconiumX | pepijndevos_: try this patch https://pastebin.com/av1VyJsD | 11:50 |
tpb | Title: [Diff] diff --git a/74_cmp.v b/74_cmp.v index 63c463a..5bd17c9 100644 --- a/74_cmp.v - Pastebin.com (at pastebin.com) | 11:50 |
pepijndevos_ | Ah, so that handles when A_WIDTH != B_WIDTH | 11:50 |
ZirconiumX | Yep | 11:51 |
*** adjtm_ has quit IRC | 11:52 | |
pepijndevos_ | ZirconiumX, Definitely an improvement, but it appears only to look at one bit of the counter https://imgur.com/a/J4H6BKU | 11:54 |
tpb | Title: Imgur: The magic of the Internet (at imgur.com) | 11:54 |
pepijndevos_ | unless I understand the syntax in the block wrong | 11:55 |
pepijndevos_ | ahhh, I think I know | 11:55 |
pepijndevos_ | Need to replace Y_Width with max_width in a few places | 11:56 |
ZirconiumX | Yeah | 11:56 |
ZirconiumX | Though I managed to produce a bug in Yosys | 11:56 |
ZirconiumX | I think? | 11:56 |
ZirconiumX | daveshah: should https://pastebin.com/EyCKPmka be reported as a bug? | 11:57 |
tpb | Title: ERROR: Found error in internal cell \axilxbar.$lt$../benchmarks/axilxbar.v:1435$ - Pastebin.com (at pastebin.com) | 11:57 |
daveshah | This is almost certainly a problem with how you are using `$pos` | 11:58 |
daveshah | Yosys has various checks to make sure the contract of its internal (dollar-prefixed) cell types aren't violated | 11:58 |
ZirconiumX | Ah, I see | 11:59 |
* pepijndevos_ has no idea what's going on with $pos at all | 11:59 | |
daveshah | `$pos` just does with conversion, with sign extension if applicable otherwise zero extension | 12:00 |
daveshah | *width conversion | 12:00 |
daveshah | https://github.com/YosysHQ/yosys/blob/master/techlibs/common/simlib.v#L63-L87 | 12:01 |
tpb | Title: yosys/simlib.v at master · YosysHQ/yosys · GitHub (at github.com) | 12:01 |
pepijndevos_ | Ah, fixed it | 12:02 |
*** citypw has quit IRC | 12:03 | |
ZirconiumX | pepijndevos_: https://pastebin.com/0uPeKGCb <--- this probably looks like your patch | 12:04 |
tpb | Title: diff --git a/74_cmp.v b/74_cmp.v index 63c463a..19020d8 100644 --- a/74_cmp.v - Pastebin.com (at pastebin.com) | 12:04 |
pepijndevos_ | exactly :) | 12:05 |
pepijndevos_ | PWM with my reset changes would be less than 10 chips now!! | 12:05 |
pepijndevos_ | So question is... which parts should be used? Comparison definitely makes my example a lot smaller. | 12:08 |
pepijndevos_ | At least I don't think I'll need to make a PR for my changed to cmp as yours are identical :) | 12:09 |
*** cr1901_modern has quit IRC | 12:10 | |
pepijndevos_ | Probably worth looking closer at equality to see why it's not as efficient. My guess is a lot of 1-bit comparisons that use a full chip. | 12:11 |
pepijndevos_ | Ok, I should really start studying. Looking forward to pull everything together after my exam tomorrow. | 12:12 |
ZirconiumX | pepijndevos_: As I mentioned, it's because ABC is much better at optimising equality tests | 12:19 |
*** rrika has quit IRC | 12:30 | |
*** rrika has joined #yosys | 12:32 | |
*** citypw has joined #yosys | 12:40 | |
*** kraiskil has quit IRC | 12:42 | |
*** citypw has quit IRC | 12:43 | |
*** citypw has joined #yosys | 12:44 | |
pepijndevos_ | ZirconiumX, can't be much more efficient than a single chip, right? Or you mean optimizing all stuff around them? Yesterday you had some idea about variables being much more costly than constants, which seems to be the case. Can detect that and fail the techpass? | 12:46 |
ZirconiumX | pepijndevos_: Yes, it can be more efficient than a single chip | 12:46 |
ZirconiumX | Single bit equality tests can be XOR gates, which you can fit four in a chip | 12:47 |
pepijndevos_ | Right. So the trick is to gate the techpass for wide comparisons (on variables)? | 12:48 |
ZirconiumX | Which I try to do | 12:48 |
pepijndevos_ | Hrm... | 12:48 |
pepijndevos_ | Oh yea, I see... and what about the variable part? I only see a fail on width, but no idea if we can even access than info. | 12:50 |
ZirconiumX | We can, I believe | 12:50 |
ZirconiumX | I think techmap sets CONSTMSK | 12:50 |
ZirconiumX | But I'll go check | 12:50 |
pepijndevos_ | Oh sweet | 12:51 |
ZirconiumX | Yeah, there's _TECHMAP_CONSTMSK_ | 12:52 |
*** citypw has quit IRC | 12:52 | |
pepijndevos_ | (as obvious to everyone, running cadence through double X11 forwarding and a VPN is not fun at all) | 12:52 |
*** kraiskil has joined #yosys | 12:57 | |
*** citypw has joined #yosys | 12:59 | |
*** adjtm has joined #yosys | 13:09 | |
*** rohitksingh_work has quit IRC | 13:14 | |
*** citypw has quit IRC | 13:27 | |
*** citypw has joined #yosys | 13:28 | |
*** pie_ has joined #yosys | 14:00 | |
pepijndevos_ | ZirconiumX, I'm trying something like wire _TECHMAP_FAIL_ = (A_WIDTH <= 6 && B_WIDTH <= 6) || _TECHMAP_CONSTMSK_A_ == 0 || _TECHMAP_CONSTMSK_B_ == 0; which always fails it seems. | 14:11 |
*** rohitksingh has joined #yosys | 14:15 | |
ZirconiumX | pepijndevos_: What are you using as your benchmark? | 14:21 |
pepijndevos_ | ZirconiumX, various processors. Picorv32 and VexRiscv at the moment. | 14:23 |
pepijndevos_ | But I'm not 100% convinced I got my parameters and conditions right. Verilog seems to be very loose with its types, VHDL would kill you if you compared a bitmask to a number like that. | 14:24 |
tnt | pepijndevos_: numbers in verilog are 32 bits unsigned IIRC. | 14:25 |
pepijndevos_ | So uuh, is there an equivalent to {any <= '0'} or something like that? Like, whatever this is, tell me if it's all zeros. | 14:26 |
tnt | == 0 ? | 14:27 |
pepijndevos_ | Ok great | 14:28 |
tnt | you could also use assign is_x_zero = ~|x; | 14:28 |
pepijndevos_ | whoa, that's a funky operator. | 14:29 |
tnt | ~ is NOT |x ORs all the bits of x together. | 14:29 |
pepijndevos_ | lol, nice. Do all unary bitwise operators work like that? | 14:30 |
tnt | yeh you can ^x or &x ... | 14:30 |
pepijndevos_ | sweet | 14:31 |
pepijndevos_ | ZirconiumX, I think I got it sorta working. | 14:36 |
*** vonnieda_ has quit IRC | 14:37 | |
pepijndevos_ | It uses exactly one EQ8 in both VexRiscv and Picorv32, but it actually improves chip count at least. | 14:37 |
*** vonnieda has joined #yosys | 14:54 | |
pepijndevos_ | Ok, *another* PR sent. Studying is going well today XD (I'm running simulations in the background) | 15:00 |
*** maikmerten has joined #yosys | 15:22 | |
*** Stary has quit IRC | 15:23 | |
*** zignig is now known as zignig_bedtime | 15:28 | |
*** emeb has joined #yosys | 15:29 | |
*** emeb has quit IRC | 16:23 | |
*** rohitksingh has quit IRC | 16:30 | |
*** m4ssi has quit IRC | 16:31 | |
*** rohitksingh has joined #yosys | 16:46 | |
*** rohitksingh has quit IRC | 17:28 | |
*** rohitksingh has joined #yosys | 17:30 | |
*** srk has quit IRC | 18:02 | |
*** phantomcircuit has quit IRC | 18:02 | |
*** Jybz has quit IRC | 18:02 | |
*** Jybz has joined #yosys | 18:02 | |
*** srk has joined #yosys | 18:03 | |
*** phantomcircuit has joined #yosys | 18:04 | |
*** rrika has quit IRC | 18:06 | |
*** rrika has joined #yosys | 18:07 | |
*** fsasm has joined #yosys | 18:18 | |
*** Stary has joined #yosys | 18:39 | |
*** dys has joined #yosys | 19:00 | |
* ZirconiumX pokes pepijndevos_ | 19:27 | |
*** rohitksingh has quit IRC | 19:47 | |
pepijndevos_ | ZirconiumX, eh? | 19:55 |
pepijndevos_ | Oh, stuff has been merged. Cool :) | 19:56 |
pepijndevos_ | ZirconiumX, I just pushed an update to the kicad branch that lets me compile pwm256.v to 5 chips and get them in KiCad. | 19:57 |
pepijndevos_ | oh derp, I'm an idiot... how does this even work haha | 19:58 |
*** kraiskil has quit IRC | 20:01 | |
pepijndevos_ | I'm thinking that if things work out, I could make an actual PCB over the weekend. | 20:08 |
pepijndevos_ | That would be so cool | 20:08 |
ZirconiumX | Yeah, it would | 20:10 |
ZirconiumX | Put my name on there somewhere, too, would ya? | 20:10 |
pepijndevos_ | Would you like ZirconiumX, Dan Ravensloft, or something else? (send me SVG? haha) | 20:11 |
pepijndevos_ | Also, I'm starting to think that if you'd write a RiscV with 74xx in mind, it would be waaaay less chips. | 20:12 |
*** Max-P has quit IRC | 20:14 | |
*** Max-P has joined #yosys | 20:15 | |
*** kraiskil has joined #yosys | 20:16 | |
pepijndevos_ | I wonder if I can modify the pwm to fade in and out and synth to 10 or less chips. Then I just have to add a clock and LED to make a breathing LED. | 20:19 |
*** fsasm has quit IRC | 20:39 | |
*** maikmerten has quit IRC | 20:39 | |
*** fsasm has joined #yosys | 20:39 | |
ZirconiumX | pepijndevos_: ZirconiumX is fine | 20:54 |
*** kraiskil has quit IRC | 21:22 | |
*** emeb has joined #yosys | 21:30 | |
*** benreynwar has joined #yosys | 21:46 | |
benreynwar | Hi all! I'm playing with symbiyosys for the first time. Is it normal that "Writing trace to VCD file: engine_0/trace.vcd" can take over an hour for large designs? Running the BMC only took 2 minutes since it failed at step 7 but I haven't managed to actually get a failing trace yet. | 22:05 |
ZipCPU | benreynwar: Wow! Not sure I've ever tried SymbiYosys on a design where it took that long to write a VCD file | 22:14 |
ZipCPU | In general, I'd advice running on a smaller design if possible | 22:14 |
ZipCPU | Still, that's a new one for me | 22:14 |
benreynwar | zipcpu: Yeah! I started off with a small submodule yesterday and it all went smoothly, so today I thought I'd try the top level :). | 22:16 |
ZipCPU | Ahm ... how big is this top level design? | 22:16 |
* ZipCPU has never applied formal to an entire design | 22:17 | |
ZipCPU | Normally, I break a design up into smaller pieces to formally verify it | 22:19 |
benreynwar | I've set all the generics to small values so that it'd only take a couple of thousand LUTs on an FPGA. | 22:19 |
ZipCPU | Well ... I have applied formal to a couple thousand LUTs before ... | 22:19 |
ZipCPU | One of the crossbars I applied formal to required nearly 3k iCE40 LUTs | 22:20 |
ZipCPU | benreynwar: Can I try your design myself? See if I have the same problem? | 22:21 |
benreynwar | It's a work project, so I'm afraid I can't share the code :(. | 22:22 |
ZipCPU | I can understand | 22:22 |
ZipCPU | Symbiotic EDA does sell support contracts | 22:23 |
benreynwar | Yeah, I should look into that. I'm using the trial license at the moment (the design is in VHDL) and am trying to get a feel of how useful formal is for our designs. | 22:26 |
ZipCPU | So, what I normally do ... I normally verify all of the "leaf modules" within the design | 22:27 |
ZipCPU | That is, I verify any/all of the bus masters and bus slaves | 22:27 |
ZipCPU | Separable components if you will | 22:27 |
ZipCPU | I then simulate the rest | 22:27 |
ZipCPU | I'm just now getting to the point where I can formally verify an interconnect--I just haven't tried my formally verified interconnect within any of my designs | 22:28 |
benreynwar | I wonder if the fact that it's in VHDL could be affecting the trace dumping. | 22:28 |
ZipCPU | Wow ... I hadn't thought of that | 22:28 |
ZipCPU | Is it spilling information to a file during all this time? Can you use "trace -f" to see where it's at? | 22:28 |
*** Jybz has quit IRC | 22:30 | |
benreynwar | The header of the trace.vcd gets written where all the signals are defined gets written, but none of the content. The logfile.txt in the engine_0 folder is empty. | 22:30 |
benreynwar | The small design I worked on yesterday worked without any problems though. | 22:30 |
ZipCPU | What solver are you using? | 22:31 |
benreynwar | I think your suggestion of working on the submodules is the right direction to go. Then if it is a problem with the VHDL I should see the same issue in one of the submodules. | 22:31 |
benreynwar | smtbmc boolector | 22:31 |
ZipCPU | Thanks ... that doesn't help though, since I haven't had any problems with boolector | 22:32 |
ZipCPU | I have had problems with some of the non-smt solvers, but boolector has been one of my mainstay's | 22:32 |
*** fsasm has quit IRC | 22:35 | |
benreynwar | So I'm going to leave this process running in the background to see if it ever writes than trace file, but move onto testing the submodules individually. As always, thanks for all your help! | 22:36 |
ZipCPU | I just wish I could've helped more, and perhaps even solved your problem | 22:36 |
*** vonnieda has quit IRC | 22:55 | |
*** s_frit has quit IRC | 23:02 | |
*** s_frit has joined #yosys | 23:02 |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!