<ZipCPU>
cr1901_modern: I'm not sure I follow ... are you asking a question, or making a statement?
<cr1901_modern>
I'm asking: What are the semantics of @posedge clk inside a concurrent assertion?
<ZipCPU>
Wow, ahm, okay, let me try ...
<ZipCPU>
If you are making a concurrent assertion, Verific demands a clock of some type.
<cr1901_modern>
Oh it's Verific specific... that's why I've never seen it
<ZipCPU>
That clock can be within the assert property statement, within the definition of the property, in a clocking block, or ... many other places
<ZipCPU>
Yeah, that particular piece of code is very much Verific specific.
<ZipCPU>
The txuartlite.v file has both Verific and non-Verific formal verification structures.
<ZipCPU>
The rxuartlite.v is entirely non-verific
<ZipCPU>
... and I haven't figured out how to do the rxuart.v at all yet.
<ZipCPU>
Incidentally, even with Verific, yosys can't handle the txuart.v file (yet)
<cr1901_modern>
SystemVerilog tutorials will show code like always @(posedge clk) begin assert property (#1 foo == 0); end
<cr1901_modern>
err the "#1" is misplaced
<ZipCPU>
I haven't seen that type at all. As I understand it, the "property" doesn't work within an always block. I could be wrong tho.
<cr1901_modern>
It's one of SutherlandHDL's presentations. I don't understand the semantics, considering that a concurrent assertion is supposed to be checked always
<ZipCPU>
Can you share the assertion? I could take a peek at it.
<cr1901_modern>
I don't have it on me right now, I'll find it in a bit
<ZipCPU>
Ok
<ZipCPU>
I do teach concurrent assertion stuffs, so I know a bit about it. My knowledge isn't exhaustive though, so I might still be surprised by parts and pieces of it.
<cr1901_modern>
In my SPI TB, I don't use concurrent assertions, only "assume property" for some things
<cr1901_modern>
Prob should find time to annotate that more
<ZipCPU>
So ... a quiet little note, Yosys supports some non-standard assert property things.
<ZipCPU>
The fundamental assertion is found in lines 394-398
<ZipCPU>
It says that any time a write request comes in when the core isn't busy, it must be followed by a sequence of events.
<ZipCPU>
This is a send sequence, described by SEND(CKS,VAL)
<ZipCPU>
If you back up to line 375, you'll find the definition of that sequence.
<ZipCPU>
It consists of 10 baud intervals: a start bit, 8-data bits, and a stop bit
<ZipCPU>
The sequence itself is composed of other sequences, called BAUD_INTERVAL
<cr1901_modern>
what is the throughout keyword?
<ZipCPU>
That sequence is defined in lines 360-367
<ZipCPU>
(EXP) throughout (SEQ) means that EXP *must* be true on every clock cycle of SEQ
<cr1901_modern>
I inferred that much :P. I asked the wrong q >>
<ZipCPU>
So, instead of writing A&&B ##1 A&&C ##1 A&&D, I might write (A) throughout (B ##1 C ##1 D)
<ZipCPU>
Oh, okay, go on.
<cr1901_modern>
Does (EXP) throughout (SEQ) also mean "all of the statements in SEQ get pulled into the current assertion being defined and that SEQ must ALSO be true"?
<ZipCPU>
Yes.
<cr1901_modern>
B/c I could think of an alternate semantics that makes sense to me >>
<ZipCPU>
There's a subtlety, EXP is an expression. I don't think SEQ1 throughout SEQ2 would make much sense
<ZipCPU>
Basically, I just got tired of type A&&B ##1 A&&C ##1 A&&D ... it's also harder to read, but easier to deal with if you can pull A out separate.
<cr1901_modern>
To me, (EXP) throughout (SEQ) could mean "only check (EXP) states where (SEQ) holds." without failing if (SEQ) doesn't hold
<ZipCPU>
It's more like EXP must hold for every state of SEQ
<ZipCPU>
so if you assert A |=> EXP throughout SEQ, that will mean that EXP must be true as long as SEQ is active
<ZipCPU>
Once SEQ finishes, nothing is stated about EXP
<cr1901_modern>
So if the solver is checking a state and it knows that state isn't part of SEQ, the whole proof _doesn't_ fail?
<ZipCPU>
Ahh, your missing a key ingredient: the |=>
<ZipCPU>
That's a *VERY* key ingredient to using concurrent assertions.
<ZipCPU>
The |=> states that the sequence *MUST* follow. It sort of activates the sequence.
<ZipCPU>
Once the sequence has been activated, then the solver knows it must be in SEQ
<ZipCPU>
You can also put SEQ on the left of the |=>. I did this in my flash controller at one point. I created a sequence describing the input from the flash, and then said if this sequence happens, the flash controller must return this value on the bus.
<ZipCPU>
That was sort of like: (SEQ of flash receiving value X) |=> o_wb_ack && (o_wb_data == X)
<cr1901_modern>
>Once the sequence has been activated, then the solver knows it must be in SEQ
<cr1901_modern>
And if temp induction finds a state where we aren't in SEQ after it's activated, we fail the proof :)
<cr1901_modern>
?*
<cr1901_modern>
(Or BMC)
<ZipCPU>
So ... that's the thing ... the induction engine might start in any step of the sequence.
<ZipCPU>
If SEQ is activated, and the solver finds a state that's not a part of the sequence, the assertion will fail.
<ZipCPU>
On the other hand, if you have SEQ |=> EXP, then ... the solver might start anywhere in the middle of SEQ, and only if it can be made to fit will the assertion that EXP be applied.
<ZipCPU>
So ... write your sequences well so that you can start in the middle of them without invalidating them.
<cr1901_modern>
Ack
<ZipCPU>
This was why in txuartlite.v I had so many checks within the sequence. I wanted to make certain that if the solver jumped into the middle of the squence anywhere that there'd be no ambiguity of what was going on.
seldridge has quit [Ping timeout: 245 seconds]
<cr1901_modern>
So to summarize (I have to go briefly):
<cr1901_modern>
"(EXP) throughout (SEQ)" means "(EXP) must be true for all parts of (SEQ), if the state we are in isn't part of (SEQ), don't fail the proof"
<cr1901_modern>
Is this correct as written?
<ZipCPU>
The first part is right, the last part isn't
<ZipCPU>
The problem is that the sequence can be part of the "if" portion of the assertion.
<ZipCPU>
In that case, if the SEQ doesn't match the assertion doesn't fail--it's just not checked.
<ZipCPU>
That's why I was starting to discuss (EXP) throughout (SEQ) |=> (OTHER SEQ OR EXP)
<cr1901_modern>
I'm just concerned with the expression "(EXP) throughout (SEQ)" as written, right now :). Work my way up to using it properly
<ZipCPU>
If you are in SEQ and it doesn't continue, the expression is as though the "if (X)" part were no longer true
<ZipCPU>
Ok, let's consider A |=> (B throughout SEQ)
<ZipCPU>
In that case, your statement applies
<ZipCPU>
B must be true in every stage of SEQ
<ZipCPU>
If B is somehow not true in any stage of SEQ, or if SEQ doesn't match the data, then the assertion fails.
<ZipCPU>
s/data/design/
<cr1901_modern>
Then (B throughout SEQ) means "If we are in SEQ, B must be true". If we are not in SEQ, keep going/nothing to do?
<ZipCPU>
Yes
<ZipCPU>
Well ...
<ZipCPU>
"If we are in SEQ then B must be true" implies you have (SEQ) implies B. That's not quite it. It's more (SEQ) *and* B
<cr1901_modern>
hmmm... that would explain why |=> is so important then
<ZipCPU>
Yes.
<cr1901_modern>
it means (B throughout SEQ) will fail if either B or SEQ isn't true
<ZipCPU>
Correct
<cr1901_modern>
which is ridiculous to expect
<cr1901_modern>
to be true*
<ZipCPU>
?
<cr1901_modern>
I have trouble visualizing a design where you are always within SEQ :)
<cr1901_modern>
all the time for all states
<ZipCPU>
Good.
<cr1901_modern>
for any arbitray SEQ
<ZipCPU>
I have trouble visualizing such a design as well.
<ZipCPU>
Every sequence assertion should have a |-> or |=> as part of it.
<ZipCPU>
I like to go farther and make the sequence states very unique, so the solver can't get confused by what I mean.
<ZipCPU>
In other words, I don't want to allow the solver ever to think it's in a sequence erroneously.
<cr1901_modern>
What is |->?
<ZipCPU>
|-> is the "non-overlapping implication operator". With A |-> B there's no clock between A and B.
<ZipCPU>
With "A |=> B" a clock period passes between A and B.
<cr1901_modern>
ahh
<ZipCPU>
That is, B happens one clock after A
<cr1901_modern>
Well, SEQ kinda makes sense now. I was looking at the quiz this morning and I was like "I have no idea what half that syntax is". I'm going to opt out of this quiz, but at least I learned something tonight
<ZipCPU>
:D
<ZipCPU>
As someone else commented, A |=> B is often much easier to read than if ((f_past_valid)&&($past(A)) assert(B)
<cr1901_modern>
And there's probably some stupid edge case where those two expressions are _not_ quite semantically equivalent
<ZipCPU>
Likewise, A |-> B is often easier to read and understand then always @(*) if (A) assert(B);
<cr1901_modern>
Just like |=> and "implies" are not quite
<cr1901_modern>
errr, |->... oh screw it
<ZipCPU>
lol
<ZipCPU>
There is a subtle implementation difference as I recall, but semantically the expression pairs above are equivalent.
<sorear>
Is a sequence semantically a thing which is either true or false at each timestep of a given trace?
<ZipCPU>
sorear: That's not how I would describe it.
<ZipCPU>
Sequences take place across many time steps.
<ZipCPU>
Hence, it's not really true or false on any given timestep. To know if the sequence is "true", you have to find all of the steps of the sequence
<ZipCPU>
sorear: I'm not sure if I'd say that a sequence is true at the start or at the end.
<ZipCPU>
I just don't know how I'd express that
<ZipCPU>
There's got to be a "right" way to say it, I just might not know it.
<ZipCPU>
sorear: This is why the |=> is so important. Given A |=> SEQ, the SEQ is true if it happens following A
kc5tja has joined #yosys
<kc5tja>
Sorry for the delay, just got home. BRB, though; need to take care of some things before settling in for the evening.
<ZipCPU>
Welcome!
<ZipCPU>
cr1901_modern: I'm looking through those slides and not finding any assert property (#1 foo == 0) statements.
dxld has quit [Ping timeout: 252 seconds]
srk has quit [Ping timeout: 268 seconds]
kuldeep has quit [Ping timeout: 260 seconds]
srk has joined #yosys
dxld has joined #yosys
kuldeep has joined #yosys
<cr1901_modern>
ZipCPU: it was probably "p_req_gnt" on slide 18 that tripped me up most. But I think I've had enough formal fun for tonight.
<ZipCPU>
Ok, that describes something else.
<cr1901_modern>
My other q is: you discussed: "(SEQ of flash receiving value X) |=> o_wb_ack && (o_wb_data == X)". This only runs _after_ SEQ is finished, correct?
<ZipCPU>
That's a sequence where request is true, then three clocks later grant is true, followed by the request being deasserted and then the grant is deasserted on the last clock.
<cr1901_modern>
ahhh, without the "sequence" keyword
<ZipCPU>
cr1901_modern: The assertion is only applied once the SEQ has completed successfully
<ZipCPU>
That's if you will the "if" part of the assertion
<cr1901_modern>
Is that what "SEQ on left side" means? Or can it also mean "if we are in (SEQ)"?
<ZipCPU>
If (SEQ) ever takes place, then o_wb_ack && (o_wb_data == X) must be true on the clock following the end of the sequence
<ZipCPU>
SEQ |=> A means not if we are in the sequence, but rather once SEQ completes A must then be true on the next clock
<cr1901_modern>
Okay, so the semantics of how (SEQ) returns true or not depends on the context of when it's used.
azonenberg_work has quit [Ping timeout: 240 seconds]
<ZipCPU>
I guess
<cr1901_modern>
(SEQ) |=> A returns true once we've finished SEQ, A |=> SEQ is true if we are in an SEQ if "A" is true
<cr1901_modern>
err, I said that wrong. But I need some time to think
<cr1901_modern>
so nevermind :P
<kc5tja>
(will be multitasking -- cooking dinner as well)
<ZipCPU>
kc5tja: Give me a moment to download the files
<ZipCPU>
kc5tja: I recommend `default_nettype none for all verilog files. We can discuss more if you aren't familiar with it.
<cr1901_modern>
ZipCPU: Okay I found my confusion:
<cr1901_modern>
But in your flash controller example: (9:13:27 PM) ZipCPU: SEQ |=> A means not if we are in the sequence, but rather once SEQ completes A must then be true on the next clock
<cr1901_modern>
(8:40:34 PM) ZipCPU: "If we are in SEQ then B must be true" implies you have (SEQ) implies B.
<cr1901_modern>
Is this the different between SEQ |-> B andSEQ |=> B
<cr1901_modern>
?
<ZipCPU>
The 8:40:34 comment was parsing your statement, and trying to explain why the statement didn't accurately describe how things worked
<ZipCPU>
SEQ |-> B means that B must be true on the last clock of SEQ, whereas SEQ |=> B means that B must be true on the clock after SEQ completes.
<ZipCPU>
So for example STB |-> CYC means if the wishbone strobe is ever true, cyc must also be true
<ZipCPU>
Perhaps that's a poor example--there's no sequence in it, but it does illustrate |->
<cr1901_modern>
How do you represent the expression "If we are in _any_ state of (SEQ), then "B""? "B throughout SEQ" doesn't work b/c if the solver finds any state where SEQ fails, the whole proof fails.
<ZipCPU>
The question doesn't have meaning
<ZipCPU>
What you want to say is that during SEQ assert B must be true
<ZipCPU>
The only way I can think of doing that would be to say if (SEQ.triggered) assert(B), but other than knowing that yosys supports something like that, I have yet to try it.
<ZipCPU>
Another way might be to find what triggers SEQ, and then insist that B be true for a number of clocks after that.
<cr1901_modern>
Yea it seems that (SEQ) only returns true on the last cycle of (SEQ), has indeterminate truth value while within (SEQ)*, and false if we are not in (SEQ)
<ZipCPU>
That captures what I think I've been trying to say.
<ZipCPU>
You really don't know if a sequence has taken place until ... it's taken place. ;)
<sorear>
does a sequence have a fixed finite length in timesteps?
<ZipCPU>
sorear: It can be either finite or infinite in length.
<sorear>
do sequences do anything in simulation, or only formal? do they do the same thing?
<cr1901_modern>
* I assume it has to be indeterminate truth value within (SEQ)* b/c an SMT solver checking the middle of a sequence _isn't finished_ figuring out whether the sequence holds.
kuldeep has quit [Ping timeout: 240 seconds]
<cr1901_modern>
But Idk how semantically this is represented in SystemVerilog spec, or how an SMT solver can handle "unknown truth value"
<ZipCPU>
sorear: The difference between simulation and formal is the difference between assume and assert, not in the definition of what a sequence is
kuldeep has joined #yosys
<cr1901_modern>
(other than, well not assigning it truthiness :)...)
<ZipCPU>
cr1901_modern: When clifford spent time learning that, he returned that much of it depends upon what "triggers" the sequence
<ZipCPU>
I don't quite have that in depth of an understanding (yet)
<cr1901_modern>
I would assume indeterminate truthiness to your asserts doesn't fail a proof
<ZipCPU>
Depends, are they the antecedent or the consequence?
<ZipCPU>
Likewise, if they are the consequence, you might have A |=> SEQ. In that case, the SEQ can fail the assertion before it completes.
<cr1901_modern>
I don't see the problem with that
<sorear>
(it took me a long time to figure out that non-formal Verilog is a _language for writing general discrete-event simulations_, and the fact that it can be synthesized is almost accidental)
<ZipCPU>
:D
<kc5tja>
ZipCPU: I'm familiar with it, I'm just lazy.
<ZipCPU>
Ok
<ZipCPU>
That works
<kc5tja>
More precisely, forgetful.
<cr1901_modern>
ZipCPU: In that case, the SEQ can fail the assertion before it completes. <-- and that means SEQ has a known truth value at that point
<ZipCPU>
I'm looking at a failing trace now.
<ZipCPU>
Well, it's like you said, it can be true when complete, false, or not yet determined
<ZipCPU>
If it can be determined to be false, the assertion then fails.
<cr1901_modern>
In any case, I was mostly thinking antecedent; if truthiness is unknown, the SMT solvers "figures out as many assertions that it can given incomplete information", and leaves the remaining asserts alone
<ZipCPU>
kc5tja: I haven't had a chance to study this code much. Care to give me a bit of a walk-through?
<cr1901_modern>
I would assume "we don't know yet" would be a poor reason to fail a proof ;)
<ZipCPU>
cr1901_modern: No, I think it does better than that.
<cr1901_modern>
Just imagine if computers in general gave up if they didn't know all the answers immediately
* ZipCPU
's computer just gives up/
<cr1901_modern>
ZipCPU: Idk the formal name, but there's a theorem in logic that states: If theres a boolean expression with some unknown variables, and all combinations of the unknown variables result in the expression being exclusively True or False, then the whole expression is True or False
<cr1901_modern>
i.e. (A & 0) is false
<cr1901_modern>
even if we don't know A
<kc5tja>
ZipCPU: The module in question is intended to be the TileLink interface that (eventually) will bind all the other leaf cores together. Right now, I'm just focusing on providing write access to writable registers (I've not started work on the read path yet).
<ZipCPU>
Ok
<ZipCPU>
So this is a bridge module?
<cr1901_modern>
A solver can prove some asserts hold even if we don't know the truthiness of other expressions using that law, but I don't see how the solver can do "better than that", to quote.
<sorear>
that's just a form of the law of the excluded middle
<sorear>
and SMT solvers do not use intuitionistic logic
<kc5tja>
So, for example, if you write to TXOUT while it's idle, your transaction will be acknowledged right away; however, if you write to it again while the transmitter is still shifting bits out, the request on the A-channel is accepted, but the corresponding D-channel acknowledgement will be delayed until the transmitter shift register has accepted the new data. In that way, the code doesn't need to worry about
<kc5tja>
baud rate, it can just blinding blast data to TXOUT in a tight loop.
<cr1901_modern>
sorear: A. Why not?, and B. Nevermind then. Indeterminate truth must indiscriminately cascade then.
<ZipCPU>
Ok, so ... it's a pipelined interface that can accept a request and then queue it for a later acknowledgement?
<ZipCPU>
kc5tja: How many requests can be queued?
<kc5tja>
1
<ZipCPU>
Ok, so there's the accepted request that's being acted upon, and one other that can be queued up?
* ZipCPU
examines is_put
<kc5tja>
Right. So, for example: SB t0,0(a0) { kicks off first character } SB t0,0(a0) { halts CPU until first character is done transmitting. }
<ZipCPU>
What does the SB acronymn stand for? Slave byte?
<ZipCPU>
Sorry, Im' not familiar with that notation
<ZipCPU>
Question: Why does is_put depend upon slave_ready? Shouldn't it depend only on o_a_ready to represent the slave?
kuldeep has quit [Ping timeout: 252 seconds]
<ZipCPU>
kc5tja: I have two examples you might be interested in looking at. One is a bus arbiter, another a bus delay. Both are found in https://github.com/ZipCPU/blob/dev/rtl/ex
<ZipCPU>
Each uses a formal bus interface definition file.
kuldeep has joined #yosys
<kc5tja>
Store Byte
<kc5tja>
RISC-V assembly notation.
<ZipCPU>
That bus interface definition returns three values on its output ports: the number of requests that have been made, the number of acknowledgments received, and the number of outstanding requests.
<ZipCPU>
Ok, thanks!
<ZipCPU>
These three values I then need to tie together with any piece of code that uses the property file, or the code will fail induction
<kc5tja>
slave_ready is the 1-hot state (o_a_ready = slave_ready).
<kc5tja>
(answering in order, sorry if I'm colliding with already answered Qs)
<ZipCPU>
If the two are equivalent, then have you asserted thatt fact?
<ZipCPU>
Heheheh
<kc5tja>
Not *directly*, but indirectly, yes.
<ZipCPU>
So, in every WB interaction, the bus master asserts that the number of requests, acknowledgements, and the number of outstanding transactions must match its internal state.
<kc5tja>
slave_ack is the state responsible for driving and waiting for the D-channel handoff.
<kc5tja>
slave_txout is the state responsible for waiting for the TXOUT shift register to be ready for another character.
<kc5tja>
Same with TileLink. The SIA only handles one request at a time. An external arbiter is responsible for gate-keeping the SIA amongst multiple masters.
<ZipCPU>
Let's see ... on reset, the slave is ready, has no acknowledgments to return, and ... slave_txout ... says the serial port is not busy?
<kc5tja>
No
<kc5tja>
slave_txout is a slave interface *state*. i_txd_ready indicates the readiness of the serial port.
<kc5tja>
The slave interface idles in slave_ready.
<kc5tja>
When a PUT operation comes in on the A-channel, a check is made to see if it's the TXOUT register.
<kc5tja>
If not, then we advance directly to slave_ack.
<kc5tja>
If so, we advance to slave_txout, which is responsible for handing the byte off to the transmitter.
<kc5tja>
Only when the transmitter acknowledges receipt of the data does it then advance to slave_ack.
<kc5tja>
After slave_ack gives the acknowledgement for the previous A-channel request on the D-channel, will it return to slave_ready.
<ZipCPU>
Ok, so ... now let me look at the trace again
<ZipCPU>
I see a failure of properties.vf 134, right?
emeb has quit [Quit: Leaving.]
<ZipCPU>
That says that if we are not in a reset, z_past_valid indicates ... hold on, let me check that one.
<ZipCPU>
Why is z_past_valid 32-bits?
<ZipCPU>
In my trace, it just happens to roll over on the last timestep.
<ZipCPU>
I don't think you want that, right?
<ZipCPU>
kc5tja: Can you explain z_past_valid to me?
<ZipCPU>
It's not the f_past_valid I use, where always @(posedge i_clk) f_past_valid <= 1'b1;
<kc5tja>
I needed to wait more than 10 steps in the past, and I was tired of adding z_past_valid_2, z_past_valid_3, etc.
<ZipCPU>
I think you want your counter to saturate.
<kc5tja>
Even if it does, it still fails induction the same way, just with a *slightly* different trace.
<ZipCPU>
Ok, let me keep looking then
<ZipCPU>
Let me ask you this ... what's wrong on the left half of the trace?
<ZipCPU>
Something is wrong there.
<ZipCPU>
(I can't see it yet)
<ZipCPU>
Ahh ...
<ZipCPU>
o_d_valid is constantly high. This looks familiar
<ZipCPU>
No, maybe not, i_d_ready is low
<kc5tja>
This one definitely stumped me. Spent about two days on this, hoping that *something* would come to me, but nada.
<ZipCPU>
So, if you look at the left half side of the trace, you don't see the problem?
<ZipCPU>
Let me explain
<ZipCPU>
During induction, you can split the trace into two parts.
<ZipCPU>
If the bug is in the left half, then the problem is a missing assertion
<kc5tja>
I see a lot of problems. What I don't see is how to assert them away that is meaningful.
<ZipCPU>
Ok, good, tell me what you see.
<kc5tja>
I see no activity for 200-ish steps, for one. I'd expect some kind of early failure or some kind of state exploration.
<ZipCPU>
Yes, that's a key indicator
<ZipCPU>
Usually it means that all the relevant stuffs happens in just a couple of clocks
<kc5tja>
There's no initial reset, which is absolutely essential for any stateful logic to work right.
<ZipCPU>
But you might never see that during induction
<ZipCPU>
Instead, you need to assert that illegal states are invalid.
<ZipCPU>
But let me ask a question: What is o_d_ready?
<kc5tja>
o_d_valid is high for some reason.
<kc5tja>
i_d_ready you mean?
<ZipCPU>
What is o_d_ready?
<ZipCPU>
No, I mean o_d_ready?
<ZipCPU>
A bug you would've caught with `default_nettype none
<kc5tja>
Good eye, thanks. IMO, that should be an enforced default. Would love to have an sby option that enforces this, because I am *****extremely***** prone to forgetting this.
<ZipCPU>
There is such an option, it's called `default_nettype none, and it's defined by the Verilog standard
<ZipCPU>
;)
<ZipCPU>
So if I change o_d_ready to o_d_valid, your design passes--BMC + Induction
rohitksingh has joined #yosys
<kc5tja>
Yes, I just noticed that. So it looks like I did my formal stuff OK then, I was just bungled up with a Verilog defect.
<ZipCPU>
;)
<ZipCPU>
Sounds like I solved your "problem" :) Do you have any other questions about induction tonight?
rohitksingh has quit [Quit: Leaving.]
<ZipCPU>
kc5tja: Ok, it's late here. If you have no other questions, I'll head to bed.
<kc5tja>
nope I'm good. Thanks!
<kc5tja>
Sorry, was finishing dinner. Wife just came home.
kuldeep_ has joined #yosys
kuldeep has quit [Ping timeout: 260 seconds]
kc5tja has quit [Quit: leaving]
sandeepkr has quit [Ping timeout: 252 seconds]
kuldeep_ has quit [Ping timeout: 244 seconds]
pointfree has joined #yosys
rohitksingh_work has joined #yosys
sandeepkr has joined #yosys
kuldeep has joined #yosys
esden has quit [Ping timeout: 260 seconds]
esden has joined #yosys
danieljabailey has quit [Ping timeout: 240 seconds]
danieljabailey has joined #yosys
azonenberg_work has joined #yosys
azonenberg_work has quit [Ping timeout: 240 seconds]
azonenberg_work has joined #yosys
Ultrasauce has joined #yosys
AlexDaniel has joined #yosys
AlexDaniel has quit [Ping timeout: 244 seconds]
<cr1901_modern>
So AFAICT (no, I never sleep), nextpnr is deterministic in how it places and routes, if given the same design/command line arguments. stdout is more or less identical in both cases. Why do the checksums for each phase differ then?
rohitksingh_work has quit [Read error: Connection reset by peer]
AlexDaniel has quit [Ping timeout: 245 seconds]
seldridge has joined #yosys
<q3k>
til
<q3k>
whoops.
mmaterzok has joined #yosys
FPGA_n00b has joined #yosys
<mmaterzok>
Hello! I have implemented a graphical logic simulator, which uses Yosys to convert Verilog to a block diagram: http://digitaljs.tilk.eu/
<ZipCPU>
mmaterzok: Can it handle complex designs?
<mmaterzok>
It handles multi-module designs, modules are displayed as boxes, and you can look inside them. Design loading performance needs to be improved, but I have loaded a simple CPU and it simulated fine.
gruetzkopf has quit [Read error: Connection reset by peer]
gruetzkopf has joined #yosys
<mattvenn>
looks cool!
<mattvenn>
I can't seem to zoom
<mattvenn>
is there a way to zoom out
<shapr>
mmaterzok: that's cool! and already on github!
<shapr>
it's especially cool that I can click on blocks and see the logic inside a block
<mmaterzok>
mattvenn: no zooming currently, looks like another feature for TODO ;)
<mmaterzok>
shapr: thanks! that was one of the design requirements for me
seldridge has quit [Ping timeout: 240 seconds]
seldridge has joined #yosys
<q3k>
mmaterzok: ... have you tried running picosoc/picorv32 in it? ^^
<mmaterzok>
not yet, i have to try :)
AlexDaniel has joined #yosys
<edmoore>
only slightly relatedly (apologies), does anyone know of any soft open cores that have been flown on satellites?
<sorear>
LEON?
<edmoore>
i guess that was obvious in hindsight
<edmoore>
i suppose i mean more at the hobbyist end
<edmoore>
probably still LEON :)
<q3k>
hobbyist satellites?
<ZipCPU>
There are several
<edmoore>
tens-to-hundreds probably
<q3k>
and I thoughts my hobbies were expensive
<edmoore>
:)
<edmoore>
i think most of the people who launch them are probably not shouldering the actual market price of the launch
<edmoore>
(the launch being the expensive bit)
<shapr>
q3k: expensive electronics hobbies?
<shapr>
I bought a bladecenter and a bunch of blades once, that was expensive but fun.
<sorear>
I think launching a cubesat isn’t that much more expensive than building a fab
<q3k>
shapr: pff
<edmoore>
the logic analyser pod for my tektronix scope is $600. looking at it, i'm struggling to find where the other $550 goes to
<q3k>
shapr: I have a 5-blade Itanium chassis
<q3k>
shapr: and there's three Dell M1000e blade boxen in hswaw
<shapr>
wow, I had a seven blade Cell Broadband Engine chassis, but gave it away recently
<edmoore>
it's just a high density connector broken out to some witches-hat clips. admittedly with some care taken over impedance, probably
<q3k>
shapr: although one of the chassis was just 100eur, so that's cheap
<shapr>
I spent more like $6k on my collection, just to give it away later.
<q3k>
shapr: (still, 16 machines at 24 cores and 24 gigs of RAM each)
<sorear>
strong contender for Worst Non-gaming Product Name
<q3k>
shapr: yeah, I do that too with stupid equipment I don't need :P
<shapr>
edmoore: I often wonder about that kind of thing myself
<shapr>
I still haven't replaced the fan on my risc-v board
<q3k>
edmoore: is that for an MDO3000?
<edmoore>
sorear: i've never understood that (gaming)
<q3k>
I need to get one for mine.
<edmoore>
q3k: how did you know?
<edmoore>
yes i do too
<q3k>
edmoore: I have an MDO3k on my desk, I know the pain.
<shapr>
I liked bunnie huang's design ideas for logic probes for the novena
<edmoore>
i don't actually have it, because i can't bring myself to spend that kind of money on something i can usually get by without, useful as it would be
<q3k>
edmoore: the countless nights with a drink in my hand and my cursor hovering over the 'buy' button on farnell
<edmoore>
q3k: yes!!
<edmoore>
we need a support group
<q3k>
G33katwork did buy one in the end.
<edmoore>
or go halves on one and using the saving to fund several years worth of fedexing it to each other
<q3k>
And also got a bunch of other second-hand probes from ebay (like current and EM probes, the bastard)
<shapr>
edmoore: I've had surprising success with that
<edmoore>
in all other regards i love my mdo3104, i got it for a song, but i resent the price of tek accessories
<shapr>
that is, swapping expensive hardware with friends when I get bored
<edmoore>
shapr: well, in this case i don't think i'd get bored but i only need it about 5% of the time
<edmoore>
i'd never part with the scope
<shapr>
Oh, you WANT 150 kilos of IBM hardware? drive over with your van!
<q3k>
edmoore: oh, you have the 1GHz frontend
<q3k>
edmoore: I have the 500Mhz one
<edmoore>
q3k: yes, i got the maxxed one with the everything-enabled hack on eevblog for about $2k, a few years ago, thanks to a pricing error on one of the UK websites
clifford has quit [Quit: Ex-Chat]
<edmoore>
i did a little dance
<q3k>
edmoore: heh
<q3k>
edmoore: I got my at 200MHz for... 4kEUR?
<shapr>
I do that when I get weird rare books
<edmoore>
the speccan has been jolly useful actually, and got me back to using my ham license
<shapr>
that book is an expanded version of the speech in that link
<edmoore>
shapr: oh yes, i have read that
<edmoore>
assuming it's the talk
<edmoore>
yes
<edmoore>
well i tried to pick and interesting problem to work on but i'm not really one for leaving the door open
<shapr>
it works surprisingly well
<shapr>
surprisingly, the coxeter book was expensive, and the digital magnetic logic book was cheap
<shapr>
oh, time for lunch
<shapr>
edmoore: but I want to hear about more items that produced happy dances at some point
<edmoore>
sorear: re: gaming, i got a new mouse recently and wanted a good responsive one (I am not a gamer at all, but do cad and whatever) and so ended up looking at gaming ones, and all of them have completely absurd names
<shapr>
that's azonenberg's next random board name?
* shapr
cackles and escapes
<edmoore>
shapr: well, my friend dave and I were first to solve the quest/riddle/ctf thing at EMF camp this year, and when we finally found the padlocked chest and opened it using the code we had worked out from the previous 10 mini-quests/clues, we both very definitely did a little dance
<edmoore>
i became ron swanson in that episode where he helps thingy solve the valentine clues
<edmoore>
i had only just met dave, a friend-of-a-friend who worked for pixar, but we are now blood brothers after this quest
<edmoore>
like legolas and gimli
<gruetzkopf>
shapr: i have stuff that still uses magnetic digital logic
m4ssi has quit [Remote host closed the connection]
<ZipCPU>
Let's see how hard it is to do prove an FFT butterfly, with a soft multiply capability within it.
emeb has joined #yosys
<ZipCPU>
Looks like I got through the first 11 steps or so before hitting a wall.
maikmerten has joined #yosys
fouric has left #yosys ["WeeChat 2.2"]
mmaterzok has quit [Quit: Leaving]
<shapr>
edmoore: ha, this sounds awesome
<shapr>
gruetzkopf: what do you have that uses magnetic digital logic?
<shapr>
I need to go through the book again, there was much surprise and enlightenment
<awygle>
good morning :)
<shapr>
GOOD MORNING!
<shapr>
it's a beautiful day here on the internet
<shapr>
traffic is light for now, and there's a low chance of BGP hijacks today
seldridge has quit [Ping timeout: 252 seconds]
<sorear>
morning
<cr1901_modern>
daveshah: FWIW, I've been testing seeds by routing PLLGLOBALOUT without an intermediate SB_GB in my SoC. All 4 seeds I've tried failed at my target clk.
<cr1901_modern>
My theory is that using a second SB_GB, while technically wasteful of precious resources, allows the design to pass timing (even though icetime claims it fails)
<cr1901_modern>
I'll upload my SoC soon (within the day) if you're curious to see
<gruetzkopf>
designed in the 60s, still widely used in germany
<shapr>
most interesting thing in that book: 'human' scale magnetic digital logic can't switch faster than 127kHz
<shapr>
spintronics is a new form of the same magnetic digital logic, with the advantage that switching is MUCH faster
<awygle>
spintronics is dope
<shapr>
as far as I know, paramagnetics and ... what's the other one? were discovered long years after digital magnetic logic had it's 5-10 year heyday
<shapr>
so I'm curious if those would make any difference
<awygle>
MRAM and FRAM (which is not spintronic) are two of my favorite technologies
<awygle>
diamagnetics?
<shapr>
molecular magnetics?
<shapr>
isn't that where the sum of the magnetic moments makes it a magnet?
<shapr>
in any case, all that matters is the fat S curve
<sorear>
I'm unsold on "magnetic logic and spintronics are the same thing"
<shapr>
sorear: fair enough, I'd be interested in any proof by contradiction
<sorear>
like I don't think magnetic logic cares about the spin of charge carriers at all
fsasm has joined #yosys
rohitksingh has joined #yosys
rohitksingh has quit [Ping timeout: 246 seconds]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
rohitksingh has joined #yosys
rohitksingh has quit [Quit: Leaving.]
fsasm has quit [Ping timeout: 252 seconds]
kuldeep has quit [Ping timeout: 252 seconds]
kuldeep has joined #yosys
maikmerten has quit [Remote host closed the connection]