PSL assertion checkers synthesis with ASM based HLS tool ABELITE

This paper presents a new approach for synthesizing hardware checkers from temporal assertions described in Property Specification Language (PSL). The approach utilizes Algorithmic State Machines (ASMs) based High Level Synthesis (HLS) tool ABELITE. It targets creation of functionally and temporally correct checkers that provide comprehensive assertion checking debug information during emulation. The paper contributions include a new methodology for PSL assertions translation to ASM representations and a new approach for the HLS tool ABELITE application for correct by construction assertion generation. Experimental results demonstrate feasibility and effectiveness of the proposed approach.