Skip to content

Commit

Permalink
Verilog: test for concatenation that contains an enum
Browse files Browse the repository at this point in the history
  • Loading branch information
kroening committed Nov 19, 2024
1 parent 820b050 commit f340d83
Show file tree
Hide file tree
Showing 2 changed files with 18 additions and 0 deletions.
8 changes: 8 additions & 0 deletions regression/verilog/expressions/concatenation6.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
CORE
concatenation6.sv
--bound 0
^\[.*\] always main\.x == \{ 0, 1 \}: PROVED up to bound 0$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
10 changes: 10 additions & 0 deletions regression/verilog/expressions/concatenation6.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
module main;

typedef enum { RED, YELLOW1, GREEN, YELLOW2 } my_enum;

// enums are allowed in concatenations
wire [63:0] x = { RED, YELLOW1 };

assert final (x == {32'd0, 32'd1});

endmodule

0 comments on commit f340d83

Please sign in to comment.