Interconnect Traffic Jam on your SoC
Interconnect on a System on Chip (SoC) is like the road network. There is a lot of it but it still doesn’t go everywhere and traffic jams mean that even if there is a road, you may not be able to get to your destination.
On an SoC, just because there is a wire doesn’t mean a signal can always get through. Just like there are different types of vehicles on the roads, we have different signal values on the SoC. Muxes and intersections change the flow of traffic and both roads and wires can be single lane or multi-bit.
To be sure that I can drive between two cities or that a signal on my SoC can reach module B from module A, we have to verify it. There are two popular interconnect verification methods we can use: Simulation and Formal Verification.
Source: Google Maps
For example, we want to verify that San Jose and Austin are connected by road. We can see roads on the map but we need a more detailed specification to verify that the cities are really interconnected. A more detailed specification would be something like: “Take 680 North, at intersection 71 turn right onto 80 East. At intersection 313 turn right to 287 south. At Owl Canyon turn right onto 25 South …” This would continue all the way to Austin. If you view intersections as muxes you could write this as an interconnect assertion:
assert property: (680N && (Sel_71 == right) && US80 && (Sel_313 == right) && … ) |-> (san_jose == austin)
To verify the assertion, I can follow the directions and drive from San Jose to Austin. This is analogous to verifying with simulation, when I drive one vehicle and if it arrives, it shows the two cities are connected. But, I have not proven (across all possible scenarios) that the two cities are connected. A slight improvement is to drive many different vehicles until we are confident we have covered enough cases. But, what is enough? Even if I drive 10 different vehicles I still haven’t proven it for all possible scenarios. The route goes via Boulder and in the winter, only cars with 4-wheel drive can make the trip. What about trucks? There is a bridge with a 4-ton weight limit along the way, therefore San Jose and Austin are not connected along the specified route for trucks. By successfully driving the route I have shown there is a connection but it is not proven across all possible scenarios
On an SoC, for example, we want to verify that the port 680N on the module San Jose is connected to the port loop360 on the module Austin.
Using simulation, I can force values on the select signals, drive a value on the 680N port and observe if the value is the same on the loop360 port. You can’t verify one value and assume the ports are connected. Multiple values are needed, but how many? If one bit of a bus is stuck at 1, half the values will not detect the fault. We can simulate using many different random values until we are confident we have covered enough scenarios but we have still not proven that they are connected.
This is a drawback of simulation both for driving between cities and verifying SoC interconnect. Only a small sub-set of data values or types of cars or seasons (e.g. Summer) are tested. There is no way to verify all possible values in either case.
To verify that module ports on an SoC are connected, Formal Connectivity Checking is a much more efficient solution. Unlike driving multiple values in simulation, Formal Connectivity checking is much faster and it is exhaustive. That is, all possible data values for a connection are proven at the same time. If bits are swapped or any bits are stuck at 0 or 1, verification will fail. Formal is also more complete. It proves that the source port and the destination port always have the same value when the enable expression is true and it also proves that there is a structural path through the circuit from source to destination. Omitting the structural check is like saying San Jose and Austin are connected because you can fly, you conveniently ignore the requirement for a road.
Proving that San Jose is connected to Austin via roads for all types of vehicles is a little bit trickier…
