Monday, 2019-06-24

*** tpb has joined #yosys00:00
*** svenn has quit IRC00:00
*** svenn has joined #yosys00:01
*** weatherhead has joined #yosys00:29
ZipCPUZirconiumX: What's the struggle?  Anything I can help explain?00:30
*** weatherhead has quit IRC00:39
*** weatherhead has joined #yosys00:41
*** gsi__ has joined #yosys00:58
*** ktemkin has quit IRC01:00
*** ktemkin has joined #yosys01:00
*** tannewt has quit IRC01:00
*** ZipCPU has quit IRC01:00
*** gsi_ has quit IRC01:01
*** ZipCPU has joined #yosys01:01
*** tannewt has joined #yosys01:02
*** citypw has joined #yosys02:39
*** citypw has quit IRC02:45
*** PyroPeter has quit IRC02:49
*** PyroPeter has joined #yosys03:02
*** azonenberg_mobil has joined #yosys03:24
*** proteusguy has quit IRC04:32
ZirconiumXZipCPU: 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 IRC04:32
ZirconiumXBut 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
ZirconiumXFor 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
sorearZirconiumX: have you read through riscv-formal?04:43
ZirconiumXI have, yes04:43
*** proteusguy has joined #yosys04:47
sorearI thnk the same methodology could be applied to sh?04:48
ZirconiumXSure, but first I need to grok the methodology04:49
ZirconiumXI was given my rough task for the summer: I need to run a 256 byte Dreamcast demo.04:49
ZirconiumXIt's only 34 instructions04:50
sorear1. 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
sorear2. 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 wrote04:51
ZirconiumXBut some of those instructions include fun things like IEEE 754 division .-.04:51
sorear3. forward progress: in any N cycle period, at least one instruction is retired04:51
ZirconiumXOkay, that makes sense04:53
sorearfood for thought:
tpbTitle: riscv-formal/ at master · SymbioticEDA/riscv-formal · GitHub (at
sorearverifying a FPU is a bit different from verifying a pipeline04:57
sorearpipelines are extremely complicated but have relatively few actual state bits and sparse coupling between them, so model checkers work well04: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 with04:58
ZirconiumXIt doesn't help that 754 arithmetic is perhaps a little vague; you don't have to be accurate, just accurate enough.05:00
sorearyou said "division" though, division is required to be correctly rounded05:02
sorearthere'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 allowed05:03
soreareven if it weren't, you have a goal of giving the same results as sh4 and sh4 hopefully documents what it does05:04
sorear"accurate enough" is for functions like sin()05:05
* sorear stares at FPSCR.PR05:08
*** rohitksingh_work has joined #yosys05:14
*** rohitksingh has joined #yosys05:49
*** emeb_mac has quit IRC06:14
*** tecepe_ has joined #yosys06:16
*** edmoore_ has joined #yosys06:16
*** elms_ has joined #yosys06:16
*** thoughtpolice_ has joined #yosys06:17
*** pepijndevos_ has joined #yosys06:23
*** sorear has quit IRC06:24
*** flaviusb has quit IRC06:24
*** edmoore has quit IRC06:24
*** elms has quit IRC06:24
*** tecepe has quit IRC06:24
*** thoughtpolice has quit IRC06:24
*** pepijndevos has quit IRC06:24
*** edmoore_ is now known as edmoore06:24
*** tecepe_ is now known as tecepe06:24
*** elms_ is now known as elms06:24
*** thoughtpolice_ is now known as thoughtpolice06:24
*** sorear has joined #yosys06:29
*** flaviusb has joined #yosys06:30
*** dys has quit IRC06:55
*** jakobwenzel has joined #yosys07:10
*** rohitksingh has quit IRC07:37
*** m4ssi has joined #yosys08:04
*** rohitksingh has joined #yosys08:20
*** azonenberg_mobil has quit IRC08:39
*** vup has quit IRC08:54
*** vup has joined #yosys08:54
*** rqou has quit IRC09:27
*** rohitksingh_work has quit IRC09:59
*** rohitksingh_work has joined #yosys10:01
*** rohitksingh has quit IRC10:04
*** rohitksingh has joined #yosys10:05
*** alexhw has joined #yosys10:17
*** rqou has joined #yosys10:23
*** rohitksingh_work has quit IRC10:44
*** rohitksingh_work has joined #yosys10:45
*** rohitksingh has quit IRC10:46
*** Kitlith has quit IRC10:49
*** Kitlith has joined #yosys10:53
*** nurelin_ has quit IRC10:55
*** nurelin_ has joined #yosys10:55
*** GoldRin has joined #yosys11:07
*** proteusguy has quit IRC11:57
*** GoldRin has quit IRC12:15
*** proteusguy has joined #yosys12: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 parts12:49
ZirconiumXpepijndevos_: I did look at part availability; AC is still manufactured by TI and ON Semi12:50
ZirconiumXAnd for KiCad, remember that 74 series parts are *mostly* pin compatible12:50
ZirconiumXThough they don't have the AC11 series12:50
pepijndevos_Yea... I figured I could probably get away with any of the variations they might have.12:51
ZirconiumXAnd AC11 is pretty important12:51
pepijndevos_AC11 is the 16 bit stuff?12:51
ZirconiumXNo, that's AC1612:51
ZirconiumXAC11 is an alternative layout that puts VCC and GND in the middle of the chip12:51
pepijndevos_... why is that important?12:52
pepijndevos_Speed and ground bounce and stuff?12:52
ZirconiumXGround bounce, yeah12:52
ZirconiumXHaving VCC and GND in the corners of the chip means that for gates on the opposite sides of the pins have longer voltage path12:53
ZirconiumXAdd that to the very fast switching time of AC logic, and you end up with something that can bounce while switching12: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
ZirconiumXMaking KiCad libraries is easy12:56
ZirconiumXGetting them merged is harder12: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 backlog12:59
pepijndevos_I found skidl, which can programmatically make netlists, saving me a lot of trouble.13:00
ZirconiumXMorning, ZipCPU13:00
ZipCPUI remember when I verified a pipelined CPU (my own), I was concerned that instructions would be dropped or duplicated as they went through the pipeline13:03
ZipCPUSince then, I've added another worry: that the pipeline doesn't get stuck13:03
ZipCPUThe CPU pipeline logic was complex enough as it is/was so these were important criteria for me13:04
ZipCPUAs for the reset, have you thought of: if ($past(i_reset)) assert(issue_instruction_request && request_address == RESET_ADDRESS); ?13:04
ZirconiumXI have not, no13:06
ZipCPUHere's another one: if ($past(i_reset)) assert(pipeline_stage_is_valid == 0);13:07
ZipCPUOr, ... if ($past(pipeline_stage_advances)) assert(pipeline_stage_data == $past(previous_pipeline_stage_data || pipeline_stage_valid == 0);13:08
ZipCPUSince the ZipCPU has multiple pipeline stages, I did that for each13:09
pepijndevos_sigh, no 74xx16xxx parts either...13:09
ZipCPUOr, here's another: if ($past(pipeline_stage_valid)) assert($stable(pipeline_stage_data) || next_pipeline_stage_has_the_new_data);13:10
ZirconiumXHuh, that's interesting13:13
ZirconiumXsorear will be pleased to know that me and $employer have agreed on me having to implement only a subset of SH413:13
ZirconiumXUnfortunately this subset is still fairly complex13:14
ZirconiumXZipCPU: I get the feeling your general philosophy is to build the pipeline and then prove it correct, rather than worry about that as you go13:14
ZipCPUPerhaps because I had the pipeline already built when I discovered formal13:15
ZipCPUWere I to do it again, I might start with something closer to riscv-formal13:15
ZipCPUThat's a nice end-to-end approach, vs my own which was more internals based13:15
sorearRoughly what’s the subset?13:19
*** rohitksingh_work has quit IRC13:19
ZirconiumXsorear: 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 divide13:23
ZirconiumXPlus sine/cosine approximation13:24
ZirconiumX <-- anything in this block which has an sh4impl13:24
tpbTitle: fpgadc/main.cpp at master · emudev-org/fpgadc · GitHub (at
sorearsh4 has sine/cosine? I only have a document for sh2a13:24
ZirconiumXsorear: it's an approximation, but yeah13:25
tpbTitle: Hardware Docs - Dreamcast (at
* ZirconiumX whistles innocently13:25
sorearwhat significant things does that *exclude*? the MMU?13:25
ZirconiumXMMU, the concept of instruction privilege, and quite a lot of the status registers13:26
ZirconiumXZipCPU: When should you use a bounded model check and when should you use induction?13:35
ZipCPUA bounded model check can find assertion failures, and can often be done with basic "white-box" testing approaches13:36
ZipCPUInduction can prove that there are no assertion failures within a design ... ever, but it's a much more intrusive "white-box" approach13:37
ZipCPUSorry, BMC is "black box" not white box13:38
* ZipCPU looks for the editing button on IRC, to edit his prior comment13:38
ZipCPUI tend to do everything via induction if possible, but ... it's not always possible13:38
*** vonnieda has quit IRC13:56
*** rohitksingh has joined #yosys14:05
*** emeb has joined #yosys14:07
*** vonnieda has joined #yosys14:10
*** maikmerten has joined #yosys14: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 IRC15:11
*** gsi__ is now known as gsi_15:15
ZirconiumXpepijndevos_: That must be a typo; I meant the 37415:25
*** rohitksingh has quit IRC15: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
ZirconiumXpepijndevos_: Google FreeRouting15:46
ZirconiumXThe KiCad built-in autorouter was terrible, so they binned it15:47
pepijndevos_Yea, from what I can tell freerouting is some old java applet that's been open sourced15:48
pepijndevos_Maybe it's not as bad as it seems...15:49
*** rohitksingh has joined #yosys16:01
*** dys has joined #yosys16:05
pepijndevos_ZirconiumX, OMG, it works
tpbTitle: Verilog to PCB - Album on Imgur (at
ZirconiumXpepijndevos_: Now *you're* using 373s :P16:07
pepijndevos_But uuh, yea, will change that to 374 haha16:08
*** fsasm has joined #yosys16:34
pepijndevos_wat... I no git.17:04
ZirconiumXpepijndevos_: ?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 WIP17:25
ZirconiumXI don't merge PRs17:25
ZirconiumXI rebase17: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 set17:39
maikmertenverilog to PCB... huh? Is that really a thing?17:40
pepijndevos_Almost kinda hahaha17:40
ZipCPUI've heard of it from the standpoint of formal17:40
ZipCPU... as in, formally verify your PCB traces before sending the design out for manufacture17: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 chips17:44
*** rohitksingh has quit IRC17:44
pepijndevos_and I'm currently trying to generate a kicad netlist from it17:44
maikmertenexcellent! :-)17:45
ZirconiumXI'm not crazy17:45
tpbTitle: GitHub - ZirconiumX/74xx-liberty (at
ZirconiumXI think17: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 #yosys17: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
maikmertenhmmm... perhaps something like an IR decoder (e.g. NEC protocol) or a SPI controller?17:52
maikmertensomething 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
tpbTitle: 74xx-liberty/pwm256.v at master · ZirconiumX/74xx-liberty · GitHub (at
pepijndevos_And it uses like 10 different chips, so that might in fact be a good candidate.17:57
maikmertenright. 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
maikmertenI assume you'd need to be very 74xx-minded to get compact results18:01
pepijndevos_Reset? Who needs it...18:04
pepijndevos_ugh... 74xx chips are so complicated... why not do something simple like relay logic18:09
ZirconiumXmaikmerten: It helps that 74xx chips are generally tri-state18:13
ZirconiumXWhich Yosys tends not to handle wel18:14
maikmertenoh, right18:14
ZirconiumXI remember seeing a chip list for the PDP-11/4518:14
ZirconiumXBut I can't find it18:15
*** rohitksingh has quit IRC18:49
*** dys has quit IRC19:45
*** lutsabound has joined #yosys19:55
pepijndevos_ZirconiumX, "Implement the Knight processor in FPGA and then convert into TTL."
tpbTitle: GitHub - oriansj/stage0: A set of minimal dependency bootstrap binaries (at
*** dys has joined #yosys20:25
*** maikmerten has quit IRC20:28
*** adjtm_ has joined #yosys20:44
*** adjtm has quit IRC20:47
*** awordnot has quit IRC21:36
*** nurelin_ has quit IRC21:36
*** awordnot has joined #yosys21:37
*** nurelin_ has joined #yosys21:50
*** lutsabound has quit IRC22:04
*** fsasm has quit IRC22:33
*** vonnieda has quit IRC22:56
*** lutsabound has joined #yosys23:01
*** m_hackerfoo has joined #yosys23:06
*** hackerfoo has joined #yosys23:07

Generated by 2.13.1 by Marius Gedminas - find it at!