proteusguy has quit [Remote host closed the connection]
<ZirconiumX>
ZipCPU: I find it difficult to think of useful properties to prove about something. I can come up with some assertions to test preconditions (for example, two pipelines writing to the same register breaks the LVT, so it must be prohibited)
lutsabound has quit [Quit: Connection closed for inactivity]
<ZirconiumX>
But I have no clue about postconditions; more specifically, *useful* postconditions. I feel like trying to prove what the code explicitly states is a tautology, such as proving you can read from a register.
<ZirconiumX>
For useful things like the instruction decoder, trying to prove that only legal instructions are accepted requires something like a giant table of legal instructions for the test bench to work on.
<sorear>
ZirconiumX: have you read through riscv-formal?
<ZirconiumX>
I have, yes
proteusguy has joined #yosys
<sorear>
I thnk the same methodology could be applied to sh?
<ZirconiumX>
Sure, but first I need to grok the methodology
<ZirconiumX>
I was given my rough task for the summer: I need to run a 256 byte Dreamcast demo.
<ZirconiumX>
It's only 34 instructions
<sorear>
1. local correctness: for each retired instruction, does it read the correct registers, does it write the right register to the right place, does it make the correct memory access?
<sorear>
2. consistency: given a sequence of instructions, if instruction A writes register or memory location X, and instruction B reads it, and there are no intervening writes, B reads the value A wrote
<ZirconiumX>
But some of those instructions include fun things like IEEE 754 division .-.
<sorear>
3. forward progress: in any N cycle period, at least one instruction is retired
<sorear>
verifying a FPU is a bit different from verifying a pipeline
<sorear>
pipelines are extremely complicated but have relatively few actual state bits and sparse coupling between them, so model checkers work well
<sorear>
(modern) FPUs are close to combinatorial, so pipeline verification is simple, but "was the correct operation computed" is far beyond what model checkers can work with
<ZirconiumX>
It doesn't help that 754 arithmetic is perhaps a little vague; you don't have to be accurate, just accurate enough.
<sorear>
you said "division" though, division is required to be correctly rounded
<sorear>
there's some ambiguity around subnormals handling (unclear if the spec actually allows multiple results or people just think it does because it's not clear enough) but for finite results there's only one allowed
<sorear>
even if it weren't, you have a goal of giving the same results as sh4 and sh4 hopefully documents what it does
<sorear>
"accurate enough" is for functions like sin()
* sorear
stares at FPSCR.PR
rohitksingh_work has joined #yosys
rohitksingh has joined #yosys
emeb_mac has quit [Ping timeout: 258 seconds]
tecepe_ has joined #yosys
edmoore_ has joined #yosys
elms_ has joined #yosys
thoughtpolice_ has joined #yosys
pepijndevos_ has joined #yosys
sorear has quit [*.net *.split]
flaviusb has quit [*.net *.split]
edmoore has quit [*.net *.split]
elms has quit [*.net *.split]
tecepe has quit [*.net *.split]
thoughtpolice has quit [*.net *.split]
pepijndevos has quit [*.net *.split]
edmoore_ is now known as edmoore
tecepe_ is now known as tecepe
elms_ is now known as elms
thoughtpolice_ is now known as thoughtpolice
sorear has joined #yosys
flaviusb has joined #yosys
dys has quit [Ping timeout: 245 seconds]
jakobwenzel has joined #yosys
rohitksingh has quit [Ping timeout: 258 seconds]
m4ssi has joined #yosys
rohitksingh has joined #yosys
azonenberg_mobil has quit [Ping timeout: 276 seconds]
vup has quit [Ping timeout: 258 seconds]
vup has joined #yosys
rqou has quit [Quit: ZNC 1.7.x-git-709-1bb0199 - http://znc.in]
rohitksingh_work has quit [Read error: Connection reset by peer]
rohitksingh_work has joined #yosys
rohitksingh has quit [Ping timeout: 245 seconds]
rohitksingh has joined #yosys
alexhw has joined #yosys
rqou has joined #yosys
rohitksingh_work has quit [Read error: Connection reset by peer]
rohitksingh_work has joined #yosys
rohitksingh has quit [Ping timeout: 258 seconds]
Kitlith has quit [Ping timeout: 244 seconds]
Kitlith has joined #yosys
nurelin_ has quit [Ping timeout: 245 seconds]
nurelin_ has joined #yosys
GoldRin has joined #yosys
proteusguy has quit [Remote host closed the connection]
GoldRin has quit [Ping timeout: 272 seconds]
proteusguy has joined #yosys
<pepijndevos_>
ZirconiumX, looking at bit-serial architecture now...
<pepijndevos_>
ZirconiumX, another question: did you look at part availability when chosing the AC variations and particular chips?
<pepijndevos_>
Wow...that's a short wikipedia page right there.
<pepijndevos_>
Sad story: Kicad includes a whole 74xx library, but no AC parts
<ZirconiumX>
pepijndevos_: I did look at part availability; AC is still manufactured by TI and ON Semi
<ZirconiumX>
And for KiCad, remember that 74 series parts are *mostly* pin compatible
<ZirconiumX>
Though they don't have the AC11 series
<pepijndevos_>
Yea... I figured I could probably get away with any of the variations they might have.
<ZirconiumX>
And AC11 is pretty important
<pepijndevos_>
AC11 is the 16 bit stuff?
<ZirconiumX>
No, that's AC16
<ZirconiumX>
AC11 is an alternative layout that puts VCC and GND in the middle of the chip
<pepijndevos_>
... why is that important?
<pepijndevos_>
Speed and ground bounce and stuff?
<ZirconiumX>
Ground bounce, yeah
<ZirconiumX>
Having VCC and GND in the corners of the chip means that for gates on the opposite sides of the pins have longer voltage path
<ZirconiumX>
Add that to the very fast switching time of AC logic, and you end up with something that can bounce while switching
<pepijndevos_>
Right... I agree it makes sense... it's just not very convenient for generating KiCad netlists.
<pepijndevos_>
I guess I'll have to hunt for or make library parts or switch to more impractical parts.
<ZirconiumX>
Making KiCad libraries is easy
<ZirconiumX>
Getting them merged is harder
<ZirconiumX>
:P
<pepijndevos_>
I guess. Well, I'll just start playing with the parts that are there. Last time I tried to do anything in KiCad it was a nightmare.
<pepijndevos_>
I found skidl, which can programmatically make netlists, saving me a lot of trouble.
<ZirconiumX>
Morning, ZipCPU
<ZipCPU>
Morning!
<ZipCPU>
I remember when I verified a pipelined CPU (my own), I was concerned that instructions would be dropped or duplicated as they went through the pipeline
<ZipCPU>
Since then, I've added another worry: that the pipeline doesn't get stuck
<ZipCPU>
The CPU pipeline logic was complex enough as it is/was so these were important criteria for me
<ZipCPU>
As for the reset, have you thought of: if ($past(i_reset)) assert(issue_instruction_request && request_address == RESET_ADDRESS); ?
<ZirconiumX>
I have not, no
<ZipCPU>
Here's another one: if ($past(i_reset)) assert(pipeline_stage_is_valid == 0);
<ZipCPU>
Since the ZipCPU has multiple pipeline stages, I did that for each
<pepijndevos_>
sigh, no 74xx16xxx parts either...
<ZipCPU>
Or, here's another: if ($past(pipeline_stage_valid)) assert($stable(pipeline_stage_data) || next_pipeline_stage_has_the_new_data);
<ZirconiumX>
Huh, that's interesting
<ZirconiumX>
sorear will be pleased to know that me and $employer have agreed on me having to implement only a subset of SH4
<ZirconiumX>
Unfortunately this subset is still fairly complex
<ZirconiumX>
ZipCPU: I get the feeling your general philosophy is to build the pipeline and then prove it correct, rather than worry about that as you go
<ZipCPU>
Perhaps because I had the pipeline already built when I discovered formal
<ZipCPU>
Were I to do it again, I might start with something closer to riscv-formal
<ZipCPU>
That's a nice end-to-end approach, vs my own which was more internals based
<sorear>
Roughly what’s the subset?
rohitksingh_work has quit [Read error: Connection reset by peer]
<ZirconiumX>
sorear: Boolean logic operations, addition/subtraction, some immediate operations, an integer fused multiply-accumulate unit, plus a basic floating-point unit with addition, subtraction, multiply and divide
<sorear>
what significant things does that *exclude*? the MMU?
<ZirconiumX>
MMU, the concept of instruction privilege, and quite a lot of the status registers
<ZirconiumX>
ZipCPU: When should you use a bounded model check and when should you use induction?
<ZipCPU>
A bounded model check can find assertion failures, and can often be done with basic "white-box" testing approaches
<ZipCPU>
Induction can prove that there are no assertion failures within a design ... ever, but it's a much more intrusive "white-box" approach
<ZipCPU>
Sorry, BMC is "black box" not white box
* ZipCPU
looks for the editing button on IRC, to edit his prior comment
<ZipCPU>
I tend to do everything via induction if possible, but ... it's not always possible
vonnieda has quit [Quit: My MacBook Pro has gone to sleep. ZZZzzz…]
rohitksingh has joined #yosys
emeb has joined #yosys
vonnieda has joined #yosys
maikmerten has joined #yosys
<pepijndevos_>
ZirconiumX, why are you using a 373 transparent latch as a dff rather than a 374 rising edge triggered flip-flop? Not sure it matters too much, just checking...
<pepijndevos_>
And I noticed that adding a reset to my simple counter adds a lot of logic. I wonder if a resettable flip-flop could get rid of a lot of that.
m4ssi has quit [Remote host closed the connection]
gsi__ is now known as gsi_
<ZirconiumX>
pepijndevos_: That must be a typo; I meant the 374
rohitksingh has quit [Ping timeout: 246 seconds]
<pepijndevos_>
Lol... it turns out kicad does not have an autorouter at all. I found a forum thread that argued that it's not needed as much these days as back when people made stacks of 74xx boards.
<ZirconiumX>
pepijndevos_: Google FreeRouting
<ZirconiumX>
The KiCad built-in autorouter was terrible, so they binned it
<pepijndevos_>
Yea, from what I can tell freerouting is some old java applet that's been open sourced
<pepijndevos_>
Maybe it's not as bad as it seems...
<tpb>
Title: Verilog to PCB - Album on Imgur (at imgur.com)
<ZirconiumX>
pepijndevos_: Now *you're* using 373s :P
<pepijndevos_>
But uuh, yea, will change that to 374 haha
fsasm has joined #yosys
<pepijndevos_>
wat... I no git.
<ZirconiumX>
pepijndevos_: ?
<pepijndevos_>
ZirconiumX, you merged the pr in a way that when I pulled it it said my branch was 8 commits ahead. So I did some magic from stack overflow and now I'm on a fresh branch with my KiCad work. PR sent :)
<pepijndevos_>
Verry WIP
<ZirconiumX>
I don't merge PRs
<ZirconiumX>
I rebase
<pepijndevos_>
Right. I always struggle with a rebase workflow and end up force pushing a lot *facepalm*
<pepijndevos_>
74AC11074 seems to be barely used, and does not have an area set
<maikmerten>
verilog to PCB... huh? Is that really a thing?
<pepijndevos_>
Almost kinda hahaha
<ZipCPU>
I've heard of it from the standpoint of formal
<ZipCPU>
... as in, formally verify your PCB traces before sending the design out for manufacture
<maikmerten>
"designing logical circuits with NORs and 555s exclusively"
<pepijndevos_>
maikmerten, kinda... ZirconiumX made a yosys liberty cell library for 74xx logic chips
rohitksingh has quit [Ping timeout: 248 seconds]
<pepijndevos_>
and I'm currently trying to generate a kicad netlist from it
<pepijndevos_>
There is a thin line betwee genius and crazy, and you might be just on the right side... I think, maybe.
rohitksingh has joined #yosys
<pepijndevos_>
I'm wondering what would be a good balance of size and complexity for a first PCB to order. Preferrably something with only a hand full of chips with as much variety as possible. It'd be a bit sad to order your risc-V board and find all the flip-flops have their footrpint backwards.
<maikmerten>
hmmm... perhaps something like an IR decoder (e.g. NEC protocol) or a SPI controller?
<maikmerten>
something like "shift 8 bits in, transmit via SPI, shift received bits out"
<pepijndevos_>
And it uses like 10 different chips, so that might in fact be a good candidate.
<maikmerten>
right. I forget how awesome highly-integrated ICs are.
<pepijndevos_>
But stuff like the Gigagron uses very few chips for what it can do, so maybe there is still room for improvement. Or it requires very dedicated verilog compared to random code from the web.
<maikmerten>
(I also forget how awesome nextpnr vs. arachne-pnr is. Currently building picoSOC with the traditional toolchain and arachne-pnr takes three minutes to route)
<maikmerten>
I assume you'd need to be very 74xx-minded to get compact results
<pepijndevos_>
Reset? Who needs it...
<pepijndevos_>
ugh... 74xx chips are so complicated... why not do something simple like relay logic
<ZirconiumX>
maikmerten: It helps that 74xx chips are generally tri-state
<ZirconiumX>
Which Yosys tends not to handle wel
<ZirconiumX>
l
<maikmerten>
oh, right
<ZirconiumX>
I remember seeing a chip list for the PDP-11/45
<ZirconiumX>
But I can't find it
rohitksingh has quit [Remote host closed the connection]