Background

Over the last few years, we’ve seen the convergence of multiple developments at the hardware / software boundary that make research on principled, retargetable ISA testing highly promising. Those include:

• Slowing down of Moore’s law, and a concomitant rise in demand for domain specific processors and accelerators.
• Increasing pressure on lowering the time from idea to taped-out silicon, which can only be met with more automation and higher-performance from tooling such as testers and emulators.
• Novel security demands, arising from new compute tasks such as virtualisation in the cloud and new security threats, in particular side channels and micro- architectural attacks, such as Spectre.
• The hardening divide between ISA-level modelling and micro-architectural modelling, witnesses by the rise of domain-specific languages for either, e.g. Arm’s ASL and Sail for the former and Chisel, FIRRTL, LLHD for the latter.
• Increasing rigour in ISA specification, for example: Sail is rigorously formally defined, which enables and simplifies the principled automated construction of test cases, and automatic generation of notions of test coverage. Sail, unlike previous ISA specification languages, has an expressive typing system (called liquid types), and it should be possible to use types to improve automatic test generation.
• Strong demand for crossing the hardware/software chasm, for example witnessed by intense memory model verification).
• Desire of integration of verification tool chains at hardware/software boundary to deal with cross-cutting issues (e.g. memory models, security properties)
• An explosion in software testing methodology (e.g. property based testing) and tooling: in particular, large-scale automated software testing has progress in in leaps and bounds with the rise of Coverage-guided greybox fuzzers and explosion in SMT-solver performance.
• Availability of much more compute resources that makes ultra-large scale automated testing more feasible, see e.g. Google’s cloud fuzzing.