This is something I'm working on at work... Maybe blogging it will help me state the problem for myself.

We have signals, that may be defined in terms of other signals, constants and operations:

define [sig_name] := [expr];

For example:

define foo := bar & 1; define baz := (trix = 1) | (moby = 0)

I want to find which signals are equivalent. For instance, the following two signals are obviously equivalent:

define foo := ttt + vvv; define bar := ttt + vvv;

But in the following, foo and bar are also equivalent:

define ss := oregano; define tt := oregano; define foo := (ss = 1) & yoyo; define bar := (tt = 1) & yoyo;

I have two mutually recursive functions: is_equiv_signal and is_equiv_expr. For instance, running is_equiv_signal(foo, bar) will call is_equiv_expr(foo's definition, bar's definition) and so on. I wonder whether one pass on a group of signals is enough to determine all equivalences. As is_equiv_signal and is_equiv_expr delve deep until they reach constants (or undefined signals), it seems to be enough.

Initially, I thought of several passes. Each time all equivalences are found, and signals are replaced by their equivalents. But now, it appears to me that one pass is all I need, because my comparison is "deep". Hmm... though I'm not quite sure.

Anyway, if I take the "deep" approach, an efficiency problem arises. Clearly, is_equiv_signal and is_equiv_expr will be called on the same input over and over again. This can be solved with Memoization, at least in is_equiv_signal (signal names are easy to compare, but expressions aren't). It's interesting, since I never before used Memoization in C.