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
aaaa has quit [Ping timeout: 265 seconds]
Degi has quit [Ping timeout: 272 seconds]
Degi has joined #yosys
citypw has joined #yosys
awordnot has quit [Read error: Connection reset by peer]
awordnot has joined #yosys
emeb_mac has quit [Quit: Leaving.]
jakobwenzel has joined #yosys
az0re has quit [Remote host closed the connection]
az0re has joined #yosys
forrestv has quit [Ping timeout: 260 seconds]
forrestv has joined #yosys
N2TOH has quit [Quit: PULL!]
flaviusb has joined #yosys
citypw has quit [Remote host closed the connection]
citypw has joined #yosys
nengel has quit [Quit: nengel]
attie has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
az0re has quit [Ping timeout: 240 seconds]
citypw has joined #yosys
kristianpaul has joined #yosys
<z0ttel> I am somewhat puzzled by what I read about the verific frontend. Does it really allow SymbiYosys to prove sequence expressions? Are these expanded by the frontend and reduced to what the expressions understood by the open-source front-end are capable of, or are there more powerful temporal logic expression understood internally than the regular front-end supports?
<daveshah> The expansion code is all open source
<tpb> Title: yosys/verificsva.cc at master · YosysHQ/yosys · GitHub (at github.com)
<daveshah> aiui, it basically compiles them down to a FSM of sorts
<daveshah> All Verific is doing is parsing and elaboration, it doesn't do any of the real 'magic' in compiling these
<z0ttel> Ah, interesting. Thank you :)
klotz has joined #yosys
az0re has joined #yosys
Asu has joined #yosys
emeb has joined #yosys
somlo has quit [Remote host closed the connection]
somlo has joined #yosys
LJ_cache has joined #yosys
citypw has quit [Ping timeout: 240 seconds]
<ZipCPU> z0ttel: You can find a fascinating discussion of sequence properties using the Verific front end here: https://zipcpu.com/formal/2019/02/21/txuart.html
<tpb> Title: Using Sequence Properties to Verify a Serial Port Transmitter (at zipcpu.com)
<z0ttel> @ZipCPU: Already had a look at that today :)
<ZipCPU> Cool. That should help you understand the power of the sequence properties
<z0ttel> Well, I haven't touched verific itself yet.
<z0ttel> Used to do LTL/CTL* at university tho, so I have some familiarity with temporal logic.
<z0ttel> My first attempt at verifying a FIFO: https://gist.github.com/Zottel/6b5075602dfae367be0c8305423e474c
<tpb> Title: generic_fifo_proof.sv · GitHub (at gist.github.com)
<z0ttel> I'm pretty confident that I can trust a FIFO that succeeds in cover and bmc checks with that scaffolding, but somehow, a more integrated version that will help when the FIFO is embedded in a whole system would be nice too.
<ZipCPU> z0ttel: The typical proof of a FIFO is that you can write an arbitrary two values into it, and then some time later read them back out and in the same order
<ZipCPU> To see how you might handle that, feel free to check out the FIFO lesson of my tutorial: https://zipcpu.com/tutorial
<tpb> Title: Verilog, Formal Verification and Verilator Beginner's Tutorial (at zipcpu.com)
kristianpaul has quit [Ping timeout: 260 seconds]
<z0ttel> Ah, I must've skipped the presentation. cool, thx.
<z0ttel> @ZipCPU: There's something I thought about when reading your skynet/exchanging asserts/assumes article: Wouldn't a general assert(all assumptions imply property) style solve that issue?
<ZipCPU> I'm not sure how it would or could
kristianpaul has joined #yosys
klotz has quit [Quit: klotz]
emeb_mac has joined #yosys
<ZipCPU> z0ttel: The problem with skynet was roughly: assume(A); B = A; assert(B); If you switch it to B=A; if (A) assert(A) ... you still have the same problem.
<z0ttel> I meant switch "assume(A) ... assert(B)" to "assert (A -> B)".
<z0ttel> but will have another look at the issue tomorrow, EU sleepy time now.
<ZipCPU> o/
<ZipCPU> But ... A = B; assert(A |-> B) is next to tautologous. So also is: A = B; assert(B |-> A); It doesn't make a difference
<z0ttel> but having assume(A); B=A; assume(B) is just as tautologous^^
<z0ttel> (the latter assume being an assert)
<ZipCPU> Yes
Asu has quit [Ping timeout: 240 seconds]
Asuu has joined #yosys
Asuu has quit [Remote host closed the connection]
pacak has quit [Remote host closed the connection]
pacak has joined #yosys
lf_ has joined #yosys
lf has quit [Ping timeout: 260 seconds]
FFY00 has quit [Read error: Connection reset by peer]
FFY00 has joined #yosys
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #yosys
FFY00 has quit [Remote host closed the connection]
FFY00 has joined #yosys