Assertion-Based Design with Horus

The Horus tool, based on formally proven correct methods, provides a unified support to assertion-based design, between the specification and the test phases. Given a set of logical and temporal properties written in PSL, Horus automatically constructs a test environment for the design. This construction is fast, correct, and produces efficient monitors and generators. The size of the instrumented design is determined by the number of distinct properties needed to specify the behavior and by the number of repetitions of each property over duplicated blocks that play symmetric roles. We have seen in the case of a wishbone switch that the number of repetitions may be quadratic in the number of nodes that compete for a resource, times the number of resources. The main advantages of our tool is to cover the whole PSL simple subset, and the whole verification flow: from the simulation to the online testing. When synthesized on FPGA, the instrumented design under test can execute at full speed.