<lkcl>
cr1901_modern: an extremely experienced team that i knew were deeply unimpressed with puppet. they used it... however they chopped its network-push capabilities off at the knees, and used git repositories instead
<lkcl>
i.e. they placed all puppet configs in a git repo, used a cron job to sync that
<lkcl>
and then used git hooks to activate jobs, locally
<lkcl>
as they were managing 1,000 systems, some of them over incredibly expensive or unreliable 2G/3G networks, it was crucial to *not* rely on the network "push" being successful.
<lkcl>
all puppet jobs were written as locally-executable scripts (#!/usr/bin/env php at the top)
rohitksingh_work has joined #m-labs
_whitelogger has joined #m-labs
m4ssi has joined #m-labs
proteusguy has joined #m-labs
mauz555 has joined #m-labs
mauz555 has quit [Ping timeout: 246 seconds]
mauz555 has joined #m-labs
mauz555 has quit [Remote host closed the connection]
mauz555 has joined #m-labs
mauz555 has quit []
bluebugs has joined #m-labs
bluebugs has quit [Changing host]
bluebugs has joined #m-labs
cedric has quit [Ping timeout: 268 seconds]
<mtrbot-ml>
[mattermost] <sb10q> how to do formal verification for a round-robin wishbone arbiter? any ideas?
<cr1901_modern>
sb10q: assert(s_eventually "cyc/stb changes value to the next master")
<cr1901_modern>
I don't know how to write a symbiyosys script to prove that tho
<cr1901_modern>
At present only the AIGER backend to symbiyosys supports $live (s_eventually) cells
<cr1901_modern>
and I've never used it
<mtrbot-ml>
[mattermost] <sb10q> whitequark: should nMigen support zero-length signals?
<mtrbot-ml>
[mattermost] <sb10q> i.e. signals with zero bits, which can only have value 0, which do nothing when part of Cat(), etc.
<lkcl>
sb0: ah, yes, this is actually important for us, too
<lkcl>
we have discovered some code that is functionally equivalent to a hybrid combination of SyncFIFO and SyncFIFOBuffered
<lkcl>
that can accept queue sizes down to ONE in size.
<lkcl>
(as long as fwft=True)
<lkcl>
the internal calculations result in *ZERO* width signals for things such as the difference between the head and tail pointers
<lkcl>
and in the digraphs we see computations (eq, NOT) and so on with, again, ZERO widths
<lkcl>
whilst most of that code gets ignored, some of it actually goes into e.g. the address of the SRAM on the read and write ports
<lkcl>
a zero-width Signal as the SRAM read/write address
<lkcl>
we *hope* that gets assigned to zero!!!
<cr1901_modern>
sb10q: Yea, see daveshah's link for an example... you'll need to install something that can handle aiger files
proteusguy has quit [Ping timeout: 255 seconds]
rohitksingh_work has quit [Read error: Connection reset by peer]
proteusguy has joined #m-labs
proteusguy has quit [Ping timeout: 258 seconds]
proteusguy has joined #m-labs
<npulido>
We want to control a PDQ using artiq 4.0 and have a crate with the artiq-kasli-hub 4.0 variant flashed. Is it possible to configure the PDQ using only the USB connection (and trigger it with a ttl)? Or does it always need an SPI connection?
<rjo>
npulido: you can upload data and configure it via USB as well.
<npulido>
rjo: We built the gateware in a linux machine but couldn't manage to flash the bitstream, so we flashed it using a windows computer. Is that OK?
<rjo>
npulido: sure.
<rjo>
npulido: are you with christian?
<npulido>
rjo: alright. We have been playing around with the cli.py example, we get no output from the PDQ (0 Volts), but also no error.
<lkcl>
graphviz (of code that works) with zero-width signals
<rjo>
npulido: there is no readback on USB so it could be anything.
<npulido>
rjo: ok, makes sense
<lkcl>
also, the code conforms directly with the FIFOInterface API, provides the *exact* same functionality as SyncFIFO and SyncFIFOBuffered, combined, including support for the fwft parameter
<lkcl>
it's based on Chisel3's QueueIO object and provides a "bypass" path for Memory, so does not suffer from the problem of FPGA SRAMs not having write-through capability
<lkcl>
end result: the need for SyncFIFOBuffered is gone.
<lkcl>
we also found a work-around for Memory not being able to handle address sizes of 1 - it's pretty awful: allocate a minimum of a 2-address SRAM
<npulido>
rjo: I guess we should keep trying then. This particular PDQ we tested using the hf-gui system and works, so we must be making some mistake... We thought maybe it was that it needed the SPI connection also, as the documentation either mentions SPI only or SPI and USB.
<lkcl>
and then ignore the 2nd entry.
<rjo>
npulido: you can check wether the most basic things work, like setting the clock to 100 MHz and checking it on a scope.