llvm / llvm/circt

[FIRRTL] User assertions reading ports produce SV reading values from equivalent wire not port; no mechanism to express intent

Open
#11,114 0 comments 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

FIRRTL
Dominant language
C++
Stars
2.2k
Forks
524
Avg merge
3d 2h
Merged PRs (30d)
46

Description

Formal flows measure coverage by cone-of-influence on a module's ports.

Users writing assertions against the ports have repeatedly run into issues that result simply from not having the mechanism to capture their intent.

An assertion written reading a port is reading its value, the FIRRTL compiler is free to read that value from anywhere equivalent.

Nevertheless, the user is left unable to achieve their desired result -- even heavier (not semantically aligned) alternatives do not work reliably, at best leaving the user reliant on fragile pipeline-happenstance behaviors that are "time bombs" a future compliant compiler can and likely will break.

Two Minimal Examples on main

A. Aggregate port field (LowerSignatures bounce wire):

FIRRTL version 4.0.0
circuit Foo:
  layer V, bind:
  public module Foo:
    input clock : Clock
    input a : UInt<1>
    output agg : { f : UInt<1> }
    output scalar : UInt<1>
    connect agg.f, not(a)
    connect scalar, not(a)
    layerblock V:
      assert(clock, agg.f,  UInt<1>(1), "agg.f")
      assert(clock, scalar, UInt<1>(1), "scalar")

-->

// Generated by CIRCT firtool-1.159.0
module Foo_V();
  always @(posedge Foo.clock) begin
    assert(Foo.agg_f_0) else $error("agg.f");
    assert(Foo.scalar) else $error("scalar");
  end // always @(posedge)
endmodule

module Foo(
  input  clock,
         a,
  output agg_f,
         scalar
);

  wire agg_f_0 = ~a;
  assign agg_f = agg_f_0;
  assign scalar = ~a;
endmodule

Note the assertion reads agg_f_0 and not the port agg_f.

B. Scalar output read in the body (LowerToHW moves the port's inner symbol onto the wire it materializes):

FIRRTL version 4.0.0
circuit LayerCapture:
  layer L, bind:
  public module LayerCapture:
    input in : UInt<1>
    input clock : Clock
    output out : UInt<1>
    output out2 : UInt<1>
    connect out, in
    connect out2, and(in, out)
    layerblock L:
      assert(clock, out, UInt<1>(1), "foo")
      assert(clock, out2, UInt<1>(1), "bar")

-->

// Generated by CIRCT firtool-1.159.0
module LayerCapture_L();
  always @(posedge LayerCapture.clock) begin
    assert(LayerCapture._out_output) else $error("foo");
    assert(LayerCapture.out2) else $error("bar");
  end // always @(posedge)
endmodule

module LayerCapture(
  input  in,
         clock,
  output out,
         out2
);

  wire _out_output = in;
  assign out = _out_output;
  assign out2 = in & _out_output;
endmodule

Note the assertion reads _out_output , not the port out .

This has no consistent fix given the "promises" inner symbols make today: force requires readers observe the forced value (the wire) and some other users (this issue) require the target remain the port it was placed on.
This is a long-known "quirk".

This is Recurring

#8426
#8465
#9657
#9954

The above and related issues/PR's are reasonable stop-gaps but none are solutions nor can they be.
The issue is foundational.

What closes this

Offering users the mechanism needed for their use case OR deciding clearly WONTFIX.

Additional stop-gap tweaks should reference but not close this; they are pointers to the problem not the problem itself.

Contributor guide

No contributing guide indexed for this repository

First steps

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. Open a pull request that references the issue number.

Research direction

Start with the two minimal FIRRTL examples and their generated SystemVerilog, then compare the cited LowerSignatures and LowerToHW behaviors. Review issues #8426, #8465, #9657, and #9954; done means defining a mechanism that preserves the intended port target, or documenting a clear WONTFIX decision.

Written by the indexing model from the issue text.

Assessment

Domain
compilers
Issue type
Feature
Difficulty
5/5
Estimated time
Over a week
Activity status
Active
Clarity
Needs clarification
Newbie friendliness
30/100

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.