clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
tpb has quit [Remote host closed the connection]
tpb has joined #yosys
Degi has quit [Ping timeout: 246 seconds]
Degi has joined #yosys
citypw has joined #yosys
emeb_mac has quit [Quit: Leaving.]
gorbak25 has quit [Quit: gorbak25]
kraiskil has joined #yosys
Asu has joined #yosys
kraiskil has quit [Ping timeout: 260 seconds]
pacak has quit [Read error: Connection reset by peer]
pacak has joined #yosys
kraiskil has joined #yosys
unkraut has quit [Remote host closed the connection]
unkraut has joined #yosys
<thardin> is it possible to prevent yosys from replacing memory with registers?
<tnt> (* nomem2reg *) IIRC
strubi has joined #yosys
<thardin> read_verilog -nomem2reg works
<thardin> I think replacing the state machine with a ROM based one is better use for the BRAM for now
<daveshah> Be careful with nomem2reg, it can cause missynthesis
<thardin> yep, saw that
<thardin> sweet, using a state mechine LUT brings LC use down by 6%
<thardin> perhaps I can do something similar with division
<strubi> hi there, just tuning in...is anyone aware of the current situation on the pyosys API, is it used much at all? I think I recall someone mentioning integration with nmigen, but not sure if that was using pyosys
<mwk> that's not pyosys
<strubi> Allright, thought they were connected (from whitequark's comments on github WRT python API)
m4ssi has joined #yosys
<lambda> can someone explain to me why this two-stage evaluation of DFF inputs is necessary in the btor backend? I don't see why it wouldn't be possible to just recurse on the D port's signal immediately when exporting the cell https://github.com/YosysHQ/yosys/blob/master/backends/btor/btor.cc#L70
<tpb> Title: yosys/btor.cc at master · YosysHQ/yosys · GitHub (at github.com)
FFY00 has quit [Quit: dd if=/dev/urandom of=/dev/sda]
FFY00 has joined #yosys
<lambda> huh, `test_cell` has been broken for $[s]sh(l|r) since december 2019 (it generates B_SIGNED=1 with 50% probability) and apparently nobody noticed yet
X-Scale has quit [Ping timeout: 256 seconds]
kraiskil has quit [Ping timeout: 264 seconds]
m4ssi has quit [Remote host closed the connection]
emeb has joined #yosys
<thardin> can yosys do simulation? or is iverilog the way to go?
<whitequark> yosys has a sim pass
<whitequark> though it's pretty basic
<whitequark> it also has the cxxrtl backend, which is similar to verilator
<lambda> $shift and $shiftx ignore \A_SIGNED; is that intentional? it seems to be accounted for in satgen.h so `check_cells` doesn't catch it, but it's highly unintuitive
<tpb> Title: yosys/satgen.h at master · YosysHQ/yosys · GitHub (at github.com)
<thardin> I see the yosys site recommends using iverilog due to potential bugs in yosys
<thardin> I suppose simulating in both is useful for discovering bugs in either :)
<Lofty> <thardin> I suppose simulating in both is useful for discovering bugs in either :) <-- this is what vloghammer does
<tnt> Lofty: does vloghammer include cxxrtl now ?
<tnt> oh wait ... laste published report is 2014-01-24.
<Lofty> There's no reason you couldn't add it, tbh
kraiskil has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
<strubi> lambda, are you saying that srl/srr is broken WRT signedness?
<strubi> It *might* be intentional, if it's supposed to be a logical shift (vs. arithmetic)
<thardin> is it possible to formally verify verilog code?
<Lofty> Yes, SystemVerilog Assertions
<Lofty> And SymbiYosys
<Lofty> ZipCPU does it extensively
<thardin> interesting
<thardin> I've used frama-c quite a bit, so it shouldn't be too hard
<lambda> strubi: no, its's $shift/$shiftx that are broken https://github.com/YosysHQ/yosys/issues/2196
<tpb> Title: $shift and $shiftx ignore \A_SIGNED · Issue #2196 · YosysHQ/yosys · GitHub (at github.com)
<strubi> Ok, got me worried for a second, as it didn't turn up on my side. Haven't used $shift. Would that turn up in a VHDL test scenario?
<lambda> I don't know if anything internal generates a $shift with \A_SIGNED=1, so no idea, sorry
<lambda> I stumbled on it through targetted fuzzing of that cell
kraiskil has quit [Ping timeout: 260 seconds]
X-Scale has joined #yosys
<ZipCPU> thardin: I'm also known for wandering about the channel every now and again, so feel free to ask if you have any questions
<ZipCPU> As for those 509 pages, I use them for teaching a course over the course of (roughly) two full days--when you include the exercises
kraiskil has joined #yosys
kraiskil has quit [Ping timeout: 258 seconds]
<thardin> ZipCPU: yeah so I gathered :)
<thardin> I've become the "formal verification guy" in town lately
<thardin> or I guess the formal verification guy in norrland
oldtopman has quit [Ping timeout: 260 seconds]
<ZipCPU> thardin: Yeehaa! Welcome to the club, huh?
<ZipCPU> Only ... I'm not in norrland, but we can skip that part ...
<thardin> yesd
oldtopman has joined #yosys
<thardin> like I like to tell people: "you have tests, huh? I have proofs"
<ZipCPU> o/
<thardin> in case you haven't seen it: http://langsec.org/
<tpb> Title: Language-theoretic Security (at langsec.org)
<thardin> it's hard to impress on people just how godawful everything is in terms of correctness or even just not crashing or having horrible 0days
emeb_mac has joined #yosys
<ZipCPU> "Language security"? The concept looks interesting ... untrusted inputs into a formal model to turn them into something trusted, hmm ... okay. I came across something else similar recently under the title "Promise theory".
<thardin> the E language is based around promise pipelining if I remember correctly
<tpb> Title: Welcome to ERights.Org (at erights.org)
<thardin> lots of interesting stuff that haven't been explore enough
<sorear> I really doubt those are the same promises
<sorear> promises in the E sense come from the smalltalk/actors tradition, about as far as you can get from formal methods
<thardin> yeah E doesn't have much to do with formal methods come to think of it
<thardin> we looked at it for a distributed project at un
<thardin> uni
<sorear> interesting, this is the first I've heard of anyone trying to use that as-is
<thardin> welll it didn't really leave the idea stage :)
<thardin> we hacked something together using mpi and shared memory instead
Asu has quit [Quit: Konversation terminated!]
nengel has quit [Ping timeout: 240 seconds]
az0re has joined #yosys
Cerpin has quit [Ping timeout: 264 seconds]
Cerpin has joined #yosys
fevv8[m] has joined #yosys