Sunday, 2019-07-28

*** tpb has joined #yosys00:00
*** rqou has quit IRC00:07
*** rqou has joined #yosys00:07
*** sorear has quit IRC00:17
*** sorear has joined #yosys00:19
*** _whitelogger has quit IRC00:42
*** _whitelogger has joined #yosys00:44
*** emeb_mac has quit IRC01:15
*** GoldRin has joined #yosys02:10
*** PyroPeter has quit IRC02:22
*** PyroPeter has joined #yosys02:36
*** hca has quit IRC03:22
*** AlexDaniel has quit IRC03:48
*** emeb_mac has joined #yosys04:01
*** dys has joined #yosys06:12
*** _whitelogger has quit IRC06:48
*** _whitelogger has joined #yosys06:50
*** emeb_mac has quit IRC07:13
*** dys has quit IRC07:31
*** _whitelogger has quit IRC08:48
*** _whitelogger has joined #yosys08:50
*** Laksen has joined #yosys10:09
*** _whitelogger has quit IRC11:51
*** _whitelogger has joined #yosys11:53
*** proteusguy has quit IRC13:52
*** proteusguy has joined #yosys13:54
*** lutsabound has joined #yosys13:58
*** citypw has joined #yosys14:07
*** citypw has quit IRC14:16
pepijndevosHow does yosys represent x in sigspec?14:26
pepijndevosThere is a constructor that just takes an unsigned int, and ones that take various other representations.14:28
daveshahpepijndevos: you want SigSpec(RTLIL::State bit, int width = 1);14:30
daveshahWith State::Sx14:30
pepijndevosdaveshah, oooh, thanks. And if I want a vector of them?14:33
pepijndevosSeems I can make it into a const and use that?14:33
daveshahIf they aren't all Sx, you probably want to use RTLIL::Const14:34
pepijndevosfancy fancy14:35
pepijndevosHow can I break on a log_assert?15:10
pepijndevosERROR: Assert `is_fully_const() && GetSize(chunks_) <= 1' failed in kernel/
pepijndevosI'm a bit perplexed how it can be not fully const when I just created it from a constant15:11
pepijndevosohhhh I see... it's from something else15:13
pepijndevosoh no!15:15
pepijndevosSeems in yosys an adff takes a constant reset and in this case the reset value is not actually constant15:15
pepijndevosWould I have to do a dff+mux instead?15:19
daveshahYosys doesn't have a first class primitive for a non constant *async* reset value15:21
daveshahA dff+mux would be the way to go for a *sync* non constant reset value15:21
daveshahBut that wouldn't involve an adff in any case15:22
daveshahIf you want a non constant async reset value then you'll need to use a dffsr and some steering logic15:22
pepijndevosOh shit...15:22
pepijndevosSo an Adff is an asynch d flip flop with a reset value?15:23
daveshahYes, a dff with a constant async reset value15:24
daveshahA dffsr is a dff with both an async set and reset15:25
daveshahNot that most FPGAs that Yosys supports don't support such a primitive15:25
*** emeb has joined #yosys15:26
pepijndevosIf 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
daveshahSounds good15:31
pepijndevosMaybe 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
daveshahBasically, but if you have a filename and line number you should use log_file_error not log_error15:37
pepijndevosAh, hmmm, so it'll tell the user which line... lemme check.15:39
daveshahYeah, it's generally preferred for frontend errors15:40
*** rohitksingh has joined #yosys16:54
GenTooManAnyone 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 IRC17:17
ZirconiumXGenTooMan: I think you expect too much of the Verilog tooling and ecosystem17:24
*** rohitksingh has quit IRC17:35
*** bwidawsk has quit IRC18:00
*** bwidawsk has joined #yosys18:01
pepijndevosHow does one use symbiyosys with vhdl?18:07
daveshahI'm assuming you want to know behaviour in the commercial suite (SES). VHDL asserts are supported but at present there is no support for assumes18:10
daveshahThey would have to be in a Verilog module (possibly using bind)18:10
pepijndevosI don't even know the difference between assert and assume yet. But yea, SES.18:42
pepijndevosDoes VHDL have stuff like (* anyconst *)?18:46
daveshahIt has attributes, yes18:48
*** Laksen has quit IRC18:49
pepijndevosEh, so can you do useful stuff without assume, or do you practually have to write your testbenches in verilog?19:02
daveshahYou pretty much need assume19:06
pepijndevosAlright, sad, but maybe I'll learn some actual verilog on the way...19:08
ZirconiumXWhat does SES provide over FOSS Yosys? Verific parser support, commercial support; what else? Out of pure curiosity.19:09
daveshahVerific and support are the main things, but also some things like extra formal verification IP for verifying things like AXI cores19:10
daveshahPlus everything is prebuilt in a distribution-independent way19:11
ZirconiumXThat's fair enough. Presumably the money goes towards paying Clifford et al.19:12
daveshahFYI, there are free licenses for OSHW/non-commercial research, see the bottom of
*** mithro has quit IRC19:44
*** mithro has joined #yosys19:45
pepijndevosI am so confused...20:11
pepijndevosCan I see a trace if the thing passed?20:23
daveshahThere is no trace if the thing passed20:24
ZipCPUUnless you run cover20:24
daveshahThis is true20:25
ZipCPUUsing cover() you can get traces from when things pass20:25
pepijndevosHow do I tell the thing to start in reset?20:25
daveshahAlthough it is important to remember that when FV passes, the solver has checked every possible path through the design20:25
ZipCPUYou should be able to do: initial assume(i_reset);20:25
ZipCPUHowever, Verific doesn't support "initial" assumes or asserts (yet)20:25
ZipCPUAn 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
pepijndevosEhhhh, that's so ugly I wonder if I'm taking the wrong approach?20:27
ZipCPUThe "right" answer here is to "fix" Verific.20:28
ZipCPUYou could also write for the block with the assumption: assume property (@(posedge i_clk) !f_past_valid |-> i_reset);20:29
daveshahIn general you need the f_past_valid for other stuff anyway, so it's not as bad is it looks20:30
daveshahSomething 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/signal20:31
pepijndevosOkay, I think I passed my first assertion... but without a trace how do I know it even left reset...20:31
ZipCPUdaveshah: Yes.  Clifford and I discussed this sort of thing last week20:32
ZipCPUI asked for an "asic" option that would throw out initial statements, assume an initial reset, and only check assertions on the next clock cycle20:32
daveshahYou could also have something that automatically does the f_past_valid stuff whenever it sees $past etc20:33
ZipCPUWe both agreed we *should* have an option like that, but the more we discussed it the more difficult the details turned out to be20:33
daveshahpepijndevos: as ZipCPU says, this is where you probably want to use cover20:34
ZipCPUYosys 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 irrelevant20:35
pepijndevosI see... but he also said you don't use them at the same time, so do you write two testbenches?20:35
ZipCPUNo--you place cover() statements side by side with your assert()/assume() statements20:35
ZipCPUThen you run the tool twice--once in either bmc or prove mode, and once in cover mode20:35
pepijndevosSo do you need to have two sby files? or can you have multiple modes?20:36
ZipCPUYou can have multiple modes in the same sby file20:37
pepijndevoshm ok20:37
ZipCPUTo do that, you need a [tasks] section--I typically place it at the top20:37
pepijndevosoh ok20:37
ZipCPUI 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
ZipCPUThen on any line to be executed in prove mode, I prefix it with "prf:"20:37
pepijndevosah I see20:38
ZipCPUAny line to be executed in cover mode gets prefixed with "cvr"20:38
tpbTitle: Reference for .sby file format SymbiYosys 0.1 documentation (at
ZipCPUAh, yeah, that's it20:38
ZipCPUpepijndevos: Here's an example from when verifying Xilinx's AXI-lite core:
tpbTitle: wb2axip/xlnxdemo.sby at master · ZipCPU/wb2axip · GitHub (at
ZipCPUYou can find the core itself here,
tpbTitle: wb2axip/xlnxdemo.v at master · ZipCPU/wb2axip · GitHub (at
ZipCPUAnd my report on the bugs I found here:
tpbTitle: Using a formal property file to verify an AXI-lite peripheral (at
ZipCPUpepijndevos: Have you found my course notes for using Symbiotic EDA Suite to verify VHDL designs?20:43
pepijndevosZipCPU, eh no, I have not.20:45
ZipCPULook for the link to the VHDL slides on this page:
tpbTitle: Verilog, Formal Verification and Verilator Beginner's Tutorial (at
ZipCPUYou should there find the course notes for the VHDL course, as well as several examples to work through20:46
pepijndevosBookmarked. 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
ZipCPUDid your assertion use $past()?20:48
ZipCPUCare to post it somewhere, so I can take a look?20:49
pepijndevosIt'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
pepijndevoshold on20:49
pepijndevoslemme add the remaining asserts so I can commit something sane20:50
ZipCPUDon't tell anyone, but I typically browse several forums each morning just looking for code I can try the formal tools on20:51
ZipCPUSo .... debugging the code of others is something I tend to enjoy20:51
pepijndevosdoes binary and have any footnukes?20:51
pepijndevosI'll show you, ready to commit, just need to make a github repo.20:53
pepijndevosUhg... quick, give me a name for a bit serial CPU haha20:53
ZipCPUfootnuke-and-fiance-free ?20:54
tpbTitle: GitHub - pepijndevos/seqpu: A bit-serial CPU (at
*** emeb_mac has joined #yosys20:56
pepijndevosOther advice on useful properties to test and stupid things I'm doing of course very welcome20:57
ZipCPUOkay, so how about:  cover property (@(posedge i_clk) opcode == 3'b000 ##1 );20:59
ZipCPUHmm ... that reset might get in the way20:59
ZipCPUHow about:  cover property (@(posedge i_clk) disable iff !rst; opcode == 3'b000 ##1 );20:59
pepijndevosWhat does that do?21:01
ZipCPUSo an assert() does anything it can to make the expression within false, a cover() is the opposite21:01
ZipCPUA cover statement will do anything to make the expression within the cover statement tru21:01
pepijndevosRight, 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 00021:02
ZipCPU##1 means go to the next clock cycle21:02
ZipCPUSo the result would be a trace showing the opcode == 3'b000 on one cycle, but not ending 'til at least the next21:02
ZipCPUFurther, the disable iff statement makes it so that it will have to pick a time when the reset value is low21:02
ZipCPUErr ... high in your case, since your resets are all using negative logic21:03
ZipCPUIt'd be sort of like: always @(posedge i_clk) cover(initial_reset && $past(opcode != 3'b000) && $past(rst) && rst);21:03
pepijndevosIt'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
ZipCPUNo, sleepy brain probably gets21:04
ZipCPUgets it21:04
ZipCPUWe can discuss more tomorrow if you'd like21:04
pepijndevosHave a nice day :)21:05
pepijndevosLast thought: In the whole CPU it would very much make sense to verify that the opcode can't change mid-instruction XD21:05
*** emeb_mac has quit IRC21:06
ZipCPUQuoted 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 IRC21:17
*** bwidawsk has joined #yosys21:21
*** emeb has quit IRC22:21
*** Stroboko1p has quit IRC23:31

Generated by 2.13.1 by Marius Gedminas - find it at!