looking for assertion language for instruction set verification

Summary: I'm looking for existing research on an assertion language
      suitable for testing an instruction set architecture.


I'm involved in a project to emulate an instruction set (doing runtime
translation). As part of testing and validating the behavior of this
tool, I'd like to automate test generation.


For example, we have a lisp-like language that we can write pseudocode
to describe the host machine instructions that are equivalent to the
instruction we're emulating.


I'd like to augment this with another set of statements that would
make assertions about the pre and post-conditions that are relevant
to the instruction. These statements would be used to automatically
generate test programs.




As a simple minded example, assume I had a 3 address add instruction.
I'd want to be able to write the following assertions and auto-generate
a program to test them...




      ForAny(RX,RY,RZ,RQ)
                                    ADD RZ,RX,RY
                                    ADD RQ,RY,RX


                          RQ==RZ /* ADD is commutative... */




      ForAny (RX,RZ)
                                ADD RZ,RX,#1
                                ADD RZ,RZ,#-1


                        RZ==RX


Anybody out there seen anything like this? Or do I have to
reinvent this wheel myself?


Thanks,
Al Lehotsky


--
                                Quality Software Management
                          http://www.tiac.net/users/lehotsky
Process Improvement | Management Consulting | Compiler Implementation

Return to the comp.compilers page.
Search the comp.compilers archives again.