looking for assertion language for instruction set verification

Alan Lehotsky <lehotsky@tiac.net>
6 Mar 2000 00:31:04 -0500

          From comp.compilers

Related articles
looking for assertion language for instruction set verification lehotsky@tiac.net (Alan Lehotsky) (2000-03-06)
Re: looking for assertion language for instruction set verification nr@labrador.eecs.harvard.edu (2000-03-06)
| List of all articles for this month |

From: Alan Lehotsky <lehotsky@tiac.net>
Newsgroups: comp.compilers,comp.arch
Date: 6 Mar 2000 00:31:04 -0500
Organization: Quality Software Management
Keywords: architecture

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...

                                    ADD RZ,RX,RY
                                    ADD RQ,RY,RX

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

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


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

Al Lehotsky

                                Quality Software Management
Process Improvement | Management Consulting | Compiler Implementation

Post a followup to this message

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