<tpb>
Title: UART/test_UART.v at development · promach/UART · GitHub (at github.com)
<promach__>
ZipCPU awygle
<ZipCPU>
At one time your design was set up to force the creation of a parity error. Did you ever fully fix/repair that code back to normal?
<promach__>
ZipCPU: at one time ???
<ZipCPU>
Yeah, when you first started to try and prove that your UART worked.
<promach__>
it seems like BMC passes for me, not induction
<promach__>
but let me check again
<ZipCPU>
promach__: Okay, but let's think about this a moment first.
<ZipCPU>
Have you looked at the trace?
<ZipCPU>
If so, which is in error: 1) the logic, 2) the formal properties, or 3) the formal engine is placing the logic into a state it should never be able to get into?
digshadow has quit [Quit: Leaving.]
<promach__>
ZipCPU: I found my bug using BMC. my assert() at line #172 is not correct
digshadow has joined #yosys
<promach__>
seems like if I am stucked at induction, I should run BMC again instead
<promach__>
thanks ZipCPU
<ZipCPU>
There is another method.
<ZipCPU>
... which would even work here. I haven't tried it though.
<promach__>
would you mind sharing to all of us here ?
<ZipCPU>
That would be to use an updated Verilator.
<promach__>
huh ?
<ZipCPU>
You might need to get rid of your $past statements, 'cause I don't think Verilator supports those yet.
<promach__>
I am using FORMAL tag
<promach__>
so, it is okay
<promach__>
why use verilator for formal verification ?
<ZipCPU>
Then, you'd use Verilator to go through a full trace of your design, and to halt on any assert()ion or assume()ption errors.
<promach__>
so, use verilator for BMC sort of thing ?
<promach__>
but I do not think verilator supports induction or coverage yet, right ?
<ZipCPU>
Yes, but you would go *much* deeper (i.e. more cycles), and you wouldn't exhaust all possibilities.
<ZipCPU>
Verilator is more of a simulator than a formal engine, but the formal properties are supposed to have meaning within a simulator.
<ZipCPU>
assert() turns into the C-language assert.
<promach__>
but increasing BMC depth would also do the same thing, right ?
<ZipCPU>
I also pushed a patch to Verilator to turn assume() statements into C-language asserts as well.
<ZipCPU>
Not quite.
<promach__>
I do not get it
<promach__>
why not ?
<ZipCPU>
Increasing BMC depth would still test your design with *EVERY POSSIBLE* input. When using Verilator, your design would only have the inputs you give it.
<promach__>
I see, stimulus
<promach__>
I got your message, simulate first, then only do formal verification
<promach__>
ZipCPU: I got to go now
<ZipCPU>
Well ... that wouldn't normally be my message
<ZipCPU>
But it might help you figure out what's going wrong.
<promach__>
sure, okay
<promach__>
let me fix the assert() at line #172 first
<ZipCPU>
See ... if you knew what assert() at line #172 were failing, then 1) you wouldn't be asking for help, and 2) you wouldn't need the Verilator route.
jwhitmore_ has quit [Remote host closed the connection]
pie__ has joined #yosys
proteus-guy has joined #yosys
proteusguy has quit [Ping timeout: 240 seconds]
promach has quit [Quit: WeeChat 2.1-dev]
pie__ has quit [Ping timeout: 246 seconds]
m_t has joined #yosys
cemerick has joined #yosys
cemerick_ has joined #yosys
FabM has quit [Ping timeout: 245 seconds]
cemerick has quit [Ping timeout: 246 seconds]
FabM has joined #yosys
cemerick has joined #yosys
cemerick_ has quit [Ping timeout: 276 seconds]
AlexDaniel has joined #yosys
pie_ has joined #yosys
clifford has joined #yosys
seldridge has joined #yosys
promach__ has joined #yosys
sklv has joined #yosys
seldridge has quit [Ping timeout: 246 seconds]
igmar has joined #yosys
<igmar>
ZipCPU : Thanks for the hint
<ZipCPU>
??
<ZipCPU>
Which one? ;)
<igmar>
On formal verification, and the exitence of this channel
<ZipCPU>
Oh, sure, my pleasure! Welcome to the channel!
<igmar>
I'm @Palsenberg on Twitter
<ZipCPU>
Sure! We discuss all kinds of yosys related (and unrelated) topics here, including formal.
<ZipCPU>
You'll find several individuals on this channel working on using formal methods: some new comers, some who've been doing it much longer, and you might even get access to some developers. :D
<igmar>
Resources are a bit scarse on that area. And the question usualy is : How to get started, and what is good / isn't
<ZipCPU>
igmar: That's something I'm working on. Not only am I creating a (for profit, pay, etc.) course, but I'm also trying out course material in my blog posts.
<igmar>
I'll just get my hands dirty, even if Verilog is quite some while ago
<ZipCPU>
Jump right in!
<ZipCPU>
Have you found my blog? And the (bare) introductory material I've posted on it?
<ZipCPU>
Or any of the examples I've posted?
<igmar>
For profit is fine with me. I just did nand2tetris on coursera
<igmar>
Yeah, reading through them
<ZipCPU>
Fun course, huh?
<igmar>
Yeah, it was a good course
<ZipCPU>
Feel free to come here if you have questions.
<igmar>
I will
<igmar>
And checking if I can help edaplayground devs out
<ZipCPU>
Not sure how many of those types are on this channel ...
<igmar>
No idea. For now, email only
<ZipCPU>
Ok. Sure.
<ZipCPU>
Incidentally, the "Clocks for Software engineers article" was in response to someone I had met who was using EDA playground without access to real hardware ... ;)
<igmar>
I'm a good SW dev. Which isn't a good thing when doing HW I discovered
<ZipCPU>
It's not as bad as folks make it out to be. I came from the SW world myself.
<igmar>
And I go my tinyfpga board, which will be fun
<igmar>
At least the syntax is familiar
<ZipCPU>
Heheh ... got one of those on my desk as well. Love what Luke's been up to.
seldridge has joined #yosys
<igmar>
Indeed
<ZipCPU>
One of my goals is to get a ZipCPU running on it.
<ZipCPU>
Right now it fits, but I need to do some more work before the flash driver is running and ... my designs just require too much memory to be able to run without flash.
<igmar>
flash for running the zipcpu code ?
<sorear>
is it much easier if you already know what a nand and a dff are?
<ZipCPU>
igmar: Yes.
<ZipCPU>
sorear: If you are asking me, I wouldn't know.
<igmar>
I had that in university... 20 years ago :)
<ZipCPU>
igmar: You must be like me. The last University course I took in Computer Engr was at least 20 years ago.
<igmar>
BSc in 2001 :)
<ZipCPU>
MSc in '95.
<igmar>
You win :-)
<ZipCPU>
I remember studying how the Alpha was designed. That design has now been defunct for quite a while too.
<igmar>
I grew up with a z80
seldridge has quit [Ping timeout: 240 seconds]
<igmar>
Any ideas on UVM / OVM / OVL ?
<ZipCPU>
No. Sadly, I just learned what UVM was this month.
<sorear>
defunct commercially but it's still the subject of surprisingly many papers
<ZipCPU>
sorear: You mean the alpha? or UVM?
<sorear>
i'm unfamiliar with UVM/OVM/OVL, i mean alpha
<ZipCPU>
k
eduardo_ has joined #yosys
eduardo__ has quit [Ping timeout: 240 seconds]
<awygle>
sorear: I'd say a dff is important to know, I can explain NAND in like 30m to someone with no prior knowledge of boolean algebra
promach__ has quit [Ping timeout: 268 seconds]
digshadow has quit [Ping timeout: 260 seconds]
<ZipCPU>
awygle: For me, working on FPGA's, understanding a LUT has been more useful than understanding what a NAND is.
digshadow has joined #yosys
<awygle>
ZipCPU: sure, but I wouldn't look at nand2tetris for utility exactly, more for understanding
<tpb>
Title: Implementing FizzBuzz on an FPGA (at www.righto.com)
<ZipCPU>
shapr: Yeah, I saw that. Reading what a fizzbuzz was was a lot of fun.
seldridge has joined #yosys
<shapr>
I've been surprised how many interviewees can't do fizzbuzz
seldridge has quit [Ping timeout: 276 seconds]
GuzTech has quit [Quit: Leaving]
<awygle>
ZipCPU: excellent article today! I really enjoyed it
<awygle>
I think I understand your point about Formal not being black box a lot better now
seldridge has joined #yosys
seldridge has quit [Ping timeout: 276 seconds]
clifford has quit [Quit: Ex-Chat]
clifford has joined #yosys
clifford has quit [Quit: Ex-Chat]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
clifford has joined #yosys
cemerick has quit [Ping timeout: 265 seconds]
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
dys has joined #yosys
<ZipCPU>
awygle: Thanks!
<ZipCPU>
I was afraid it was going to ramble too much, wandering far afield of a clear topic line.
<awygle>
well, i get to cheat a bit, being privy to much of the background
<ZipCPU>
So, it made sense to you, then, since you'd been working with formal?
<awygle>
yes
<awygle>
on a somewhat related topic
<awygle>
does your course discuss the details of the formal verification algorithms?
<ZipCPU>
Go on
<awygle>
well i've been reading about Property Driven Reachability after our discussion about induction
<ZipCPU>
... and what have you discovered?
<awygle>
and i'd be interested in some discussion of the power and efficiency of the various algorithms in various conditions
<awygle>
well, certainly the PDR algorithm is much harder to explain!
<ZipCPU>
Of these "various algorithms", are you referencing formal engines, or the designs those engines would be used to prove?
<awygle>
my understanding is this
<awygle>
there are several SAT or SMT solvers (e.g. Minisat)
<awygle>
then on top of that there are several formal engines which use them (e.g. avy)
leviathan has quit [Remote host closed the connection]
<awygle>
each of those formal engines may implement one or more formal verification algorithms (basic k-induction, interpolation, pdr, others?)
<ZipCPU>
So far, so good ... go on.
<awygle>
the lines can get blurry (maybe an engine contains its own SAT solver) but that's the basic shape of things
<awygle>
i'm interested in when it is appropriate to use one algorithm over another. for example, your induction example was provable by pdr but not by k-induction.
<ZipCPU>
Aahh ... okay.
<awygle>
i imagine there are probably some problems that k-induction can solve that pdr can't or that k-induction is much more efficient on, or or or....
<ZipCPU>
I'm not sure if the engines are told "this is induction" or "this is bmc". For that, I think the difference is only in the problem setup.
<awygle>
i intend to dig into it more myself (as time permits) but some received wisdom would be nice :P
<ZipCPU>
You assume I have some of that? :D
<awygle>
i assume you either have it or can get it more readily than i
<awygle>
(although i see clifford is in the channel today)
dys has quit [Ping timeout: 276 seconds]
<ZipCPU>
Hmm ... I take back my comment on Induction and BMC just being the same problem presented differently. Yosys will present both for the yosysbmc engines (yices, boolector, z3, etc) in the same format.
<awygle>
on another axis entirely the PDR papers i've read make a point of how parallelizable it is, which interests me as well
<ZipCPU>
In other words, the solver/engine needs to know the difference between the two.
<ZipCPU>
Yeah, parallelization would interest me too ... probably only enough to watch someone work on it and to try it out. I'm not sure if I'm ready to dig into building my own engine.
<awygle>
i'll put it into my queue of projects
<awygle>
(a queue which grows at a rate beta >> 1)
<ZipCPU>
Your queue sounds like mine ...
pie_ has quit [Ping timeout: 264 seconds]
<ZipCPU>
Not that building a parallelized formal engine wouldn't be fun ...
dys has joined #yosys
<awygle>
Someday (TM)
<awygle>
or how about this - if you decide to pull the trigger on that project, you know where to find a collaborator :P
<ZipCPU>
More likely I'd never be anything more than a cheerleader or a tester.
<cr1901_modern>
ZipCPU: The engines aren't told whether it's induction or bmc
<ZipCPU>
cr1901_modern: They must be told--how else can you give them the same .smt2 file?
<cr1901_modern>
ZipCPU: B/c you don't give them the same .smt2 file. yosys-smtbmc adds different code to the smt files depending on whether you do BMC or induction
<ZipCPU>
Ahh ... okay, that must be what I was missing.
<cr1901_modern>
I guess it depends on what you mean by "being told". There isn't a command-line switch you give the engines to say "I want to do induction or BMC"
<ZipCPU>
That's what I was referencing ... I was assuming yosys-smtbmc must've set such a switch, while leaving the smt2 file intact.
<ZipCPU>
I gather you are telling me it works the other way around.
<tpb>
Title: GitHub - cr1901/spi_tb: CPOL=0, CPHA=0 SPI core for practicing formal verification with yosys (at github.com)
<cr1901_modern>
it'll dump two files: spi_tb_bmc.smt2 and spi_tb_tmp.smt2
<cr1901_modern>
They are the smt2 file that yosys outputs using the SMTv2 backend decorated with the extra required statements/asserts to feed into an SMT solver to do BMC/Induction
<cr1901_modern>
you'll notice they are different
<ZipCPU>
Ok. Are you using the same smt2 engines that yosys-smtbmc already uses?
<awygle>
ZipCPU: cr1901_modern: how does this discussion apply to engines other than smtbmc? guessing .smt2 files are not used in those cases so somewhat different circumstance
<cr1901_modern>
smtbmc isn't an engine
<cr1901_modern>
it calls out to an SMT solver
<cr1901_modern>
ZipCPU: I use z3, so yes
<awygle>
cr1901_modern: per my taxonomy above it's an engine which calls out to one of several SMT solvers (as opposed to something like avy which does its own thing)
<cr1901_modern>
Idk if it's an engine then. But the SMT solver it calls out to is doing the bulk of the work