| *** tpb has joined #yosys | 00:00 | |
| *** rqou has quit IRC | 00:07 | |
| *** rqou has joined #yosys | 00:07 | |
| *** sorear has quit IRC | 00:17 | |
| *** sorear has joined #yosys | 00:19 | |
| *** _whitelogger has quit IRC | 00:42 | |
| *** _whitelogger has joined #yosys | 00:44 | |
| *** emeb_mac has quit IRC | 01:15 | |
| *** GoldRin has joined #yosys | 02:10 | |
| *** PyroPeter has quit IRC | 02:22 | |
| *** PyroPeter has joined #yosys | 02:36 | |
| *** hca has quit IRC | 03:22 | |
| *** AlexDaniel has quit IRC | 03:48 | |
| *** emeb_mac has joined #yosys | 04:01 | |
| *** dys has joined #yosys | 06:12 | |
| *** _whitelogger has quit IRC | 06:48 | |
| *** _whitelogger has joined #yosys | 06:50 | |
| *** emeb_mac has quit IRC | 07:13 | |
| *** dys has quit IRC | 07:31 | |
| *** _whitelogger has quit IRC | 08:48 | |
| *** _whitelogger has joined #yosys | 08:50 | |
| *** Laksen has joined #yosys | 10:09 | |
| *** _whitelogger has quit IRC | 11:51 | |
| *** _whitelogger has joined #yosys | 11:53 | |
| *** proteusguy has quit IRC | 13:52 | |
| *** proteusguy has joined #yosys | 13:54 | |
| *** lutsabound has joined #yosys | 13:58 | |
| *** citypw has joined #yosys | 14:07 | |
| *** citypw has quit IRC | 14:16 | |
| pepijndevos | How does yosys represent x in sigspec? | 14:26 |
|---|---|---|
| pepijndevos | There is a constructor that just takes an unsigned int, and ones that take various other representations. | 14:28 |
| daveshah | pepijndevos: you want SigSpec(RTLIL::State bit, int width = 1); | 14:30 |
| daveshah | With State::Sx | 14:30 |
| pepijndevos | daveshah, oooh, thanks. And if I want a vector of them? | 14:33 |
| pepijndevos | Seems I can make it into a const and use that? | 14:33 |
| daveshah | If they aren't all Sx, you probably want to use RTLIL::Const | 14:34 |
| daveshah | Yup | 14:34 |
| pepijndevos | fancy fancy | 14:35 |
| pepijndevos | How can I break on a log_assert? | 15:10 |
| pepijndevos | ERROR: Assert `is_fully_const() && GetSize(chunks_) <= 1' failed in kernel/rtlil.cc: | 15:10 |
| pepijndevos | 3720 | 15:10 |
| pepijndevos | I'm a bit perplexed how it can be not fully const when I just created it from a constant | 15:11 |
| pepijndevos | ohhhh I see... it's from something else | 15:13 |
| pepijndevos | oh no! | 15:15 |
| pepijndevos | Seems in yosys an adff takes a constant reset and in this case the reset value is not actually constant | 15:15 |
| pepijndevos | Would I have to do a dff+mux instead? | 15:19 |
| daveshah | Yosys doesn't have a first class primitive for a non constant *async* reset value | 15:21 |
| daveshah | A dff+mux would be the way to go for a *sync* non constant reset value | 15:21 |
| daveshah | But that wouldn't involve an adff in any case | 15:22 |
| daveshah | If you want a non constant async reset value then you'll need to use a dffsr and some steering logic | 15:22 |
| pepijndevos | Oh shit... | 15:22 |
| pepijndevos | So an Adff is an asynch d flip flop with a reset value? | 15:23 |
| daveshah | Yes, a dff with a constant async reset value | 15:24 |
| daveshah | A dffsr is a dff with both an async set and reset | 15:25 |
| daveshah | Not that most FPGAs that Yosys supports don't support such a primitive | 15:25 |
| *** emeb has joined #yosys | 15:26 | |
| pepijndevos | If I use sync reset it's fine. Asynch reset with non-constant reset value is such an edge case I'll ignore it for now. | 15:29 |
| daveshah | Sounds good | 15:31 |
| pepijndevos | Maybe I should add a nice error message though. I see log_assert being used, but that doesn't have a message. Do I just do if() log_error? | 15:34 |
| daveshah | Basically, but if you have a filename and line number you should use log_file_error not log_error | 15:37 |
| pepijndevos | Ah, hmmm, so it'll tell the user which line... lemme check. | 15:39 |
| daveshah | Yeah, it's generally preferred for frontend errors | 15:40 |
| *** rohitksingh has joined #yosys | 16:54 | |
| GenTooMan | Anyone know of an IDE that will work with Icarus and Yosys? I happen to be use to Eclipse but I don't expect anything their as Eclipse is SO Java centered it's hard to get a decent plugin for anything other than Java. | 17:01 |
| *** lutsabound has quit IRC | 17:17 | |
| ZirconiumX | GenTooMan: I think you expect too much of the Verilog tooling and ecosystem | 17:24 |
| *** rohitksingh has quit IRC | 17:35 | |
| *** bwidawsk has quit IRC | 18:00 | |
| *** bwidawsk has joined #yosys | 18:01 | |
| pepijndevos | How does one use symbiyosys with vhdl? | 18:07 |
| daveshah | I'm assuming you want to know behaviour in the commercial suite (SES). VHDL asserts are supported but at present there is no support for assumes | 18:10 |
| daveshah | They would have to be in a Verilog module (possibly using bind) | 18:10 |
| pepijndevos | I don't even know the difference between assert and assume yet. But yea, SES. | 18:42 |
| pepijndevos | Does VHDL have stuff like (* anyconst *)? | 18:46 |
| daveshah | It has attributes, yes | 18:48 |
| *** Laksen has quit IRC | 18:49 | |
| pepijndevos | Eh, so can you do useful stuff without assume, or do you practually have to write your testbenches in verilog? | 19:02 |
| daveshah | You pretty much need assume | 19:06 |
| pepijndevos | Alright, sad, but maybe I'll learn some actual verilog on the way... | 19:08 |
| ZirconiumX | What does SES provide over FOSS Yosys? Verific parser support, commercial support; what else? Out of pure curiosity. | 19:09 |
| daveshah | Verific and support are the main things, but also some things like extra formal verification IP for verifying things like AXI cores | 19:10 |
| daveshah | Plus everything is prebuilt in a distribution-independent way | 19:11 |
| ZirconiumX | That's fair enough. Presumably the money goes towards paying Clifford et al. | 19:12 |
| daveshah | Yes | 19:15 |
| daveshah | FYI, there are free licenses for OSHW/non-commercial research, see the bottom of https://www.symbioticeda.com/seda-suite | 19:17 |
| *** mithro has quit IRC | 19:44 | |
| *** mithro has joined #yosys | 19:45 | |
| pepijndevos | I am so confused... | 20:11 |
| pepijndevos | Can I see a trace if the thing passed? | 20:23 |
| daveshah | There is no trace if the thing passed | 20:24 |
| ZipCPU | Unless you run cover | 20:24 |
| daveshah | This is true | 20:25 |
| ZipCPU | Using cover() you can get traces from when things pass | 20:25 |
| pepijndevos | How do I tell the thing to start in reset? | 20:25 |
| daveshah | Although it is important to remember that when FV passes, the solver has checked every possible path through the design | 20:25 |
| ZipCPU | You should be able to do: initial assume(i_reset); | 20:25 |
| ZipCPU | However, Verific doesn't support "initial" assumes or asserts (yet) | 20:25 |
| ZipCPU | An alternative would be to do something like: initial f_past_valid = 0; always @(posedge i_clk) f_past_valid <= 1; always @(*) if (!f_past_valid) assume(i_reset); | 20:26 |
| pepijndevos | Ehhhh, that's so ugly I wonder if I'm taking the wrong approach? | 20:27 |
| ZipCPU | The "right" answer here is to "fix" Verific. | 20:28 |
| ZipCPU | You could also write for the block with the assumption: assume property (@(posedge i_clk) !f_past_valid |-> i_reset); | 20:29 |
| daveshah | In general you need the f_past_valid for other stuff anyway, so it's not as bad is it looks | 20:30 |
| daveshah | Something I've thought would be fun would be a small Yosys pass that creates this logic automatically, just given the name of your reset port/signal | 20:31 |
| pepijndevos | Okay, I think I passed my first assertion... but without a trace how do I know it even left reset... | 20:31 |
| ZipCPU | daveshah: Yes. Clifford and I discussed this sort of thing last week | 20:32 |
| ZipCPU | I asked for an "asic" option that would throw out initial statements, assume an initial reset, and only check assertions on the next clock cycle | 20:32 |
| daveshah | You could also have something that automatically does the f_past_valid stuff whenever it sees $past etc | 20:33 |
| ZipCPU | We both agreed we *should* have an option like that, but the more we discussed it the more difficult the details turned out to be | 20:33 |
| daveshah | Ah | 20:33 |
| daveshah | pepijndevos: as ZipCPU says, this is where you probably want to use cover | 20:34 |
| ZipCPU | Yosys once had an option for generating a trace automatically. It might even still be there. The problem I found with that option was that the trace was typically quite irrelevant | 20:35 |
| pepijndevos | I see... but he also said you don't use them at the same time, so do you write two testbenches? | 20:35 |
| ZipCPU | No--you place cover() statements side by side with your assert()/assume() statements | 20:35 |
| ZipCPU | Then you run the tool twice--once in either bmc or prove mode, and once in cover mode | 20:35 |
| pepijndevos | ah | 20:36 |
| pepijndevos | So do you need to have two sby files? or can you have multiple modes? | 20:36 |
| ZipCPU | You can have multiple modes in the same sby file | 20:37 |
| pepijndevos | hm ok | 20:37 |
| ZipCPU | To do that, you need a [tasks] section--I typically place it at the top | 20:37 |
| pepijndevos | oh ok | 20:37 |
| ZipCPU | I also typically place two tasks under neath it. All the tasks have names you assign, but I like to pick "prf" and "cvr" | 20:37 |
| ZipCPU | Then on any line to be executed in prove mode, I prefix it with "prf:" | 20:37 |
| pepijndevos | ah I see | 20:38 |
| pepijndevos | https://symbiyosys.readthedocs.io/en/latest/reference.html | 20:38 |
| ZipCPU | Any line to be executed in cover mode gets prefixed with "cvr" | 20:38 |
| tpb | Title: Reference for .sby file format SymbiYosys 0.1 documentation (at symbiyosys.readthedocs.io) | 20:38 |
| ZipCPU | Ah, yeah, that's it | 20:38 |
| ZipCPU | pepijndevos: Here's an example from when verifying Xilinx's AXI-lite core: https://github.com/ZipCPU/wb2axip/blob/master/bench/formal/xlnxdemo.sby | 20:40 |
| tpb | Title: wb2axip/xlnxdemo.sby at master · ZipCPU/wb2axip · GitHub (at github.com) | 20:40 |
| ZipCPU | You can find the core itself here, https://github.com/ZipCPU/wb2axip/blob/master/bench/formal/xlnxdemo.v | 20:41 |
| tpb | Title: wb2axip/xlnxdemo.v at master · ZipCPU/wb2axip · GitHub (at github.com) | 20:41 |
| ZipCPU | And my report on the bugs I found here: http://zipcpu.com/formal/2018/12/28/axilite.html | 20:42 |
| tpb | Title: Using a formal property file to verify an AXI-lite peripheral (at zipcpu.com) | 20:42 |
| ZipCPU | pepijndevos: Have you found my course notes for using Symbiotic EDA Suite to verify VHDL designs? | 20:43 |
| pepijndevos | ZipCPU, eh no, I have not. | 20:45 |
| ZipCPU | Look for the link to the VHDL slides on this page: https://zipcpu.com/tutorial/ | 20:46 |
| tpb | Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com) | 20:46 |
| ZipCPU | You should there find the course notes for the VHDL course, as well as several examples to work through | 20:46 |
| pepijndevos | Bookmarked. I can't think straigt anymore. I added an assertion and the output looks fine to me but apparently it's a failure. | 20:47 |
| ZipCPU | Did your assertion use $past()? | 20:48 |
| pepijndevos | no | 20:48 |
| ZipCPU | Care to post it somewhere, so I can take a look? | 20:49 |
| pepijndevos | It's just virtually the same as the previous one except it's a different opcode. | 20:49 |
| * ZipCPU looks for the "previous one" ... | 20:49 | |
| pepijndevos | t | 20:49 |
| pepijndevos | hold on | 20:49 |
| pepijndevos | lemme add the remaining asserts so I can commit something sane | 20:50 |
| ZipCPU | Don't tell anyone, but I typically browse several forums each morning just looking for code I can try the formal tools on | 20:51 |
| ZipCPU | So .... debugging the code of others is something I tend to enjoy | 20:51 |
| pepijndevos | does binary and have any footnukes? | 20:51 |
| ZipCPU | ? | 20:52 |
| pepijndevos | I'll show you, ready to commit, just need to make a github repo. | 20:53 |
| pepijndevos | Uhg... quick, give me a name for a bit serial CPU haha | 20:53 |
| ZipCPU | footnuke-and-fiance-free ? | 20:54 |
| pepijndevos | ZipCPU, https://github.com/pepijndevos/seqpu | 20:55 |
| tpb | Title: GitHub - pepijndevos/seqpu: A bit-serial CPU (at github.com) | 20:55 |
| *** emeb_mac has joined #yosys | 20:56 | |
| ZipCPU | Cloned! | 20:56 |
| pepijndevos | Other advice on useful properties to test and stupid things I'm doing of course very welcome | 20:57 |
| ZipCPU | :D | 20:57 |
| ZipCPU | Okay, so how about: cover property (@(posedge i_clk) opcode == 3'b000 ##1 ); | 20:59 |
| ZipCPU | Hmm ... that reset might get in the way | 20:59 |
| ZipCPU | How about: cover property (@(posedge i_clk) disable iff !rst; opcode == 3'b000 ##1 ); | 20:59 |
| pepijndevos | What does that do? | 21:01 |
| ZipCPU | So an assert() does anything it can to make the expression within false, a cover() is the opposite | 21:01 |
| ZipCPU | A cover statement will do anything to make the expression within the cover statement tru | 21:01 |
| pepijndevos | Right, so it'd just set the opcode to 000? | 21:02 |
| ZipCPU | (opcode == 3'b000) is a test for a clock cycle where thee opcode is 000 | 21:02 |
| ZipCPU | ##1 means go to the next clock cycle | 21:02 |
| ZipCPU | So the result would be a trace showing the opcode == 3'b000 on one cycle, but not ending 'til at least the next | 21:02 |
| ZipCPU | Further, the disable iff statement makes it so that it will have to pick a time when the reset value is low | 21:02 |
| ZipCPU | Err ... high in your case, since your resets are all using negative logic | 21:03 |
| ZipCPU | It'd be sort of like: always @(posedge i_clk) cover(initial_reset && $past(opcode != 3'b000) && $past(rst) && rst); | 21:03 |
| pepijndevos | It's bedtime for me, but my sleepy brain just doesn't get what it shows that opcode is 0, because it's just an input. | 21:04 |
| ZipCPU | No, sleepy brain probably gets | 21:04 |
| ZipCPU | gets it | 21:04 |
| ZipCPU | We can discuss more tomorrow if you'd like | 21:04 |
| pepijndevos | Gladly | 21:04 |
| pepijndevos | Have a nice day :) | 21:05 |
| ZipCPU | o/ | 21:05 |
| pepijndevos | Last thought: In the whole CPU it would very much make sense to verify that the opcode can't change mid-instruction XD | 21:05 |
| *** emeb_mac has quit IRC | 21:06 | |
| ZipCPU | Absolutely! | 21:08 |
| ZipCPU | Quoted from online: "I cannot understand your code because I learnt [sic] VHDL only". Poor guy. Even before I learned (some) VHDL (thanks daveshah!) I could still understand most of it. | 21:14 |
| *** bwidawsk has quit IRC | 21:17 | |
| *** bwidawsk has joined #yosys | 21:21 | |
| *** emeb has quit IRC | 22:21 | |
| *** Stroboko1p has quit IRC | 23:31 | |
Generated by irclog2html.py 2.13.1 by Marius Gedminas - find it at mg.pov.lt!