In academia and particularly at Princeton we have research groups making chip designs into silicon. In the industry you would have dedicated engineers doing verification, both simulating tests and using formal methods, but in Academia, we can't afford this duplication, so we need hardware designers, aka grad students, to also do the verification. The problem is that doing thorough verification using formal methods has a steep learning curve and incur in significant effort. This is why it is mostly used by dedicated verification engineers. Our innovation, the AutoSVA tool, enables hardware designers to achieve this verification goal for an important part of the problem, that is, checking that each hardware module follows its interface expectations so that the chip would not hang. Designers can achieve this by simply annotating the hardware module interface in a language we developed that captures its transaction expectations. Aside from adding clarity to the interface itself, this annotations are parsed by AutoSVA, which automatically generate formal properties that standard tools can check. These properties ensure that transactions between modules eventually complete and follow certain conditions. Counterexamples or violations of these properties would provide a very targeted trace for designers to debug. Writing these properties manually would be very hard and time consuming for hardware designers as this is usually only done by verification engineers. With AutoSVA we want to democratize formal verification of hardware module interactions.