clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
emeb_mac has joined #yosys
leviathan has joined #yosys
rohitksingh_work has joined #yosys
pie_ has quit [Ping timeout: 268 seconds]
emeb has left #yosys [#yosys]
dys has quit [Ping timeout: 252 seconds]
emeb_mac has quit [Quit: Leaving.]
m4ssi has joined #yosys
cr1901_modern has quit [Ping timeout: 246 seconds]
gundy has joined #yosys
cr1901_modern has joined #yosys
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
xdeller_ has quit [Read error: Connection reset by peer]
xdeller_ has joined #yosys
<gundy> Is this a reasonable place to ask questions about nextpnr?
<ZipCPU> About as good as any
<ZipCPU> Some of the developers are on this channel
<gundy> actually, don't worry - I think I know what's going on... I've just switched from arachne-pnr to nextpnr, and started seeing some "Floating wire node value, [X] on [Y], converted to zero driver" warnings around some of the BRAM blocks I was using.
<gundy> I _think_ that it might just be warning me that it's assembled/synthesised things in such a way that not all of the ports on the underlying blocks are used.
voxadam has joined #yosys
tautologico has quit [Quit: Connection closed for inactivity]
<daveshah> Just ignore those warnings
<daveshah> They shouldn't be printed in that case
NB0X-Matt-CA has quit [Ping timeout: 245 seconds]
NB0X-Matt-CA has joined #yosys
pie_ has joined #yosys
<gundy> cool, thanks.. actually, since you're here, big thanks for all the work you've put into the OS toolchain!!
gundy has quit [Ping timeout: 252 seconds]
<ZipCPU> daveshah: That's a shout out to you :D
<daveshah> Cheers gundy!
rohitksingh_work has quit [Read error: Connection reset by peer]
Aleksandar-K has joined #yosys
rohitksingh has joined #yosys
Aleksandar-K has quit [Remote host closed the connection]
Aleksandar-K has joined #yosys
leviathan has quit [Read error: Connection reset by peer]
leviathan has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
voxadam_ has joined #yosys
zino_ has joined #yosys
kuldeep_ has joined #yosys
Nazara_ has joined #yosys
voxadam has quit [*.net *.split]
knielsen has quit [*.net *.split]
pointfree has quit [*.net *.split]
Nazara has quit [*.net *.split]
zino has quit [*.net *.split]
brandonz has quit [*.net *.split]
kuldeep has quit [*.net *.split]
TFKyle has quit [*.net *.split]
Nazara_ is now known as Nazara
danieljabailey has quit [Ping timeout: 252 seconds]
danieljabailey has joined #yosys
TFKyle has joined #yosys
brandonz has joined #yosys
m4ssi has quit [Remote host closed the connection]
Aleksandar-K has quit [Quit: Leaving]
emeb has joined #yosys
rohitksingh has quit [Quit: Leaving.]
leviathan has quit [Quit: http://quassel-irc.org - Chat comfortably. Anywhere.]
rohitksingh has joined #yosys
zino_ is now known as zino
pointfree has joined #yosys
rohitksingh has quit [Ping timeout: 268 seconds]
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
dys has joined #yosys
dys has quit [Ping timeout: 244 seconds]
leviathan has joined #yosys
FL4SHK has quit [Ping timeout: 260 seconds]
FL4SHK has joined #yosys
tautologico has joined #yosys
rohitksingh has joined #yosys
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
maikmerten has joined #yosys
dys has joined #yosys
leviathan has quit [Quit: http://quassel-irc.org - Chat comfortably. Anywhere.]
maikmerten has quit [Remote host closed the connection]
TFKyle has quit [Quit: :q!]
gundy has joined #yosys
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
<ZipCPU> Yaaayyy!! I just managed to formally verify my first RISC-V core using riscv-formal! (It's a client's core, and not my own--this is just my first time using riscv-formal)
emeb_mac has joined #yosys
emeb_mac has left #yosys [#yosys]
<sorear> \o/
<sammy> What's riscv-formal?
<ZipCPU> sammy: Yes, that's it
<ZipCPU> It's a series of tests that a RISC-V CPU should pass in order to be called a RISC-V CPU
<ZipCPU> This was my first project using it
pie_ has quit [Remote host closed the connection]
pie_ has joined #yosys
<sammy> I'm guessing I can't use it to verify a RISCV CPU written in VHDL?
<ZipCPU> You could ...
<ZipCPU> But you'd need to get the commercial copy of Yosys to do it with
<ZipCPU> Likewise for a SystemVerilog version
<sammy> I thought the idea with formal is to have the assertions embedded with the HDL. Does this insert assertions?
<ZipCPU> Not necessarily
<ZipCPU> That's actually a statement of debate
<ZipCPU> The industry standard is to place the formal assertions *outside* of the HDL
<ZipCPU> I do the opposite, placing my assertions in the same HDL file, but after the HDL
<ZipCPU> Part of the reason for doing this is that Yosys (the only FV solution I could afford) doesn't support referencing variables from within submodules other than through a module port
<ZipCPU> Hence if you have a design, toplevel, with a CPU within it, cpu, and a decoder within that, at the toplevel you might wish to support the instruction within the decoder as toplevel.cpu.decoder.instruction
<ZipCPU> The free version of yosys doesn't support this notation
<ZipCPU> Hence, I'm confined to placing assertions within the HDL in question
<ZipCPU> riscv-formal handles this by passing a packet of instruction information through the CPU's toplevel port list
<ZipCPU> The riscv-formal tests are then applied to this packet of information