gen_test_cases command

CodeArtifact

The `gen_test_cases` command is used in HOL-TestGen proof scripts to automatically generate schematic test cases from test specifications. In the cited VAMP microprocessor case study, it is applied to unit and sequence scenarios for load/store, arithmetic, and branching instructions, producing symbolic test cases, uniformity hypotheses, and test theorems that can later be instantiated with concrete data by `gen_test_data`.

First seen 5/26/2026

Last seen 5/26/2026

Evidence 3 chunks

Wiki v1

WIKI

Overview

gen_test_cases is a HOL-TestGen command used in proof scripts after a test_spec formula has constrained the intended test domain. In the VAMP microprocessor case study, it is shown as an apply method that generates schematic test cases for a system under test (SUT) and is followed by store_test_thm, which stores the result as a named test theorem. [c1]

Typical forms shown in the evidence include:

READ FULL ARTICLE →

NEIGHBORHOOD

No graph connections found for this entity yet. It may appear in future ingestion runs.

explore full graph →

RELATIONSHIPS

1 connections

HOL-TestGen part of → 100% 1e

gen_test_cases is a command in HOL-TestGen used for test case generation.

LINKED ENTITIES

2 links

HOL-TestGen implemented_in The evidence identifies `gen_test_cases` as part of the HOL-TestGen test case generation procedure and as an automatic test case generation method used in HOL-TestGen scripts.

gen_test_data command workflow_successor The evidence states that schematic test cases generated in the first phase are instantiated with concrete values by the `gen_test_data` command.

CITATIONS

14 sources

14 citations — click to expand

[1] c1: `gen_test_cases` is used after `test_spec` and before `store_test_thm`, with forms including `gen_test_cases 0 1 SUT` and `gen_test_cases SUT`. Test Program Generation for a Microprocessor: A Case Study

[2] c2: In the sequence scenario, the automatic test case generation call declares the free variable `SUT` as the system under test. Test Program Generation for a Microprocessor: A Case Study

[3] c3: HOL-TestGen performs exhaustive case splitting on the instruction datatype and generates symbolic operands for instructions. Test Program Generation for a Microprocessor: A Case Study

[4] c4: `gen_test_data` is the second phase that instantiates schematic variables with concrete values. Test Program Generation for a Microprocessor: A Case Study

[5] c5: The load/store unit-test scenario generated eight symbolic test cases and eight uniformity hypotheses, whose conjunction is called a test theorem. Test Program Generation for a Microprocessor: A Case Study

[6] c6: Variables beginning with `??X` are schematic variables representing possible witness values, and generated cases are paired with uniformity hypotheses. Test Program Generation for a Microprocessor: A Case Study

[7] c7: Load/store unit tests can reveal design faults in operation results and undesired state modifications such as changes to flags or registers. Test Program Generation for a Microprocessor: A Case Study

[8] c8: For arithmetic unit tests, `gen_test_cases 0 1 SUT` is used with `is_arith`, and each arithmetic operation is covered by one generated test case at that stage. Test Program Generation for a Microprocessor: A Case Study

[9] c9: For branching unit tests, `gen_test_cases 0 1 SUT` generates unit test cases from initial state `σ0`, but the fixed initial state is problematic because branch behavior depends on flags. Test Program Generation for a Microprocessor: A Case Study

[10] c10: Instruction sequence scenarios use `list_all` and monadic state-exception combinators such as `mbind` and `assertSE` to define valid test sequences. Test Program Generation for a Microprocessor: A Case Study

[11] c11: A generated load/store sequence example has length three and contains `Isw` followed by two `Ilbu` instructions, with an associated uniformity hypothesis. Test Program Generation for a Microprocessor: A Case Study

[12] c12: An arithmetic sequence scenario uses `gen_test_cases SUT`; after data generation, an example concrete sequence is `ISUB` followed by two `IADD` operations. Test Program Generation for a Microprocessor: A Case Study

[13] c13: A branch sequence scenario uses `gen_test_cases SUT`; after data generation, an example concrete sequence is `IJ 1` followed by `IJALR 0`. Test Program Generation for a Microprocessor: A Case Study

[14] c14: Test data generation in the considered scenarios is performed by constraint solving and random instantiation, can lead to coarsely grained memory access, and may be refined by adding constraints over addresses or subdomains. Test Program Generation for a Microprocessor: A Case Study