Verification of Properties for Embedded Systems


From large public applications (transport, multimedia, telecoms) to critical applications (aerospace, aeronautics), embedded systems integrate an infinitely increasing number of functionalities. In order to guarantee the performance of these systems – real-time, safety/security, consumption, etc. – complex verifications are required at each stage of development from the initial stages of the design flow until the hardware prototyping.


The HORUS environment with its ergonomic interface will allow you to save considerable time in the different stages of design flow, thanks to the automatic verification of your system’s performance.

  • Ease and speed of implementation
  • Specifications expressed using standardised language
  • Officially proven construction method

Service Offering

At Register Transfer Level:

  • simulation with standard tools
  • accelerated simulation using FGP emulation
  • online surveillance of critical circuits
  • extension to the construction of asynchronous monitors currently in progress (verification of multi-clock systems)

For transaction Level Modelling:

  • dynamic verification of System C TLM descriptions with or without time
  • expression of elaborate  properties (over several communication channels and/or signals)
  • expression of restrictions on communication function parameters
  • performance (very little loss of time for simulation)


The HORUS environment uses the verification methodology of logico-temporal assertions (ABV, Assertion-Based Verification). From assertions written in a standard IEEE 1850 PSL language, it enables automatic generation.

In terms of RTL: Synthesisable VHDL or Vérilog descriptions

  • of synchronous or asynchronous surveillance monitors for verification of functionalities to be guaranteed by the system (assert)
  • of sequence generators for satisfactory testing of temporal restrictions on its entries (assume)

In terms of (transactional) TLM: System C TLM descriptions of surveillance monitors for the verification of logico-temporal properties on communications



  • Multimedia Applications
  • Telecommunications
  • Avionics or Space
  • Automobiles
  • Buildings

Contact Us