pie_ has quit [Read error: Connection reset by peer]
pie_ has joined #yosys
AlexDaniel` has quit [Remote host closed the connection]
AlexDani` has joined #yosys
AlexDani` is now known as AlexDaniel`
Guest64469 is now known as jayaura
m_t has joined #yosys
pie_ has quit [Ping timeout: 240 seconds]
_whitelogger has joined #yosys
knielsen has quit [Quit: leaving]
proteusguy has quit [Remote host closed the connection]
knielsen has joined #yosys
pie_ has joined #yosys
qu1j0t3 has quit [Ping timeout: 240 seconds]
_whitelogger has joined #yosys
indy has quit [Ping timeout: 240 seconds]
leviathanch has joined #yosys
pie_ has quit [Ping timeout: 252 seconds]
proteus-guy has joined #yosys
qu1j0t3 has joined #yosys
indy has joined #yosys
indy has quit [Ping timeout: 248 seconds]
indy has joined #yosys
Brando753-o_O_o has quit [Ping timeout: 246 seconds]
pie_ has joined #yosys
proteusguy has joined #yosys
pie_ has quit [Ping timeout: 258 seconds]
leviathanch has quit [Read error: Connection reset by peer]
jj_ has joined #yosys
proteusguy has quit [Ping timeout: 248 seconds]
ZipCPU|Laptop has joined #yosys
ZipCPU|Laptop has quit [Ping timeout: 252 seconds]
leviathanch has joined #yosys
jj_ has quit [Ping timeout: 260 seconds]
cr1901_modern has quit [Ping timeout: 248 seconds]
cr1901_modern has joined #yosys
proteusguy has joined #yosys
ZipCPU|Laptop has joined #yosys
proteusguy has quit [Ping timeout: 240 seconds]
proteus-guy has quit [Ping timeout: 246 seconds]
sklv1 has quit [Read error: Connection reset by peer]
sklv1 has joined #yosys
sklv1 has quit [Remote host closed the connection]
sklv1 has joined #yosys
proteusguy has joined #yosys
Brando753-o_O_o has joined #yosys
m_t has quit [Ping timeout: 258 seconds]
proteusguy has quit [Read error: Connection reset by peer]
proteusguy has joined #yosys
pie_ has joined #yosys
proteusguy has quit [Remote host closed the connection]
proteusguy has joined #yosys
beefok has joined #yosys
<beefok>
howdy all :)
<beefok>
any ice40'ers here? Since when does it not support tristate ports? I'm getting a synplify pro error, FX741 : "Part ice5lp2k does not support tristates"
<beefok>
since when?! I know the I/O have tristates, lol
<beefok>
I know the ice40 tech library has SB_IO with tristate enables, so what the hecks
<beefok>
am I going to have to generate an SB_IO per pin?
<ZipCPU|Laptop>
iCE40 supports tri-states.
<cr1901_modern>
What I don't remember is whether arachne-pnr does
<cr1901_modern>
beefok: SB_IO per pin will most certainly work, even though its inelegant
<ZipCPU|Laptop>
As I recall, the tools supported the SB_IO primitive, but not the 'z
<sorear>
is it common for synthesis tools to support 'z and nets?
<cr1901_modern>
nets? No modern FPGA family supports internal tristates if that's what you're asking.
<sorear>
no, I was asking specifically about synthesis tools, not the FPGAs themselves
<ZipCPU|Laptop>
All of the Xilinx FPGA's I have worked with have supported tri-state I/O ports.
<ZipCPU|Laptop>
... just not tri-state internal nets
<sorear>
ZipCPU|Laptop: does the synthesis tool understand 'z or do you need to use a primitive?
<ZipCPU|Laptop>
For Xilinx, the synthesis tool has no problems with 'z--no primitive required.
<ZipCPU|Laptop>
The yosys/arachne/ice-tools iCE40 toolchain is different in this respect.
<ZipCPU|Laptop>
sorear: Since you are asking the question, have you never needed a 'z before? or, if so, what tool chain do you typically use?
<sorear>
i don't, i'm saying it in the context of beefok's question
<beefok>
thanks guys :)
<beefok>
Yeah for some reason the icecube2 tool doesn't recognize 'z' either
<beefok>
just ended up having to do a bunch of SB_IO in gen for loops (vhdl lol)
<beefok>
ended up making a separate module just for all the SB_IO, that way I can control it
<beefok>
actually, according to the lattice manual, you can set attributes for tristates 0_o
<beefok>
attribute syn_tristate : boolean; attribute syn_tristate of tout: signal is true;
<beefok>
apparently after that, you can then set tout <= 'Z'
adj__2 has quit [Quit: Leaving]
beefok has quit [Quit: Page closed]
adj__ has joined #yosys
<awygle>
to the Formal People - is it possible (in theory and/or with yosys) to prove for a parameterized module that it is correct for all legal parameter values?
<ZipCPU|Laptop>
If it is, I don't know how to do that (yet)
<ZipCPU|Laptop>
I'll add that I just tested a FIFO that did different things for reads and writes depending upon the parameter. If I set the parameter one way, it would fail, if the other way it would succeed.
<ZipCPU|Laptop>
Basically, if it was a "READ-ONLY" FIFO (really a mis-nomer, since it was a fully implemented FIFO), there'd be a status word telling you how many items are available to be read.
<ZipCPU|Laptop>
The WRITE-ONLY FIFO had a status word telling how many empty positions were within the FIFO that could be written to.
digshadow has joined #yosys
<awygle>
The next best thing, which would be formally verifying the actual instantiation that's used in a larger design as part of the verification of that design, seems achievable at least...
<sorear>
my mental model of how model checkers work says that doing it for an infinite number of parameterizations at once would be impossible
<awygle>
I was thinking some kind of higher level induction. It would get N-dimensional really quickly but if you are parameterizing a counter length, that should be inductable
eduardo has joined #yosys
ZipCPU|Laptop has quit [Ping timeout: 246 seconds]
<adityaP>
I am using yosys-smtbmc to do formal verification of Synchronous FIFO. When I am running the formal check on the FIFO from the diagram you can see that the rd_ptr is becoming zero after one clock cycle of smt_clock. But when I am running fifo in ModelSim, the rd_ptr is becoming 0 as soon as the reset is asserted one. In my code I haven't mentioned any one clock cycle delay. Can any one please explain why is this