Simulate/approximate "stream-like"/"stream-strength" synthesis by making assertions about outputs in consecutive cycles

[gussmith23]

Lakeroad doesn't give guarantees about behavior of infinite streams, which is what Verilog synthesis tools attempt to do. A goal of Lakeroad is to step towards stronger guarantees. One way to do this would be to add assertions about the outputs at multiple cycles, not just the outputs at one point. For example, if your module should give output in 3 cycles, we currently symbolically evaluate for 3 cycles and assert that the output is as expected. One very easy way to strengthen our synthesis query would be to evaluate for 3 cycles, make the assertion, and then evaluate a 4th cycle, and make an assertion about that output as well. Even just one more assertion would strengthen our case a lot!

Message I sent to channel:

here’s something interesting that i think should help the paper story/fortify peoples’ beliefs in our synthesis query. i realized we can pretty easily approximate the guarantees that streams give (i.e. that two designs are equivalent on an infinite stream of inputs) by simply making a finite number of additional assertions. i.e. there is a spectrum of assertions we could make about the output of two designs (the spec and the sketch):
one extreme, and what lakeroad currently does: run the designs for exactly the number of clock cycles needed to produce one output from each module, and make one assertion that the outputs are equal.
the other extreme, which isn’t possible without some kinda induction: run the designs on an infinite stream of inputs, and make an infinite number of assertions that the outputs are equal. not possible b/c infinite.
but there’s a middle option: run the designs for enough cycles to produce n outputs (# cycles = the pipeline depth + n - 1), and then make n assertions on those n outputs.
i realized this because, in the course of doing some testing infra improvements, i found a pipelined design (using a Xilinx DSP) synthesized by lakeroad that could successfully produce one correct output, but every output after that would be incorrect! that pretty clearly showed the weakness of our current synthesis query.
i prototyped the third option above, and now i’m successfully able to synthesize e.g. with n=3 extra cycles, which produces designs which are correctly pipelined (not just for 3 cycles, but for thousands!). i don’t yet know how the change will affect the whole eval — it will certainly create more solver timeouts, but hopefully not too many.
in the paper, we can now explicitly acknowledge the shortcoming of the synthesis query, but also explain this mitigation (and back up its efficacy with results).
tl;dr: i made the synthesis query stronger, which should be a good thing for the paper story and hopefully won’t affect results too much.