clifford changed the topic of #yosys to: Yosys Open SYnthesis Suite: http://www.clifford.at/yosys/ -- Channel Logs: https://irclog.whitequark.org/yosys
gundy has quit [Ping timeout: 276 seconds]
<sammy> interesting
<ZipCPU> So, the RISC-V core isn't verified in its natural environment. It's verified as just a core.
<ZipCPU> The formal verification cores, and the assertions and properties, replace the top level
<sammy> How is this different than testbench simulation with assertions in the testbench files?
<ZipCPU> The formal engine picks the instructions and the instruction sequences
<ZipCPU> It's like a petulant child just trying to prove you wrong
<ZipCPU> Only ... it plays by the rules (the child might not)
<ZipCPU> One new formal learner put it this way, "that formal engine is really quite a bastard isn't he?"
<ZipCPU> For example, you might run a test bench on all your instructions, but miss a particular instruction sequence with a pipelining bug in it
<ZipCPU> You might have an instruction that should be an illegal instruction, yet you never test that the "right-thing" is done with it
<ZipCPU> It can also pick how long the bus (or other external interface) will take to respond to the CPU
Ultrasauce has quit [Quit: Ultrasauce]
Ultrasauce has joined #yosys
leviathan has joined #yosys
emeb has left #yosys [#yosys]
gundy has joined #yosys
pie_ has quit [Ping timeout: 246 seconds]
emeb_mac has joined #yosys
gundy has quit [Ping timeout: 252 seconds]
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
dys has quit [Ping timeout: 260 seconds]
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
nrossi has joined #yosys
rohitksingh has quit [Ping timeout: 272 seconds]
kraiskil has joined #yosys
m4ssi has joined #yosys
massi_ has joined #yosys
emeb_mac has quit [Quit: Leaving.]
rohitksingh has joined #yosys
leviathan has quit [Quit: http://quassel-irc.org - Chat comfortably. Anywhere.]
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
massi_ has left #yosys ["Leaving"]
m4ssi has quit [Quit: Leaving]
m4ssi has joined #yosys
rohitksingh has quit [Ping timeout: 245 seconds]
rohitksingh has joined #yosys
GuzTech has joined #yosys
kraiskil has quit [Ping timeout: 250 seconds]
gundy has joined #yosys
gundy has quit [Ping timeout: 252 seconds]
xdeller_ has quit [Remote host closed the connection]
xdeller_ has joined #yosys
rohitksingh has quit [Quit: Leaving.]
kraiskil has joined #yosys
leviathan has joined #yosys
rohitksingh has joined #yosys
jayaura has joined #yosys
Aleksandar-K has joined #yosys
pie_ has joined #yosys
emeb has joined #yosys
GuzTech has quit [Quit: Leaving]
maikmerten has joined #yosys
Aleksandar-K has quit [Quit: Leaving]
leviathan has quit [Quit: http://quassel-irc.org - Chat comfortably. Anywhere.]
emeb has quit [Ping timeout: 252 seconds]
emeb has joined #yosys
dxld has quit [Ping timeout: 252 seconds]
kraiskil has quit [Ping timeout: 250 seconds]
dxld has joined #yosys
kraiskil has joined #yosys
maikmerten has quit [Remote host closed the connection]
m4ssi has quit [Remote host closed the connection]
pie_ has quit [Read error: Connection reset by peer]
pie__ has joined #yosys
kraiskil has quit [Ping timeout: 276 seconds]
s_frit has quit [Remote host closed the connection]
s_frit has joined #yosys
dys has joined #yosys
rohitksingh has quit [Quit: Leaving.]
kraiskil has joined #yosys
kraiskil has quit [Client Quit]
dxld has quit [Quit: Bye]
dxld has joined #yosys
dxld has quit [Client Quit]
dxld has joined #yosys
develonepi3 has quit [Read error: Connection reset by peer]
develonepi3 has joined #yosys
leviathan has joined #yosys
emeb has quit [Quit: Leaving.]