• LOGAN^TM (LOGic ANalyzer) : A Model Checker supporting both the classical concept of Computational Tree Logic [McMillan,CMU] and a proprietary concept called Symbolic Constraint Filtering to provide the validation of specifications expressed as temporal properties on synthesizable RTL/Gate models.
• LEQ^TM (Logic EQuivalence) : A formal verification tool that analyzes the quality of complex logic designs (eg. detection of functional loops, dead codes, unused objects, conflicts, ...), provides formal comparison at different levels of abstraction (RTL/RTL, RTL/Gate, Gate/Gate) and assists in debugging logic errors. The proprietary Boolean manipulation technique developed by METASymbiose provides LEQ with the ability to handle large and complex design including arithmetic operators (eg. multiplier).
• STEQ^TM (STructure EQuivalence) : A formal comparison tool dedicated to the efficient formal comparison of large flattened netlists (in the range of million of gates) with similar structure.
• LABS^TM (Logic ABStraction) : An abstraction tool to produce automatically RTL/Logic descriptions from hierarchical mixed gate/transistor netlists. Different design styles including dynamic logic can be recognized automatically.

ThePrototyping Suite developed to support design emulation targeting semi-custom platforms (commercial emulator, programmable boards) is composed of tools performing the following tasks : Generic FPGA synthesis, Flattening an Re-optimization, Automatic Partitioning, Interconnection Reduction and Multiplexing.