Overview

Hardware Control Language (HCL) is a simple hardware description language used to describe the control logic for both the SEQ and PIPE Y86-64 processor implementations. In the cited UCLID5 verification workflow, HCL provided a common representation from which multiple downstream artifacts could be generated, helping keep simulation models, synthesizable hardware descriptions, and formal-verification models consistent.

Role in processor verification

The verification task compared SEQ, used as a reference version of the Y86-64 ISA, against seven variants of PIPE for functional equivalence. The two implementations shared functional elements such as instruction decoding logic and the ALU, while differing in PIPE-specific pipeline registers and control logic. Their control logic was described in HCL.

A model-generation framework combined HCL control logic with frameworks for functional-block behavior and interconnection. The resulting processor models were then merged with common data types, the overall system model, and verification scripts to generate UCLID5 files for specific verification tasks.

Translation targets and tool flow

The evidence describes several translators from HCL:

• HCL to C, used to construct processor simulation models.
• HCL to Verilog, used to construct versions suitable for implementation generation by logic synthesis.
• HCL to an earlier version of UCLID, used in a previous verification effort.
• HCL to UCLID5 through the HCL2U translator, used in the cited UCLID5 verification workflow.

In the UCLID5 flow, HCL2U translated HCL signal definitions into UCLID5 macro definitions. A separate Python program performed model merging and option selection.

Language constructs

An HCL file contains a series of signal definitions, each defining how a logic block operates. The cited example defines the A input to an ALU. HCL supports case expressions that evaluate a sequence of possible choices and return the result for the first matching choice. It also supports set-membership tests.

HCL does not require a default case. When HCL2U translates a case expression into nested UCLID5 if-then-else expressions, the final then value is replicated as the final else value.

Example

The cited paper gives an HCL signal definition for selecting input A to an ALU:

##   Select input A to ALU
word  aluA = [
       icode in { IRRMOVQ, IOPQ } : valA;
       icode in { IIRMOVQ, IRMMOVQ, IMRMOVQ } : valC;
       icode in { ICALL, IPUSHQ } : -8;
       icode in { IRET, IPOPQ } : 8;
       # Other instructions don’t need ALU
];

The corresponding generated UCLID5 macro uses nested if-then-else expressions and expands set membership into equality disjunctions:

define gen_aluA() : common.word_t =
     (if ((icode == IRRMOVQ || icode == IOPQ)) then valA else if ((icode     ==
       IIRMOVQ || icode == IRMMOVQ || icode == IMRMOVQ)) then valC else
      if ((icode == ICALL || icode == IPUSHQ)) then CONSTM8() else if ((
       icode == IRET || icode == IPOPQ)) then CONST8() else CONST8());

In this example, the ALU input is selected from valA, valC, -8, or 8, depending on the instruction-code field of the current instruction.