UC Santa Cruz

Modern electronics feature semiconductor chips which are incredibly sophisticated consisting of multi-millions of logic gates. A small change has the potential to produce disastrous consequences effecting project timelines and time to market. Developing these complex chips requires correct tools and verifiable designs during all stages of design and testing.

LiveHD is an open-source EDA tool for synthesis and simulation that provides quick feedback for small design changes. LGraph is the optimized, netlist, graph representation of LiveHD. To maintain correctness over optimizations and to aid in performing logic equivalence checking, the integration of an SMT solver, Boolector, with LGraph is proposed. This thesis outlines the process of developing the interface between Boolector and LGraph to produce a logic equivalence check (LEC) pass for LiveHD. Although full integration was not achieved, the current status of the pass, limitations and future work are discussed.