ZipCPU|Alt has quit [Quit: Cap'n! The dilithium crystals are ...]
eduardo_ has joined #yosys
<ZipCPU>
awygle: If you just want cover, then don't worry about then know that I've used cover with yosys-smtbmc and not AIGER.
<ZipCPU>
awygle: I also would share your desire for "naming" properties. Specifically, I'd like to name a bunch of properties and then choose to assert or assume them en masse as appropriate.
eduardo has quit [Ping timeout: 248 seconds]
<awygle>
ZipCPU: my concern is that I don't know if I need "live" or not because I don't know what it does lol
<ZipCPU>
Yeah, that's a chapter I have yet to write ... if I understand correctly, it implements the s_eventually property and some others like it.
<ZipCPU>
These are properties I have yet to use.
<promach_>
ZipCPU: what do you mean by s_eventually property ???
<ZipCPU>
assert(s_eventually i_wb_ack); asserts that at some undefined point in the future, i_wb_ack will go high.
<promach_>
that is sequence
<promach_>
but does yosys support it currentlly ?
<ZipCPU>
As I understand, it's one of a couple of items yosys supports that aren't yet in my class notes.
<promach_>
what does AIGER actually do within yosys ?
<ZipCPU>
AIGER is just a format.
<ZipCPU>
However, the solver's that can handle s_eventually require an AIGER formatted input.
<awygle>
I admit that I don't immediately see how s_eventually is more useful than cover...
<ZipCPU>
The two solver's that use AIGER are avy and suprove.
dmin7 has joined #yosys
<promach_>
ZipCPU: so, to use s_eventually sequence property, I need to use avy / suprove instead of yices2 / z3 ?
<ZipCPU>
awygle: The difficult part of using s_eventually is that s_eventually will still return true even if it takes half of an infinite number of clock ticks to get there.
<ZipCPU>
promach_: Yes.
<promach_>
"half of an infinite number of clock ticks" <-- what do you exactly mean ?
<awygle>
you say "o_wb_stall is used to control the flow of data into the slave. it will be true on any cycle when the master cannot accept data from the slave"
<awygle>
those two things seem in conflict - is that supposed to say "when the slave cannot accept data from the master"?
* ZipCPU
looks up the simple-wishbone.html page ...
<ZipCPU>
awygle: Yes, you have the correct understanding. It will be true in any cycle when the *slave* cannot accept data from the master.
<awygle>
ZipCPU: okay, just checking :)
emeb_mac has quit [Quit: emeb_mac]
<awygle>
ZipCPU: i'm reading http://zipcpu.com/blog/2017/07/29/fifo.html again, and i wanted to confirm my understanding of the "high speed verilog cut". am i correct that the reason the earlier implementation was slow is because a) "full" and "empty" are calculated from a wide comparator and b) they're then used all over the place (high fan out)?
indy has quit [Ping timeout: 240 seconds]
* ZipCPU
looks it up ...
<ZipCPU>
Ah, yes, exactly!
<ZipCPU>
Yeah, you've got it. In general, you want to keep large comparisons out of complex logic expressions.
<awygle>
okay. i'm writing a FIFO with no overrun or underrun protection, so i'm not using "full" or "empty", just driving them out to the user. am i right that you _are_ still doing the wide comparisons in the "fast" cut, you're just doing them ahead of time and registering them?
<ZipCPU>
Yep!
<awygle>
okay great :) i should probably do that too, just to be nice to the user
<ZipCPU>
I would also caution you against building a FIFO with *no* overflow or underflow protection ... 'cause I can just about guarantee that it'll come back to bite you.
indy has joined #yosys
cemerick has joined #yosys
<awygle>
ZipCPU: actually, as i develop it more, it's becoming more that overflow is expected and operates as "drop last value"
<awygle>
hm, that's an interesting error. "Read port of memory is clocked, this is not supported by write_smt2"
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
cemerick has quit [Ping timeout: 256 seconds]
<ZipCPU>
awygle: Are you crossing clock domains?
<awygle>
ZipCPU: no
<ZipCPU>
Are you using clk2fflogic?
<awygle>
and afaict i'm not actually clocking the read port - it's done in an assign statement
<awygle>
no
<awygle>
also, jumping back to a discussion we had a long long time ago - i'm finally designing some circuits where knowledge of internal state would be hugely helpful for proofs
seldridge has joined #yosys
<ZipCPU>
Hehe --- Good!
seldridge has quit [Ping timeout: 256 seconds]
dmin7 has quit [Ping timeout: 245 seconds]
leviathan has quit [Read error: Connection reset by peer]
<awygle>
i respectfully disagree with your assessment :P
<ZipCPU>
Really? Where are you stuck? Need some help?
<awygle>
i think i'm mostly stuck due to stubbornness
<awygle>
if i just put in an assert(count == (dut.write_ptr - dut.read_ptr)); everything would work
<awygle>
but i don't like reaching into the module like that
<awygle>
what i'm trying to do is assert that when "count" == "depth", then "full" is asserted, and vice versa
<awygle>
and also that when "count" == 0 then "empty" is asserted
<awygle>
but my induction step is failing by starting from "count" being whatever it wants, and because i'm tracking count in a running fashion instead of just subtracting write from read, it stays out of sync forever
<awygle>
i'm thinking of calculating count each time inside the module, since i already have a huge comparator and a comparator is basically a subtraction, but again, i feel like i shouldn't have to
sklv has quit [Remote host closed the connection]
sklv has joined #yosys
<ZipCPU>
awygle: Why don't you put the assert within the FIFO module? You can surround it with `ifdef FORMAL and `endif if you would like.
<awygle>
ZipCPU: i tried doing that, but i still had issues. basically it seemed to want me to pull _every_ assert into the FIFO module, which i didn't want to do
<ZipCPU>
Well, did you see how I handled things with the WB properties?
<ZipCPU>
You should be able to do something similar here.
<ZipCPU>
Sure, if you'd like. The WB property file exports three variables to the external environment, the three it needs to force its state to match the state of its environment: how many requests have been made, acknowledgements have been received, and how many requests are outstanding.
<ZipCPU>
Exporting something similar from your FIFO might easily help you in your problem(s).
<awygle>
ZipCPU: i'm not sure i'm looking in the right place - can you link me to this WB property file?
<ZipCPU>
All of my WB bridges, also found in that same rtl/ex/ directory, require using the counters coming from the properties as well--as does *every* formally proven wishbone component I've built using those properties.
<awygle>
ZipCPU: okay, so i am doing something similar (i think). i'm counting the number of reads and the number of writes that have been made to the fifo. but the problem is that although i can assert that count is what it should be based on those counters, the induction step can assume arbitrary things about the read and write pointers. and if i do track those counters inside the module, then i'm writing the same algorithm for "count" in both the
<awygle>
module and the formal code, making the assertions of limited use.
AlexDaniel has quit [Ping timeout: 248 seconds]
<ZipCPU>
Where are you maintaining your counters? Within the FIFO only, or without and within the FIFO?
<awygle>
outside the fifo only
<awygle>
"above" it, in terms of the hierarchy
<ZipCPU>
Yeah, okay, you'll need to connect those to the ones within the FIFO then.
<awygle>
whereas i think your wishbone properties end up "below" the DUT in your setup
<ZipCPU>
Not quite.
<ZipCPU>
Well ... okay, yeah, I take that back, you are right.
<ZipCPU>
But those two counters also may need to propagate up even further than the DUT any time the DUT is made a submodule of another module.
<awygle>
so how do you handle that? `ifdef FORMAL output f_nacks `endif?
<ZipCPU>
It's also got to end up in the parameter list, but, yeah, that's pretty much how it's going to need to take place.
<ZipCPU>
I grimace when doing so, too, because it kind of destroys the whole point of encapsulation in the first place.
<ZipCPU>
But .... that's the current state of the tool set.
<awygle>
hmm... let me try one more thing and then i'll give up lol
<ZipCPU>
See, that's the thing with induction, it starts in a fairly random state.
<ZipCPU>
Unless you can constrain the state via assert/assume, you might just end up with something like that.
<pie___>
are there any fpgas other than the ice40 stuff planned to be sufficiently reversed to compile for?
<awygle>
pie___: "planned to be"? yes.
<ZipCPU>
yosys was supposed to have Altera support right now. It's all in there (I'm told), just still buggy.
<ZipCPU>
I know I've used the Xilinx support as well to count LUTs--just not to actually build designs.
<pie___>
ah wait im probably mixing stuff up because "im 12 and what is this
<pie___>
"
<pie___>
not actually sure how the build chain works ;_;
<awygle>
pie___: i'm pretty sure you're talking about "i want to build a design for an fpga architecture using only open source tools", right?
<pie___>
more or less yeah
<pie___>
also i kind of just want to avoid learning vhdl / verilog :P
* pie___
pokes at clash
<awygle>
in that case the ice40s are the only game in town right now, but there's an active effort underway for the Xilinx 7-series (particularly the Artix) and at least some moves in the direction of the ECP5s (also from Lattice)
<pie___>
great
<sorear>
greenpak, xc2
<ZipCPU>
"avoid learning vhdl / verilog" ? How would you rather program one of these beasts?
<pie___>
iirc someone (not the devs iirc?) brought up a yosys backend for clash without the vhdl/verilog intermediate but im quite sure nothing came of that and i cant remember any details
<pie___>
ZipCPU, yepp
<ZipCPU>
:P
<sorear>
there must be some form of IR
<ZipCPU>
sorear: Within yosys? Definitely.
<awygle>
yosys has RTLIL
<awygle>
something (chisel?) has FIRRTL
<awygle>
idk if clash has one
<sorear>
firrtl came out of chisel, yes
<pie___>
im probably not even approaching this right htough
<pie___>
what would cause you to need to poke at outputted verilog?
<pie___>
i guess interfacing with existing IP for starters
<sorear>
pie___: cross-correlating it with your source files when you get an error from some verification tool
<pie___>
meanwhile, how long till oss fpga stuff starts getting sued on software patents? :P
<awygle>
i'm surprised no one's been sued yet tbh
<awygle>
not so much over patents but just over general RE
<awygle>
which would be stupid, as closed-source bitstream formats are stupid ab initio, because none of the FPGA companies actually make their money on software
<awygle>
UGH yosys doesn't support hierarchical references because they're not synthesizable
<awygle>
okay, i successfully dragged out the signals i needed to prove these properties. i need to do cover stuff now but more importantly i need to take a break because that was really frustrating lol