文摘
Behavioural equivalence checking of the refinements of the input behaviours taking place at various phases of synthesis of embedded systems or VLSI circuits is a well pursued field. Although extensive literature on equivalence checking of sequential behaviours exists, similar treatments for parallel behaviours are rare mainly because of all the possible execution scenarios inherent in them. Here, we propose a translation algorithm from a parallel behaviour, represented by an untimed PRES+ model, to a sequential behaviour, represented by an FSMD model. Several equivalence checkers for FSMD models already exist for various code based transformation techniques. We have satisfactorily performed equivalence checking of some high level synthesis benchmarks represented by untimed PRES+ models by first translating them into FSMD models using our algorithm and subsequently feeding them to one such FSMD equivalence checker.