Skip to content
STIMSMITH

HCL2U Translator

Tool WIKI v1 · 5/26/2026

HCL2U is a translator used in a UCLID5-based verification framework for Y86-64 processor models. It converts Hardware Control Language (HCL) signal definitions into UCLID5 macro definitions, enabling control logic to be extracted directly from HCL descriptions and reused in formal verification models.

Overview

The HCL2U Translator is a tool described in the verification framework for pipelined Y86-64 microprocessors using UCLID5. Its role is to translate control logic written in HCL (Hardware Control Language) into UCLID5 macro definitions. In the framework, HCL2U is one of the programs used to generate UCLID5 files for specific verification tasks, alongside a Python program that performs file merging and option selection.

Role in the verification workflow

The verification framework generates UCLID5 files that each describe a model and verification script. Processor models are built by combining HCL-expressed control logic with frameworks for functional blocks and their interconnections. The generated processor models are then merged with files defining common data types, the overall system model, and the verification script. HCL2U performs the translation from HCL signal definitions into UCLID5 macro definitions, while a Python program performs merging and selection among modeling and verification options.

The framework was used in a task comparing the SEQ processor model against seven variants of PIPE for functional equivalence. The control logic for both SEQ and PIPE is written in HCL, and generating logic directly from the common HCL representation helps maintain consistency among simulation models, synthesizable hardware descriptions, and formal verification models.

Translation behavior

HCL2U generates a UCLID5 macro for each HCL signal definition. The translation is described as straightforward, but not designed to produce human-readable output.

Important translation rules include:

  • HCL case expressions are translated into nested UCLID5 if-then-else expressions.
  • HCL set-membership tests are expanded into disjunctions of equality tests.
  • Because HCL does not require a default case, the translator replicates the final then value as the final else value when constructing nested if-then-else expressions.

Example: ALU input selection

The source evidence gives an example HCL signal definition for selecting input A to the ALU. The HCL definition selects among valA, valC, -8, and 8 based on the instruction code. HCL2U translates this into a UCLID5 macro named gen_aluA() returning common.word_t. The generated UCLID5 code uses nested if expressions and replaces membership tests such as icode in { IRRMOVQ, IOPQ } with equality disjunctions such as icode == IRRMOVQ || icode == IOPQ.

Design significance

Within the described framework, HCL2U helps ensure that the formal verification model uses control logic extracted from the same HCL descriptions used elsewhere. The evidence states that HCL had also been translated to C for simulation, to Verilog for logic synthesis, and to an earlier version of UCLID in prior work; using a common representation supports consistency across those generated artifacts.

CITATIONS

8 sources
8 citations
[1] HCL2U translates HCL signal definitions into UCLID5 macro definitions. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[2] The UCLID5-generation workflow combines HCL control logic with functional-block frameworks, common data types, a system model, and a verification script; HCL2U handles HCL-to-UCLID5 translation while a Python program handles merging and option selection. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[3] The verification task used SEQ as a reference model and compared it with seven variants of PIPE for functional equivalence. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[4] Control logic for SEQ and PIPE is described in HCL, and using a common representation helps maintain consistency among simulation models, synthesizable hardware descriptions, and formal verification. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[5] HCL2U generates a UCLID5 macro for each HCL signal definition, and the translation is straightforward but not intended to be human-readable. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[6] HCL case expressions are translated into nested if-then-else expressions, and HCL set membership tests are expanded into disjunctions of equality tests. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[7] Because HCL does not require a default case, HCL2U replicates the final then value as the final else value in nested if-then-else translations. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5
[8] The provided ALU input example translates an HCL signal definition into a UCLID5 macro named gen_aluA() returning common.word_t. Formal Verification of Pipelined Y86-64 Microprocessors with UCLID5