[Formal] What are the Semantics of Hardware?

[rdaly525]

Authors: Gilbert Bernstein, Ross Daly, Jonathan Ragan-Kelley, Pat Hanrahan
Paper PDF: https://capra.cs.cornell.edu/latte21/paper/19.pdf
Talk Recording: https://www.youtube.com/watch?v=xiAW7ULIulM

[slyubomirsky]

Perhaps I'm missing something obvious, but will the lattices always be of finite height? (E.g., how is time represented?) Is there any concern about the abstract interpretation losing precision?

[stephenneuendorffer]

I don't think they have to be. In fact, infinite partial orders/lattices underlie Kahn's formal semantics of dataflow process networks: streaming programs are defined by the composition of functions on infinite streams. In this case, one never really gets to 'top', because the lattice is infinite.

[slyubomirsky]

Thank you; I will look into the work on dataflow process networks. The reason I ask is because abstract interpretation needs a "widening" function in order to guarantee termination when the lattice has infinite height and I'm wondering whether that turns out to be inconvenient in this context

[gilbo]

Yes, apologies for glossing that inaccurately. If you have an infinite height lattice, then termination is not trivial.

Since the infinite-height lattices only really arise with time (infinite streams) we're considering two pragmatic ways of truncating infinitely running simulation:

1. If you have a finite sequence of inputs that you want to test with, then truncate all of your sequences with a finite time horizon. You now have a finite height lattice.
2. If your sequences are "regular" in the sense that they are eventually infinitely repeating, then they can be described finitely, and (insert some fancy reasoning here) you are guaranteed that all intermediate values and the fixpoint are also describable as such regular sequences, so you get termination.

[sampsyo]

It would be super interesting to think about how to build an RTL simulator on top of this foundation. It seems like a netlist simulator would be a more natural fit, but how hard would it be to add more RTLish semantics on top?

[rdaly525]

I think the two key components of this is expanding values/operations from bits to bitvectors (which will be easy), and introducing time semantics. The latter is the more interesting one and we are exploring different models of that. In my mind there are lots of different possibilities: verilator-style event sequences, single-clock, multi-clock, and circuits with gate/wire delays. The cool thing is relating these in terms of which can be abstracted from each other or a more fundamental analog semantics

[rdaly525]

One could also argue that "always-block" like sequential semantics are core to RTL, and that would be an interesting direction as well.

[gilbo]

@sampsyo: Yes, we have a ~300 line netlist simulator prototype, but the original motivation was closer to synchronous time RTL simulation. We had a DSL in Python and wanted to simulate by "just running the Python code". But we realized that we couldn't properly handle circular/cyclic/loopy value propagation within a clock-cycle (which is necessary for e.g. a ready-valid interface). Using this point of view, you could take that Python DSL and lift every python function to a transition function on abstract values. Then, instead of just naively executing all sub-procedure calls once, you can re-execute any given procedure until it reaches convergence.

We're also trying to figure out a robust way of determining tight bounds on how many times functions need to be "re-executed" to reach convergence, since that will help with scheduling this kind of modular simulation. (e.g. for Cascade, if you need to ping-pong between software and the FPGA, how many times do you need to ping-pong per cycle? And can you get away with running only a subset of the software-side on the different iterations to convergence.)

[gilbo]

Also, if any of this is useful or interesting for your lab's work, please let us know. We'd be happy to collaborate.

[sampsyo]

Awesome. I kinda think even a single-global-clock version of this vision could be really useful. I'd be happy to talk more!

[angl-dev]

I wonder if the proposed semantics could solve certain X-propagtaion challenges in gate-level simulation. For example, we know that xor(A, not(A)) is always 1. However, when A is x, most simulators just output x at the end. This is especially annoying when such deduction is on the reset path.

[angl-dev]

And yes, xor(A, not(A)) is not always 1 when we add timing information, because there might be glitches. Would it be possible to represent the static-1 glitch as well?

[gilbo]

Let me restate and answer the two questions.

1. Does this help resolve known X imprecision problems, such as xor(A, not(A))? Yes and No. You will get the same imprecision problem. However, the abstraction viewpoint does help explain this imprecision problem. In general, the relationship between "abstraction" and "concretization" is that the two functions are adjoint rather than inverse. abstracting and then concretizing may introduce imprecision in a set of values. This observation also extends to abstracting functions, not just values. So in general we can state that abstracting the composition of functions is always more precise than composing the abstraction of those functions.
2. Can we represent glitches? I think the answer is yes, although we need to specify something about the temporal and maybe intermediate value semantics of components. We are especially interested in bounding the problem of glitches/metastability in registers/latches at clock-domain crossings and at analog-to-digital boundaries.

[angl-dev]

I totally agree with the "abstracting the composition of functions" vs. "composing the abstraction of functions" statement. That's a great point.

[gilbo]

And thank you for this question! I think it's helping me think more carefully about the precise way to address that phenomenon.

[threonorm]

Hi Gilbert, Ross, In the talk you mentioned the different level of abstractions at which one may be interested in giving semantics of hardware. You semi-jokingly mentioned Maxwell's equation. Have you thought about what is the lattice correspondind to simulating the hardware at the Maxwell's equation level? ^^ (It seems like in a sense, such lattices fixpoint computation would correspond to iterative methods to solve the PDEs, guaranteed to converge. Up to the problem that it may take infinite long to compute)

[gilbo]

Yeah, definitely thought about that! =)

I think a general statement can be made about abstract interpretation: Given any system of equations, (which may not even be solvable!) you can apply abstract interpretation to the values. In the case of Diff Eq. the concrete values are functions (the unknowns) and we must have abstract values that represent sets of functions. So this ends up slightly different than just using an iterative method to solve a PDE. One would also have to track some kind of error/interval bound that then characterizes a set of possible functions. If the PDE is elliptic, then the iterative mapping ought (guessing here) to be contractive on the function space. So, the error bound should shrink. In general that may not be true, which may mean that every simulation just explodes the bounds out to TOP. However, that is somewhat inevitable in general because we don't have known ways to decide whether a given PDE is solvable at all. Also, if you consider chaotic attractors, then we know that one would almost certainly converge to an imprecise abstract value (in fact that's what people mean when they characterize the shape of an attractor region).

More pragmatically, I think Diff. Eq. semantics in this sense may be useful for reasoning about "cyber-physical systems" or characterizing analog components (e.g. signal processing). Having a sensible and sound way of bridging those semantics with digital systems seems potentially useful.

[threonorm]

Thanks! I think I understand better, so I guess that the semantics of an equation, e.g. "solving" the equation, in that context could sometimes means converging to the function "x-> top", as you point out.

[threonorm]

Hi Gilbert, Ross,
During the talk I was thinking that the semantics you presented is reminescent of the way denotational semantics works for loops, recursive calls etc... That is the computation of a least fixed point in a well chosen "information" lattice. Though your talk emphasized that I should not only think about the denotational semantics aspect, but also have abstract interpretation in mind.

When I think of abstract interpretation, what comes to my mind is usually that there are different domains: one concrete and one abstract, or a flurry of different abstracts related to each other with relative precision.
Have you started thinking about the relations (I guess formally, that would be to spell out the Galois connections) between the different abstraction level you mentioned in your semantics. For example that the naive complete boolean lattice is an abstraction of the semantics based on a lattice that woudl some form of timing constraints and propagations time. And so maybe started to build a multitower of sound abstractions (maybe some semantics are actually incomparable to eachother), with more and more efficient simulation computing less precise informations.

[gilbo]

Yes, this thought has occurred to me. I think one interesting complication is that higher-level abstractions might only be sensible under the assumption that certain phenomena in the lower-level abstraction are impossible.

For instance, consider a domain of voltage values in the range [0,1]. In abstracting this domain, we probably want to set thresholds for "high" and "low" s.t. there also exists an intermediate range between the two thresholds. One can say that these intermediate values just get mapped to TOP, but it's not clear that everything will work out correctly if you just turn the crank on that approach. At the transistor level, you really do need to limit the length of paths extending from power or ground leads, so that the voltage levels don't decay too much from their ideal level.

Likewise there exist temporal periods where the values are indeterminate. So, moving from a more precise temporal model to a clock-synchronous one is contingent on the "clock" being a sensible concept which is correctly handled within all circuit components at the lower level.

I think we just need to get into the details of some of these cases, but my current suspicion is that we need some concept of a "partial abstraction" or a galois connection that holds for specific circuits rather than all possible circuits. So then I think we need some kind/kinds of program analyses to certify that such relations hold.