llvm
How to obtain Core-only (hw/comb/seq) MLIR from verilog?
circt-bmc does not accept LLHD;
Verilog -> Moore -> Core still emits llhd.*, how to obtain Core-only (hw/comb/seq) MLIR for BMC?
Thank you!
Why not something like:
circt-verilog --ir-hw your_verilog.sv -o core
(For the steps used by the current circt-verilog, see https://github.com/llvm/circt/blob/main/tools/circt-verilog/circt-verilog.cpp)
After converting this Verilog file using the command, it still contains the LLHD dialect.
module fifo (
input clk,
input rst,
input wr_en, rd_en,
input [7:0] data_in,
output reg [7:0] data_out,
output wire empty, full
);
reg [7:0] mem [3:0];
reg [1:0] rd_ptr, wr_ptr;
reg [2:0] count;
initial rd_ptr = 0;
initial wr_ptr = 0;
initial count = 0;
always @(posedge clk) begin
if (wr_en && !full) begin
mem[wr_ptr] <= data_in;
wr_ptr <= wr_ptr + 1;
count <= count + 1;
end
if (rd_en && !empty) begin
data_out <= mem[rd_ptr];
rd_ptr <= rd_ptr + 1;
count <= count - 1;
end
end
assign empty = (count == 0);
assign full = (count == 4);
always @(posedge clk) begin
assert((count & 3) == ((wr_ptr - rd_ptr) & 3));
end
endmodule
module {
hw.module @fifo(in %clk : i1, in %rst : i1, in %wr_en : i1, in %rd_en : i1, in %data_in : i8, out data_out : i8, out empty : i1, out full : i1) {
%c-4_i3 = hw.constant -4 : i3
%c-1_i3 = hw.constant -1 : i3
%c1_i3 = hw.constant 1 : i3
%c1_i2 = hw.constant 1 : i2
%true = hw.constant true
%0 = llhd.constant_time <0ns, 0d, 1e>
%c0_i8 = hw.constant 0 : i8
%c0_i3 = hw.constant 0 : i3
%c0_i2 = hw.constant 0 : i2
%rd_ptr = llhd.sig %c0_i2 : i2
%1 = llhd.prb %rd_ptr : i2
%wr_ptr = llhd.sig %c0_i2 : i2
%2 = llhd.prb %wr_ptr : i2
%count = llhd.sig %c0_i3 : i3
llhd.drv %rd_ptr, %c0_i2 after %0 : i2
llhd.drv %wr_ptr, %c0_i2 after %0 : i2
llhd.drv %count, %c0_i3 after %0 : i3
%3 = comb.xor %27, %true : i1
%4 = comb.and %wr_en, %3 : i1
%5 = comb.add %2, %c1_i2 : i2
%6 = comb.add %25, %c1_i3 : i3
%7 = comb.xor %4, %true : i1
%8 = comb.mux %7, %2, %5 : i2
%9 = comb.mux %7, %25, %6 : i3
%10 = comb.xor %26, %true : i1
%11 = comb.and %rd_en, %10 : i1
%12 = comb.add %1, %c1_i2 : i2
%13 = comb.add %25, %c-1_i3 : i3
%14 = comb.xor %11, %true : i1
%15 = comb.mux %14, %9, %13 : i3
%16 = comb.or %11, %4 : i1
%17 = comb.mux %14, %1, %12 : i2
%18 = comb.mux %14, %c0_i8, %21 : i8
%19 = seq.to_clock %clk
%20 = comb.mux bin %4, %8, %wr_ptr_0 : i2
%wr_ptr_0 = seq.firreg %20 clock %19 {name = "wr_ptr"} : i2
llhd.drv %wr_ptr, %wr_ptr_0 after %0 : i2
%mem = seq.firmem 0, 1, undefined, undefined : <4 x 8, mask 1>
%21 = seq.firmem.read_port %mem[%1], clock %19 : <4 x 8, mask 1>
seq.firmem.write_port %mem[%2] = %data_in, clock %19 enable %4 : <4 x 8, mask 1>
%22 = comb.mux bin %16, %15, %count_1 : i3
%count_1 = seq.firreg %22 clock %19 {name = "count"} : i3
llhd.drv %count, %count_1 after %0 : i3
%23 = comb.mux bin %11, %17, %rd_ptr_2 : i2
%rd_ptr_2 = seq.firreg %23 clock %19 {name = "rd_ptr"} : i2
llhd.drv %rd_ptr, %rd_ptr_2 after %0 : i2
%24 = comb.mux bin %11, %18, %data_out : i8
%data_out = seq.firreg %24 clock %19 : i8
%25 = llhd.prb %count : i3
%26 = comb.icmp eq %25, %c0_i3 : i3
%27 = comb.icmp eq %25, %c-4_i3 : i3
llhd.process {
cf.br ^bb1(%clk : i1)
^bb1(%28: i1): // 3 preds: ^bb0, ^bb2, ^bb3
llhd.wait (%clk : i1), ^bb2(%28 : i1)
^bb2(%29: i1): // pred: ^bb1
%30 = comb.xor bin %29, %true : i1
%31 = comb.and bin %30, %clk : i1
cf.cond_br %31, ^bb3, ^bb1(%clk : i1)
^bb3: // pred: ^bb2
%32 = comb.extract %25 from 0 : (i3) -> i2
%33 = comb.sub %2, %1 : i2
%34 = comb.icmp eq %32, %33 : i2
verif.assert %34 label "" : i1
cf.br ^bb1(%clk : i1)
}
hw.output %data_out, %26, %27 : i8, i1, i1
}
}
Yes, if you just only use 'circt-verilog --ir-hw fifo.sv -o core', you'll force llhd because of the initials and the assert. Remove the initials and the assert, and it will work as expected (i.e., without llhd in the result).
I wonder if we could turn assignments in initial blocks into initial values for the registers 🤔. SV has very strange rules about the values that variables have when the simulation is started up, and in what order initialization occurs. But there might be enough wiggle-room there to get rid of simple initial blocks.
And we should definitely come up with a way of assigning a clock to that verif.assert inside an always @(...) process 😁
