A Symbolic Model Checker supporting both the classical concept of
Computational Tree Logic (CTL) [CMU] and the proprietary concept Symbolic Constraint Filtering (SCF) extended from STE [CMU]
to provide the validation of specifications expressed as temporal properties on synthesizable RTL/Gate models.
Main Features
Temporal properties are expressed in a proprietary language name TPL and models can adopt either standard Vhdl or Verilog format.
Debugging functions are available to assist in the diagnosis of errors.
Automated generation of properties provide an original feature in model analysis and/or subsequent non-regression checking of overall functions after major changes.
Availability
Release 4.0 available on Sun Solaris, HP, DPX20 and PC
