| *** tpb has joined #yosys | 00:00 | |
| Postmanmods | Its. The. WORST! | 00:00 |
|---|---|---|
| ZipCPU | Nah, it's not nearly that bad ... but you need to learn the ways of the formal methods | 00:00 |
| Postmanmods | So I have been only dealing in Lattice thus far. Which FPGA would you say is the best in general? | 00:00 |
| Postmanmods | Or your preferred? | 00:01 |
| ZipCPU | That's a hard question | 00:01 |
| Postmanmods | I know, different pros and cons, but what is your go to? | 00:01 |
| ZipCPU | I tend to prefer Digilent as a source for my boards. They tend to be well documented. That puts me often in the Xilinx camp. The problem is ... the open source tools don't work with Xilinx (much) yet | 00:01 |
| ZipCPU | So I've got a bunch of iCE40 and ECP5 boards on my desk that I'm working with as well | 00:01 |
| ZipCPU | They aren't nearly as well documented as the Xilinx ones are--or if they are I haven't found the key documents (yet) | 00:02 |
| Postmanmods | Oh hang, I need your opinion on a dev cyclone board (if its worth the $$ or not) | 00:02 |
| ZipCPU | I only have one cyclone board, the DE-10 Nano | 00:03 |
| Postmanmods | http://www.terasic.com.tw/cgi-bin/page/archive.pl?Language=English&CategoryNo=167&No=1046 | 00:03 |
| tpb | Title: Terasic - All FPGA Main Boards - Cyclone V - DE10-Nano Kit (at www.terasic.com.tw) | 00:03 |
| ZipCPU | I do have a max-1000 board as well | 00:03 |
| Postmanmods | OH | 00:03 |
| Postmanmods | THAT SOLVES THAT LOL | 00:03 |
| Postmanmods | The link is to a DE10 | 00:03 |
| ZipCPU | I wrote about my experiences with the DE10-nano on the blog | 00:03 |
| Postmanmods | No way | 00:04 |
| Postmanmods | Thats a weird coincidence... | 00:04 |
| ZipCPU | ;) | 00:04 |
| Postmanmods | woah | 00:04 |
| ZipCPU | Not really ... I've done a *lot* of writing | 00:04 |
| Postmanmods | I highly appreciate the effort in this | 00:04 |
| ZipCPU | Thanks! | 00:04 |
| ZipCPU | The blog has lots of good stuff on it | 00:05 |
| Postmanmods | It's extremely well put together, I really dig the learning method. Resonates with me, ya now? | 00:05 |
| ZipCPU | That's my argument | 00:05 |
| ZipCPU | Here's my thesis: Verilog design needs to be taught hand-in-hand with how to work with a good simulator (Verilator) and formal tools. Without those, you'll end up like so many students at the end of a semester with a design that sort-of works | 00:06 |
| Postmanmods | Hmmm... Haven't gotten that far yet. Verilator simulates the ckt? | 00:07 |
| ZipCPU | Technically Verilator just converts Verilog to C++ | 00:07 |
| ZipCPU | You can then use that for simulation. Supposedly (I haven't done the measurements) it's at least as good as if not better (i.e. faster) than the big vendor simulators | 00:07 |
| Postmanmods | *Insert shocked pikachu meme here* | 00:08 |
| ZipCPU | The other really cool thing about Verilator is that it's easy to integrate into your desktop environment | 00:08 |
| Postmanmods | Genuine question: do they just not care about the software usability that much or what? | 00:08 |
| ZipCPU | There's more to the story | 00:09 |
| Postmanmods | The design is just... Blech. | 00:09 |
| ZipCPU | For example, the Verilog spec says designs need to support 0, 1, x, and z. Verilator only supports 0 and 1 | 00:10 |
| ZipCPU | By only supporting 0 and 1, it makes it easier to be faster than the vendor sims | 00:10 |
| ZipCPU | That's the big thing as I recall | 00:11 |
| Postmanmods | How... Did they overlook that? | 00:11 |
| Postmanmods | Wat | 00:11 |
| Postmanmods | Just goes to show that simpler solutions are typically a good route. | 00:12 |
| ZipCPU | Yes | 00:12 |
| Postmanmods | Have learned that the hard way. Many many times. | 00:12 |
| Postmanmods | So uh | 00:27 |
| Postmanmods | I think I just programmed the NVCM with no lattice hardware programmer | 00:27 |
| ZipCPU | Is that a good thing? | 00:27 |
| Postmanmods | Not sure yet. At least I didnt spend $180 bucks on Lattice's! | 00:28 |
| Postmanmods | Just thought it was cool that you can use any off the shelf FT2232 with the diamond programmer software without having to buy expensive firmware. | 00:29 |
| Postmanmods | expensive hardware* | 00:30 |
| ZipCPU | Yeah ... that's how I managed to program my Max-1000. The expensive software didn't work, the open source software did | 00:30 |
| Postmanmods | My story with yosys, it's what brought me here! | 00:31 |
| ZipCPU | You have a max-1000 board? | 00:31 |
| Postmanmods | Oh no I meant the lattice software wasn't working but yosys did. | 00:32 |
| ZipCPU | Oh, yeah | 00:32 |
| *** emeb_mac has joined #yosys | 00:41 | |
| *** vonnieda has joined #yosys | 00:53 | |
| ZipCPU | Postmanmods: Do you do twitter at all? | 01:07 |
| Postmanmods | Do not, but I do have an instagram! | 01:08 |
| Postmanmods | I should probably get a twitter... | 01:08 |
| ZipCPU | I would've invited you to join my twitter feed. There's been a lot of fun information there | 01:08 |
| Postmanmods | @postmanmods on instagram if you are curious. | 01:08 |
| * ZipCPU doesn't do instragram :/ | 01:08 | |
| Postmanmods | Ah dang. I should probably just use twitter, seems to be more useful. | 01:09 |
| ZipCPU | I'm trying to keep a formal verification quiz going every Friday for anyone who wants to participate | 01:09 |
| ZipCPU | Not quite sure what this weeks quiz will be (yet) though | 01:10 |
| Postmanmods | Count me in! Is it at a certain time? | 01:11 |
| ZipCPU | It's a tweet | 01:12 |
| Postmanmods | Thats does it, I'm making a twitter. | 01:12 |
| ZipCPU | If you want to see some of the quizes I've done so far, check out the last section of: http://zipcpu.com/tutorial/class-verilog.pdf | 01:12 |
| ZipCPU | Be aware ... you might see questions (and answers) there that I haven't (yet) asked ... ;) | 01:13 |
| Postmanmods | Ha, I have that pdf open in the next tab! I was taking a gander at it. | 01:13 |
| ZipCPU | So I try to tweet the quiz on a Friday, and the answer to it on a Monday | 01:13 |
| ZipCPU | Anyone who wants to try to answer it in between is welcome to it | 01:14 |
| ZipCPU | I've promised not to be sarcastic on really wild guesses, but sometimes I do need to bite my tongue ;) | 01:14 |
| ZipCPU | "Why is the sky blue"? "Because ducks have four legs" just doesn't make sense. | 01:14 |
| ZipCPU | Some of the answers I've gotten have been just that crazy too ... but in general the quizzes are fun | 01:18 |
| Postmanmods | Just made a twitter and followed ya, I'll keep a lookout for the quiz. | 01:23 |
| ZipCPU | Look forward to you seeing you around! | 01:26 |
| Postmanmods | Same to you! When I actually have money I am definitely subscribing to your patreon. It'll be worth every penny. | 01:28 |
| ZipCPU | "When I actually have money" ... Lol! I've been saying that to myself for years too | 01:28 |
| ZipCPU | Sure, though, enjoy! | 01:28 |
| *** Cerpin has quit IRC | 01:29 | |
| *** emeb has quit IRC | 01:45 | |
| *** gsi__ has joined #yosys | 02:13 | |
| *** gsi_ has quit IRC | 02:16 | |
| *** thasti has quit IRC | 02:32 | |
| *** PyroPeter has quit IRC | 02:53 | |
| *** jevinskie has joined #yosys | 02:54 | |
| *** PyroPeter has joined #yosys | 03:06 | |
| *** jevinskie has quit IRC | 03:44 | |
| *** Cerpin has joined #yosys | 03:58 | |
| *** jevinskie has joined #yosys | 04:08 | |
| *** rohitksingh has joined #yosys | 04:34 | |
| *** rohitksingh has quit IRC | 04:39 | |
| *** _whitelogger has quit IRC | 04:50 | |
| *** _whitelogger has joined #yosys | 04:52 | |
| *** rohitksingh has joined #yosys | 05:16 | |
| *** rohitksingh has quit IRC | 05:22 | |
| *** rohitksingh_work has joined #yosys | 05:36 | |
| *** futarisIRCcloud has quit IRC | 06:10 | |
| *** rohitksingh has joined #yosys | 06:13 | |
| *** rohitksingh has quit IRC | 06:30 | |
| *** jevinski_ has joined #yosys | 06:52 | |
| *** jevinskie has quit IRC | 06:53 | |
| *** emeb_mac has quit IRC | 07:06 | |
| *** futarisIRCcloud has joined #yosys | 07:16 | |
| *** rohitksingh has joined #yosys | 07:36 | |
| *** rohitksingh has quit IRC | 07:46 | |
| *** attie has joined #yosys | 08:06 | |
| *** mjacob has quit IRC | 08:10 | |
| *** vid has joined #yosys | 08:29 | |
| *** m4ssi has joined #yosys | 08:45 | |
| *** fsasm has joined #yosys | 09:03 | |
| *** vid has quit IRC | 09:14 | |
| *** futarisIRCcloud has quit IRC | 09:30 | |
| *** futarisIRCcloud has joined #yosys | 09:56 | |
| *** rohitksingh has joined #yosys | 09:57 | |
| *** vid has joined #yosys | 11:04 | |
| *** jit10 has joined #yosys | 11:35 | |
| *** futarisIRCcloud has quit IRC | 12:05 | |
| *** rohitksingh has quit IRC | 12:40 | |
| *** rohitksingh_work has quit IRC | 12:56 | |
| *** vid has quit IRC | 13:23 | |
| *** vonnieda has quit IRC | 13:58 | |
| *** rohitksingh has joined #yosys | 14:07 | |
| *** vonnieda has joined #yosys | 14:15 | |
| *** emeb has joined #yosys | 14:43 | |
| *** Ultrasauce has quit IRC | 15:41 | |
| *** vid has joined #yosys | 15:44 | |
| *** rohitksingh has quit IRC | 15:46 | |
| *** vid has quit IRC | 16:00 | |
| *** m4ssi has quit IRC | 16:12 | |
| *** rohitksingh has joined #yosys | 16:16 | |
| *** gnufan_home has joined #yosys | 16:22 | |
| *** MoeIcenowy has quit IRC | 16:32 | |
| *** MoeIcenowy has joined #yosys | 16:32 | |
| *** voxadam has quit IRC | 16:40 | |
| *** voxadam has joined #yosys | 16:40 | |
| *** jevinski_ has quit IRC | 17:06 | |
| *** jevinskie has joined #yosys | 17:09 | |
| ZirconiumX | This is entirely the wrong channel for this, and I apologise, but ZipCPU, I think your ISA blog post is buggy. | 17:18 |
| ZipCPU | ISA post? Which one was that? | 17:18 |
| ZirconiumX | https://zipcpu.com/zipcpu/2018/01/01/zipcpu-isa.html | 17:19 |
| tpb | Title: A Quick Introduction to the ZipCPU Instruction Set (at zipcpu.com) | 17:19 |
| ZipCPU | Ahh, okay, what problem have you found? | 17:19 |
| ZirconiumX | You do comparisons through subtraction and setting flags from the result, right? | 17:20 |
| ZipCPU | That's one of many ways, yes ... go on | 17:20 |
| ZipCPU | Many of the instructions set flags, though, not just the comparison and test instructions, and not just through subtraction. But go on. If there's a bug, I'd like to fix it. | 17:21 |
| ZirconiumX | But if you take a signed byte of minimum value (0x80 AKA -128) and subtract a byte of maximum value (0x7F AKA +127), you get +1. | 17:23 |
| ZirconiumX | Which doesn't set the negative flag | 17:24 |
| ZirconiumX | So -128 is greater than +127 | 17:24 |
| ZirconiumX | Assuming I've understood this correctly | 17:24 |
| *** Ultrasauce has joined #yosys | 17:25 | |
| ZirconiumX | If not, maybe it could use clarification anyway | 17:25 |
| ZipCPU | You are assuming 8-bit values to simplify things, right? Since the ZipCPU only operates on 32-bit values. But I think I'm getting your point | 17:25 |
| ZirconiumX | Yes, I am | 17:25 |
| ZipCPU | I've been through this through several rounds of getting this right, and I think I have it right (now) | 17:25 |
| ZipCPU | If you do an A-B subtraction, the negation flag is set to more than just the high order bit | 17:26 |
| ZipCPU | It's the high order bit exclusively or'd to the overflow bit if I recall correctly | 17:26 |
| * ZipCPU pulls up the code to remind himself | 17:26 | |
| ZirconiumX | Yeah, that would work | 17:26 |
| ZirconiumX | Because you want LT/GE to check that N == V/N != V, I think | 17:27 |
| ZipCPU | Here it is: https://github.com/ZipCPU/zipcpu/blob/master/rtl/core/cpuops.v#L177-L179 | 17:28 |
| tpb | Title: zipcpu/cpuops.v at master · ZipCPU/zipcpu · GitHub (at github.com) | 17:28 |
| ZipCPU | You have the problem on ADDs as well as CMPs and SUBs | 17:29 |
| ZirconiumX | I realise it's a "quick introduction", but I found it a little confusing | 17:29 |
| ZipCPU | Here' an addition example: 0x80 + 0x80 (i.e. -128 + -128) = 00 (with overflow). The sign bit should be negative in this case as well. | 17:29 |
| ZipCPU | Let see what I said in the ALU article ... | 17:30 |
| ZipCPU | Yeah, it's discussed here: http://zipcpu.com/zipcpu/2017/08/11/simple-alu.html | 17:30 |
| tpb | Title: A Simple ALU, drawn from the ZipCPU (at zipcpu.com) | 17:30 |
| ZipCPU | The penultimate section is devoted to flag calculation | 17:31 |
| ZirconiumX | I will admit to finding your work on formal methods interesting, ZipCPU, but pretty far beyond me | 17:32 |
| ZipCPU | Really? That's a shame. Would you like some simple examples to experiment with? | 17:33 |
| ZirconiumX | I can give examples of properties I would like to prove, but I have no idea how to go about proving them. For example, in chess, pieces can't wrap around the chessboard. | 17:33 |
| ZipCPU | That one's easy. Add a bit to the position on the chess board, and then do your comparisons | 17:34 |
| ZirconiumX | But despite my course in predicate logic, I have no idea how to formalise that one. | 17:34 |
| ZirconiumX | Yeah, I've wrote a chess program, so it's something I've had to solve through brute force | 17:34 |
| ZipCPU | if (piece == ROOK) assert((ROOK.x - $past(ROOK.x)==1)||(ROOK.x-$past(ROOK.x)==-1)); assert(ROOK.x[4] == 0); | 17:35 |
| ZipCPU | You could also do, assert(PIECE.x[4] == 0); assert(PIECE.y[4] == 0); | 17:36 |
| ZirconiumX | But it gets progressively more difficult, at least in the software world | 17:38 |
| ZirconiumX | I tried to formalise my chess program | 17:38 |
| ZipCPU | Well, yeah, that's sort of the nature of formal. The more properties you add, the more challenging things get. | 17:38 |
| ZipCPU | Formally verifying software is often harder than formally verifying hardware components | 17:39 |
| ZipCPU | At least with hardware components, the size of the state space is fairly well bounded | 17:39 |
| ZirconiumX | The main thing for me is that the solver often goes "I don't know how to solve this" without any more hints | 17:41 |
| ZipCPU | So, with SymbiYosys, you can often find bugs even if the solver can't fully prove the core | 17:42 |
| ZipCPU | Indeed, formally proving a core for all time takes ... some intrusive work into the internal structure of the core in question | 17:42 |
| ZipCPU | Perhaps a story would help | 17:42 |
| ZipCPU | I've been working on formally verifying an AXI interconnect. This has been quite the challenge for me, and it's now (mostly) verified | 17:43 |
| ZipCPU | Then, someone handed me their own AXI interconnect to verify. The code within it was ... computer generated, and not necessarily easy or obvious to understand | 17:43 |
| ZipCPU | Instead of trying to verify that core for all time, I was able to find several bugs that would take place in the first 20 timesteps | 17:43 |
| ZipCPU | It's not a perfect proof, but it was enough to find some bugs | 17:44 |
| ZipCPU | If your experience is with software formal verification, I'd encourage you to look again. You can often do much better with hardware verification--the state of the art matches there better. | 17:46 |
| ZirconiumX | Thank you, I think I will | 17:57 |
| ZipCPU | ;) | 17:57 |
| ZirconiumX | Though writing in Verilog trips me up a little, I think | 17:57 |
| ZipCPU | Have you found verilator -Wall or `default_nettype none yet? | 17:58 |
| ZipCPU | Those two simple things find a *lot* of the Verilog issues for me | 17:58 |
| ZirconiumX | I have, and Yosys catches some things too | 17:58 |
| ZipCPU | It sure does | 17:58 |
| tnt | I actually find yosys pretty tolerant to "invalid" things. | 17:59 |
| tnt | (i.e. things not in the standard that verilator or iverilog choke on) | 17:59 |
| ZirconiumX | Which is why I have a """lint""" pass which runs optimisations on my code, and then spits it back out as Verilog. If I'm doing something dumb the optimiser generally turns the code to garbage | 18:00 |
| ZirconiumX | Probably not the smartest idea, but hey, I'm someone who stares at the output of their compiler | 18:03 |
| *** rohitksingh has quit IRC | 18:34 | |
| *** rohitksingh has joined #yosys | 18:40 | |
| *** maikmerten has joined #yosys | 18:57 | |
| maikmerten | seems Lattice needed to produce another batch of HX8K eval boards. The board I received last year has date codes from 2019, the one I received today seems to have a first week 2019 marking. | 19:00 |
| maikmerten | err... the one I received last year has date codes from *2013* | 19:01 |
| maikmerten | the FPGA device also now has Lattice markings, the jumpers are white - and look hand-soldered :-) | 19:01 |
| tnt | Ah yeah, I think my first dev board was still marked Silicon Blue :) | 19:04 |
| *** fsasm has quit IRC | 19:05 | |
| maikmerten | yup - the board I received last year (from Mouser) also has those old markings. The FPGA has a date code "1230", so week 30 of 2012 | 19:05 |
| maikmerten | seems they had nice big batch produced in 2013 which lasted for years on some distribution channels | 19:06 |
| maikmerten | (wow, the LT3030 LDO is a ~7$ part. Seems pretty expensive for two voltages at 750 and 250 mA) | 19:13 |
| tnt | it's a fancy ldo :) | 19:40 |
| tnt | Mmm .... I was giving formal a quick try, I figured I'd test a simple fifo I wrote. But looking athe examples in https://github.com/ZipCPU/wbuart32/blob/master/rtl/ufifo.v for instance, but I don't really see how it checks what I'd really expect from a FIFO ... i.e. what goes in, comes out in the same order ... | 19:43 |
| tpb | Title: wbuart32/ufifo.v at master · ZipCPU/wbuart32 · GitHub (at github.com) | 19:43 |
| ZipCPU | tnt: Let me suggest a different example for you | 19:44 |
| ZipCPU | http://zipcpu.com/tutorial , lesson 10 | 19:44 |
| tpb | Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com) | 19:44 |
| ZipCPU | The ufifo proof is one of my earlier ones, and as you've pointed out, it's not nearly as complete as some of my other ones | 19:45 |
| *** jevinskie has quit IRC | 19:47 | |
| *** proteusguy has quit IRC | 20:04 | |
| *** Jybz has joined #yosys | 20:12 | |
| *** rohitksingh has quit IRC | 20:38 | |
| *** maikmerten has quit IRC | 20:38 | |
| tnt | ZipCPU: mm, trying to replicate the same for my code, but so far I get 'PASS' even when trying to assert on obviously false property. | 20:40 |
| tnt | but at least that example match more what I'd expect tx. | 20:40 |
| ZipCPU | Are you working on a FIFO? | 20:40 |
| ZipCPU | Are you assert()ing outputs and local state, while assume()ing any inputs? | 20:41 |
| tnt | ZipCPU: https://pastebin.com/PRZucVXj | 20:42 |
| tpb | Title: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - Pastebin.com (at pastebin.com) | 20:42 |
| tnt | "assert((f_used > 0) == rd_empty);" this should obviously be false. | 20:42 |
| ZipCPU | Lines 131 and 132 belong in always blocks | 20:43 |
| * ZipCPU is still looking | 20:43 | |
| tnt | ok, I guess the 'assert' is also in a always. | 20:45 |
| ZipCPU | Did you get the cover traces? | 20:45 |
| ZipCPU | Yes, the free version of yosys only supports "immediate" assertions. "immediate" assertions must be in always blocks | 20:45 |
| tnt | No, it's not generating any vcd | 20:45 |
| ZipCPU | Are you using SymbiYosys? | 20:45 |
| tnt | yup, pretty much copied the .sby from your example. | 20:46 |
| tnt | https://pastebin.com/LZCrpgRD | 20:46 |
| tpb | Title: [tasks] prf cvr [options] prf: mode prove prf: depth 5 cvr: mode cover cvr: dep - Pastebin.com (at pastebin.com) | 20:46 |
| ZipCPU | Are you sure you want assign f_empty == (f_used != 8'h00)? Shouldn't it be "f_empty == (f_used == 8'h00)"? | 20:47 |
| tnt | Doh ... yeah, obviousy ... | 20:47 |
| tnt | didn't really change anything though | 20:48 |
| ZipCPU | Did it create two directories? | 20:48 |
| tnt | How does it know to generate a clk/rst ? | 20:48 |
| tnt | yes fifo_sync_shift_prf / fifo_sync_shift_cvr | 20:48 |
| ZipCPU | The clock is automatic, you need to generate the reset | 20:49 |
| tnt | same as when I run your example, except with yours I get a vcd . | 20:49 |
| ZipCPU | You should find traces in the fifo_sync_shift_*/engine_0/ directories | 20:49 |
| ZipCPU | If they aren't there, then check the fifo_sync_shift_*/logfile.txt files | 20:49 |
| tnt | nope, no traces | 20:49 |
| tnt | ## 0:00:00 Solver: yices | 20:49 |
| tnt | ## 0:00:00 Status: PASSED | 20:49 |
| ZipCPU | Which file was that one from? | 20:50 |
| tnt | cover | 20:50 |
| tnt | fifo_sync_shift_cvr/engine_0/logfile.txt | 20:50 |
| ZipCPU | And yet no traces in fifo_sync_shift_cvr/engine_0/ ? | 20:50 |
| tnt | https://pastebin.com/V4HG5RUt | 20:51 |
| tpb | Title: tnt@rei /tmp/formal/fifo $ cat fifo_sync_shift_prf/engine_0/logfile_* ## 0:00 - Pastebin.com (at pastebin.com) | 20:51 |
| tnt | nope only the logfile | 20:51 |
| ZipCPU | So, in the *_prf/ directory, no traces could mean that everything is working | 20:51 |
| ZipCPU | In the *_cvr/ directory, no traces and PASS means that SymbiYosys didn't find any cover statements in your file | 20:52 |
| ZipCPU | Can you post the logfile from the *_cvr directory? | 20:52 |
| tnt | that's the 2 lines I posted above | 20:52 |
| ZipCPU | Ok, time to roll up our sleeves. There should be a log file in *_*/model/design.log | 20:53 |
| tnt | oh, you meant not the engine one. https://pastebin.com/VzwGAFzf | 20:53 |
| tpb | Title: SBY 22:44:46 [fifo_sync_shift_prf] Removing direcory 'fifo_sync_shift_prf'. SBY - Pastebin.com (at pastebin.com) | 20:53 |
| ZipCPU | Hmm ... yeah, that means it didn't find any cover statements in your design, so it ended quickly | 20:54 |
| ZipCPU | Found the bug | 20:54 |
| ZipCPU | You need an ifdef FORMAL not FORMAT | 20:54 |
| tnt | ... | 20:54 |
| * tnt hides | 20:54 | |
| ZipCPU | (We've all done it) | 20:54 |
| * ZipCPU looks for sweets to coax tnt out of hiding | 20:55 | |
| *** emeb_mac has joined #yosys | 20:55 | |
| tnt | now it indeed fails :) (like expected) | 20:55 |
| ZipCPU | Yaaayy!!! | 20:56 |
| ZipCPU | Makes more sense, now, huh? ;) | 20:56 |
| tnt | yup. Now I probably need to generate a proper reset | 20:59 |
| ZipCPU | initial assume(i_reset); often works | 20:59 |
| tnt | indeed, thanks. | 21:00 |
| tnt | it passes coverage now. | 21:00 |
| ZipCPU | Nice | 21:00 |
| dormando | is "logic design adn verification using systemverilog (revised)" as good as it sounds? looks like yosys supports a decent chunk of it | 21:02 |
| dormando | all my verilog knowledge is based off super old materials | 21:02 |
| ZipCPU | The free version of Yosys only supports some SV features. There's a commercial version that supports SV+VHDL+Verilog | 21:03 |
| dormando | pretty sure I don't need the full stack. | 21:03 |
| dormando | trying to arm myself a bit better for my next project, but reading material is hard to find. half of it are your blog posts :) | 21:07 |
| ZipCPU | Thanks for the compliments! | 21:07 |
| dormando | it's been a big help. wrote a fifo loosely based off your post for my last one | 21:08 |
| ZipCPU | Is there something particular you are looking for that I might help you find? | 21:08 |
| dormando | not really sure. I come from a background of "new language? read the spec!" but there's a huge variance within the tooling for fpga-land | 21:08 |
| * ZipCPU sighs heavily | 21:09 | |
| ZipCPU | That's one of the things I like about using Yosys. You can go from yosys to just about any back end | 21:09 |
| dormando | and I haven't come to an understanding how different authors end up with their coding style. I landed in one that's explicit enough to me, but it feels like the style is tooling dependent too | 21:09 |
| dormando | ie: how well the backend can decide to use FF's instead of latches, some convert *'s that can be shifts into shift's automatically, and so on | 21:10 |
| ZipCPU | Have you seen my article about minimizing LUTs? That accounts for at least some of my coding style | 21:10 |
| ZipCPU | FF's and latches though ... that's easy | 21:10 |
| dormando | I may have but haven't read it yet? Culling LUT's is where I'll be starting next. I might have to hack a script to get nextpnr to visualize modules for me :) | 21:11 |
| ZipCPU | If you set anything on the posedge of a clock, always @(posedge i_clk) a <= b; // it'll use a FF | 21:11 |
| dormando | cool. so how do you... find that knowledge in the first place? or the rules around it? | 21:11 |
| ZipCPU | Typically, latches are *bad*. Therefore you'll want to avoid them. That's easily done by making sure that any time you set something in an always @(*) block, you make sure it gets set a value other than it's current one | 21:11 |
| * ZipCPU sits back | 21:12 | |
| dormando | Yeah. so I aggressively destroy latches | 21:12 |
| ZipCPU | I got schooled by Clifford when my stuff didn't work | 21:12 |
| ZipCPU | ;D | 21:12 |
| dormando | but I've tried to match some coding style to some of those who don't set much in combinatorial blocks | 21:12 |
| dormando | and inevitably I stumbled on some combination of things that degraded into a latch (in ISE) | 21:12 |
| ZipCPU | There's another way to avoid latches: use an always_comb @(*) block | 21:13 |
| dormando | so I'm not sure how much of that is solved by just using yosys or the newer xilinx tooling | 21:13 |
| dormando | always_comb is systemverilog right? | 21:13 |
| ZipCPU | Yosys supports it | 21:13 |
| dormando | right. | 21:13 |
| ZipCPU | It also supports (IIRC) always_latch and always_ff | 21:13 |
| dormando | it does | 21:13 |
| dormando | this book I was asking about goes over these extensions. I wasn't finding much online :) | 21:14 |
| dormando | I'm like dang, I really wish I had these months ago, haha | 21:14 |
| ZipCPU | You should be able to find an SV spec on line. It's not much, but it might help | 21:14 |
| ZipCPU | I did write a Verilog tutorial, but I'm not sure I went into that much depth | 21:14 |
| dormando | Yeah I found it. it doesn't do much for style tho. | 21:14 |
| ZipCPU | http://zipcpu.com/tutorial | 21:14 |
| tpb | Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com) | 21:14 |
| ZipCPU | Try this, it might help (some): http://zipcpu.com/blog/2017/06/12/minimizing-luts.html | 21:15 |
| tpb | Title: Minimizing FPGA Resource Utilization (at zipcpu.com) | 21:15 |
| dormando | like golang has this huge page on what makes good golang style.. and (sorry I forgot his name) in verilog land has that huge paper on doing cross-domain clock stuff | 21:15 |
| dormando | the specs need to be paired with more of those kinds of papers for people to really grok style | 21:15 |
| ZipCPU | Ooohh, first rule: avoid cross-domain clocks like the plague | 21:15 |
| ZipCPU | http://zipcpu.com/blog/2017/08/21/rules-for-newbies.html | 21:15 |
| tpb | Title: Rules for new FPGA designers (at zipcpu.com) | 21:15 |
| ZipCPU | There's a time for them, but they aren't easy to work with--so I avoid them to the extent that I can | 21:16 |
| dormando | haha. | 21:16 |
| dormando | Yeah. I had a blast learning how to use them. | 21:16 |
| dormando | think your blogs were in that process too | 21:16 |
| ZipCPU | Glad I could help ;) | 21:16 |
| dormando | I got my raycasting engine up to 20+ FPS at 320x240 on a tinfyga BX by cranking the SPI clock to 150mhz | 21:16 |
| dormando | but rest of the design is still 16mhz | 21:16 |
| dormando | it runs faster than an actual 386 would've run wolf3d | 21:17 |
| ZipCPU | :) | 21:17 |
| dormando | anyway sorry for the spam. appreciate the tips. | 21:17 |
| ZipCPU | :D | 21:18 |
| tnt | :/ "it might start processing from an unreachable state you aren’t expecting." ... | 21:18 |
| tnt | arf | 21:18 |
| ZipCPU | dormando: Let me know if there's something you are looking for, stuck with, or something I might help you find | 21:18 |
| dormando | my next trick is porting the DOOM rendering engine to arduino + lp8k, so I need to cut LUT's down and improve testing | 21:18 |
| ZipCPU | tnt: Yep! | 21:18 |
| ZipCPU | You can fix that by adding assertions to prevent it from starting there | 21:18 |
| dormando | but at the start of every project I also go hunting for new material to help with coding style.. so I'm not really sure what questions to ask yet | 21:18 |
| ZipCPU | tnt: Remember: assume inputs, assert local state and outputs | 21:19 |
| ZipCPU | dormando: You must learn the ways of formal :D | 21:19 |
| dormando | I at very least need automated testing :) I miss "make test" so much | 21:19 |
| dormando | verilator looks cool | 21:20 |
| tnt | ZipCPU: I was kind of hoping this would be more "black box" than this. | 21:20 |
| ZipCPU | dormando: http://zipcpu.com/zipcpu/2018/12/20/sby-makefile.html | 21:20 |
| tpb | Title: Makefiles for formal proofs with SymbiYosys (at zipcpu.com) | 21:20 |
| ZipCPU | tnt: Only BMC is black box. Formal in general is *very* white box | 21:20 |
| tnt | (so I could change completely the underlying implementation and just check external properties) | 21:20 |
| dormando | perfect :) | 21:20 |
| ZipCPU | tnt: There is some ability to do that | 21:21 |
| ZipCPU | *some* | 21:21 |
| *** gnufan_home has quit IRC | 21:31 | |
| tnt | \o/ it passed the induction step now. | 21:39 |
| daveshah | IC3 solvers like abc pdr are truly "black box" | 21:40 |
| daveshah | But they tend to suffer from combinational explosion more | 21:40 |
| ZipCPU | daveshah: They also seem to be quite limited in their capability | 21:40 |
| ZipCPU | You said it | 21:41 |
| daveshah | And unlike smt they don't support memories | 21:41 |
| daveshah | So those have to be blasted to logic first, not helping things performance wise either | 21:41 |
| ZipCPU | tnt: o/ | 21:41 |
| tnt | atm the only property I'm checking is my empty flag, so it's not a super strong proof of validity :p | 21:43 |
| ZipCPU | Yes, but consider how much work it takes to get hello world running. You've finally passed that threshold it seems. | 21:44 |
| tnt | Some properties I'm not sure yet how to express. like "if there is no data, empty should be 1" that's easy. But if there is a least one data, empty should fall _eventually_ (but not at the next cycle, that could be implementation dependent) | 21:47 |
| ZipCPU | Not necessarily | 21:48 |
| ZipCPU | You might have a FIFO that never fully empties | 21:48 |
| ZipCPU | So what you want to state is not that empty must fall, but rather that it is able to fall | 21:48 |
| ZipCPU | Consider line 169 here: https://pastebin.com/PRZucVXj | 21:49 |
| tpb | Title: [VeriLog] /* * fifo_sync_shift.v * * vim: ts=4 sw=4 * * Copyright (C) 2019 Sylvain M - Pastebin.com (at pastebin.com) | 21:49 |
| ZipCPU | That proves that it is possible to empty the FIFO after it has been full | 21:49 |
| tnt | yes, possible. | 21:51 |
| tnt | but I was more thinking of the case where you push 1 single word and empty stays asserted for instance. | 21:52 |
| ZipCPU | You mean, verify that after pushing a word empty falls? | 21:52 |
| tnt | yes. | 21:52 |
| tnt | but not at the next cycle ... pipeline delays could make it happens 1,2,3,... cycles later. | 21:53 |
| tnt | (not in this implementation obviously but in general for a fifo) | 21:53 |
| *** Jybz has quit IRC | 21:55 | |
| ZipCPU | So ... consider that the crossbar I've been working on is similar | 21:58 |
| ZipCPU | Requests can be made by any of the bus masters, and then forwarded to the slaves | 21:58 |
| ZipCPU | In the middle, there are a couple of stages of pipeline processing ... waiting for an channel grant, and a couple of skid buffers | 21:59 |
| ZipCPU | I can verify that the slave has the right counts (ignoring the interconnect), and I can verify that the master does | 21:59 |
| ZipCPU | To handle the interconnect, I assume a functioning slave and a functioning master, and then have to prove that they are each driven properly | 22:00 |
| ZipCPU | That includes correlating the transaction counters in my formal property set between the masters and the slaves, so I have to account for every piece of data transiting through the pipeline in this task | 22:00 |
| tnt | heh, yeah, that's a couple of difficulty notch above :p | 22:02 |
| ZipCPU | It's not really all that much more difficult than managing a bunch of counters | 22:06 |
| tnt | ZipCPU: anyway, time to sleep. Thanks for your help ! | 22:15 |
| ZipCPU | ;) Sleep well | 22:15 |
| *** vonnieda has quit IRC | 22:43 | |
| *** emeb has quit IRC | 23:19 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!