<porglezomp>
Basically it's running off of the idea "the real numbers are more elegant" and "let's do all computations with floating point numbers"
<porglezomp>
so they derive a universal gate that's basically NAND for NaN/Inf instead of 0/1.
citypw has joined #yosys
<cr1901_modern>
So a 64-input NAND gate that outputs 32-bits in the NaN/Inf bit pattern?
<porglezomp>
The paper derives a 3-bit floating point format, so 6-input and 3-output.
<porglezomp>
but yeah essentially
<cr1901_modern>
I read your tweet re: yosys. You seem to be playing a fun game of "Why did yosys optimize my entire design away?", correct?
vidbina has quit [Ping timeout: 255 seconds]
<porglezomp>
oh i mean it optimized the useless parts away
<porglezomp>
it turned the floating-point based design back into the binary design, modulo about a hundred LUTs
<porglezomp>
flattening + the optimizer passes do a really admirable job with that
<cr1901_modern>
And you want to keep everything?
<porglezomp>
yeah, that'd be nice. I need it to get to valid ECP5 synthesis in the end, and that's what's causing me trouble.
<cr1901_modern>
If you want to keep everything, yosys understands the "keep" attribute on modules.
<porglezomp>
Because I need to flatten it and techmap it, but can't optimize it flattened, and running synth_ecp5 -noflatten with a flatten later seems to cause trouble.
<porglezomp>
Hm, I'll try that
<cr1901_modern>
you may want to combine it with the setattr pass if that works
<porglezomp>
(* whitebox *) just ended up causing synthesis trouble
<cr1901_modern>
Huh, TIL about (* whitebox *)
<cr1901_modern>
((* lib_whitebox *) overrides blackbox when the -lib flag to read_verilog is present. I didn't know it was legal by itself.)
<cr1901_modern>
>synth_ecp5 -noflatten with a flatten later seems to cause trouble.
<cr1901_modern>
Yes my own experience is yosys can be very sensitive to pass order. :(
<porglezomp>
Oh, I just realized I've been reading the nextpnr error message wrong.
<porglezomp>
It's just complaining about *something* about the cells and is listing multiple possible causes together
<cr1901_modern>
This may be a daveshah question then (he's probably asleep right now), as I've never actually used the ECP5 backend (no ECP5 boards :P)
<porglezomp>
I'm just using it since it's big enough for my synthesis to balloon things ridiculously, and I can still place-and-route to get timing estimates.
<cr1901_modern>
Could I possibly see your yosys script, your library cells (the file where you define NaN gates), and your techmap file (where you convert from yosys cells to your NaN gates)?
<porglezomp>
You have to run make install, it'll stick it in your yosys data dir, run with yosys -m /usr/local/share/yosys/nangate/nangate.so
<porglezomp>
or whatever your yosys datadir is
<porglezomp>
I'm trying to run synth_nan -top top; synth_ecp5 -noflatten; flatten
<porglezomp>
but that causes errors when trying to place-and-route it
<cr1901_modern>
(strange, my copy of yosys doesn't have pmgen)
<porglezomp>
Ah! I should figure out where I got that.
<cr1901_modern>
It looks like it installs as part of yosys, but seeing as I'm on Windows, sometimes python scripts don't get installed properly
<cr1901_modern>
porglezomp: Okay, so unfortunately, I can't test right now. But looking at nangate.cc, I see what you're doing. You're taking all NAND/NOT gate sites, creating an entirely new cell in it's place, and deleting the original NAND/NOT?
<cr1901_modern>
I see what you're doing, I think*
<porglezomp>
Yeah, essentially
<porglezomp>
I think it ended up that way because I was techmapping with things where the port sizes didn't match
<porglezomp>
but I think I could handle it via wrapper modules that get removed before flattening
<cr1901_modern>
Without seeing the nextpnr error/able to test right now, I think adding a keep attribute to every bit_to_fp3/fp3_to_bit and nan will get you a design with all your cells
<porglezomp>
I get 10000-ish lines of "Info: remaining fanin includes OFX0" and then:
<porglezomp>
ERROR: timing analysis failed due to presence of combinatorial loops, incomplete specification of timing ports, etc.
<cr1901_modern>
OFX0 is a special LUT/flip flop output in ECP5; not sure what "remaining fanin" means
<porglezomp>
Hm... I wonder if it thinks all of the module ports are public, even after flattening?
<porglezomp>
I recall I once had unexpected public ports causing unusual numbers of IOs, but I don't remember what
<porglezomp>
I would expect a different sort of error, though
emeb has quit [Quit: Leaving.]
<porglezomp>
I'm going to sleep at this point. Thanks for your input there!
<cr1901_modern>
porglezomp: Ack, sorry
<cr1901_modern>
got distracted by looking at ECP5 routing. If you stay connected, I'm sure someone else will have input later on
<cr1901_modern>
Just ppl are asleep
<cr1901_modern>
Short version: OFX0 is special (it's not general routing), and I'm not sure why you're getting that error.
<porglezomp>
I don't think I have stuff set up to stay connected, but at the least I'll be checking the log if someone says something overnight.
* cr1901_modern
nods
<cr1901_modern>
sleep well!
vidbina has joined #yosys
porglezomp has quit [Ping timeout: 260 seconds]
vidbina has quit [Ping timeout: 268 seconds]
<N2TOH>
anyone here with experence working with the PC-AT 16 bit ISA bus?
<N2TOH>
I'd trying to resolve why it seems to have duplicate sets of A17, A18, and A19 address lines
<twnqx>
how do yosys / nextpnr extract the target frequency? or is it a happy accident that there's some internal default of 12MHz which happens to match my clock frequency?
<daveshah>
12MHz is an internal default that matches several common iCE40 boards
<daveshah>
Otherwise you need to do `--freq` on the command line or `set_frequency` in the PCF
<twnqx>
i see, so a happy accident :)
<ZirconiumX>
I think ECP5 defaults to 50MHz for a similar reason?
az0re has joined #yosys
mwk has joined #yosys
rohitksingh has quit [Ping timeout: 240 seconds]
dormito|2 has joined #yosys
dormito has quit [Ping timeout: 265 seconds]
az0re has quit [Remote host closed the connection]
<cr1901_modern>
N2TOH: ISA is more on topic for ##yamahasynths IME, (and it doesn't have duplicate address lines?)
d0nker5 has quit [Ping timeout: 256 seconds]
d0nker5 has joined #yosys
porglezomp has joined #yosys
d0nker5 has quit [Ping timeout: 268 seconds]
d0nker5 has joined #yosys
d0nker5 has quit [Ping timeout: 258 seconds]
d0nker5 has joined #yosys
dormito|2 is now known as dormito
d0nker5 has quit [Ping timeout: 265 seconds]
d0nker5 has joined #yosys
emeb has joined #yosys
d0nker5 has quit [Ping timeout: 260 seconds]
d0nker5 has joined #yosys
d0nker5 has quit [Quit: Lost terminal]
vidbina has joined #yosys
citypw has quit [Ping timeout: 255 seconds]
nils12345678 has joined #yosys
<nils12345678>
hello everyone,
<porglezomp>
hello
<nils12345678>
(I figured out my problem :D , sorry, didn't read the manual properly ;) )
nils12345678 has quit [Remote host closed the connection]
<cr1901_modern>
(well why don't you share what you- aaand they left)
<ZirconiumX>
cr1901_modern: I get this kind of thing a lot in the stuff I maintain. At least we didn't get insulted for having poor documentation (that the other person ignored)
<ZirconiumX>
It's always fun when that happens
<qu1j0t3>
i dunno, they seemed very polite to me, they admitted they hadn't rtfm
<cr1901_modern>
They were polite. I was just curious what they found :P
m4ssi has quit [Remote host closed the connection]
porglezomp has quit [Ping timeout: 255 seconds]
lambda has quit [Quit: WeeChat 2.7]
lambda has joined #yosys
vidbina has quit [Ping timeout: 258 seconds]
dys has quit [Ping timeout: 256 seconds]
rohitksingh has joined #yosys
az0re has joined #yosys
emeb_mac has joined #yosys
<az0re>
Does anyone here have experience working with exists-forall problems in Yosys? Can anyone explain how exactly backends/smt2/smtbmc.py interacts with the rest of the SMTLIBv2 backend (and yosys-smtbmc)?
<az0re>
Looking over commit b13e6bd375dc19fc2d6a3e67cdc6c045da732200, I'm also not super clear on what exactly are "ex_state_eq" and "ex_input_eq". I suppose that's partly a consequence of my lack of understanding of the whole process for setting up the problem for solving (the yosys-smtbmc part, I guess). With only the logic fragments generated by write_smt2, it's hard to get a coherent picture on how it all fits together.
mmicko has quit [Quit: leaving]
mmicko has joined #yosys
dormito has quit [Ping timeout: 256 seconds]
<cr1901_modern>
I didn't know the smtbmc backend could do forall problems tbh
dormito has joined #yosys
<az0re>
It looks like a one-time hack from Claire
<az0re>
I have actually built into a Yosys fork an entirely different way to handle exists-forall problems, and I'm now trying to merge the two. Well, by "merge" I mostly mean "figure out the best way to transition from my way of handling these circuits/problems to Claire's way"
dormito has quit [Ping timeout: 265 seconds]
awordnot has quit [Ping timeout: 256 seconds]
<az0re>
Like, I see things like: "ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort("\\Y")).c_str(), get_bv(cell->getPort("\\Y"), "other_state").c_str()));" and I wonder what exactly is the purpose of "other_state". Is the equality constraint between application with 'state' and application with 'other_state', or 's0' and 's0_', what ensures that it is the *same* constant chosen both in the outer (i.e. outside 'forall') and inner (inside
<az0re>
'forall') scope?
awordnot has joined #yosys
dormito has joined #yosys
<cr1901_modern>
Unfortunately I'm not in a position to really help with this right now... every few months I need to relearn how the SMT backend works. Emphasis relearn. Though this time I wrote down my notes.
<cr1901_modern>
I know z3 allows you to create SMT problems using quantifiers but I was under the impression that yosys always generated a header with "QF"
<cr1901_modern>
Does the SMT backend still mandate "Quantifier Free" and uses special tricks to emulate quantifiers?
<az0re>
It's a funny way of defining an exists-forall problem. It's more involved to modify the smt2 backend this way, but doesn't it make more sense to just 'declare-const' the existentially-quantified variable?
<az0re>
But the SMT backend is smart enough to detect existentially-quantified variables and does change its behavior slightly, like leaving ';yosys-smt2-forall' and ';yosys-smt2-anyconst' directives
<az0re>
And when in forall mode, it doesn't emit 'QF_' in the logic. I get '(set-logic AUFBV)' when running 'make demo8
<az0re>
' in examples/smtbmc.
<az0re>
(well, running 'make demo8' and modifying Makefile to add '--dump-smt2 demo8.full.smt2' to the yosys-smtbmc command)
rohitksingh has quit [Ping timeout: 240 seconds]
<az0re>
I also still do not understand the difference between '$anyconst' and '$allconst', or what exactly the '$anyseq' or '$allseq' do. I understand they're somehow related to sequential circuits, but at the same time, it seems unrolling is not supported in 'forall' mode. It's all pretty confusing.
<cr1901_modern>
Apparently they only differe in assumptions
<az0re>
Thanks! I'll check it out
<az0re>
I see, that makes sense.
<az0re>
I'm not sure what this means, though: "This gets around the annoying reality associated with defining a property using (* anyconst *) or (* anyseq *) only to have the solver pick a value which wasn’t the one that was constrained."
rohitksingh has joined #yosys
<cr1901_modern>
I'm not sure what it means either, tbh
<cr1901_modern>
My suggestion at this point would be to create a test design w/ anyconst, stare at the SMT output, then change _only_ that line to "allconst", and compare the SMT output
<cr1901_modern>
this is how I learn best when using formal
<az0re>
But I don't use $assume and never have, so I guess it's not super relevant for me, and I should just use $anyconst/$anyseq
<cr1901_modern>
extra info required to run the smt solver
<az0re>
Yep yep, already done
<cr1901_modern>
Then if they don't differ, I don't know what the difference is :P
<az0re>
I've been looking at the output from demo8, which is apparently the only working exists-forall example... :-\
<az0re>
Also, according to smt2.cc, you *need* to have an '$allconst' or '$allseq' in your design or it won't emit the ';yosys-smt2-forall' directive for yosys-smtbmc
<az0re>
...why? lol
<cr1901_modern>
Probably because adding quantifiers screws a lot of things up (qualitative opinion)?
<cr1901_modern>
so don't use quantifier logic unless you need it
<cr1901_modern>
Anyways I have to disengage right now, sorry :(. I'm stalling on doing some work I don't want to do LOL
<az0re>
But it should also do that for '$anyconst', no? It's also introducing a quantifier.