Skip to content

Commit 746c03c

Browse files
kroeningkroening
committed
SystemVerilog: final immediate and final static assertions
This adds SystemVerilog final immediate assertions and final static assertions.
1 parent ddd3c7d commit 746c03c

File tree

12 files changed

+159
-0
lines changed

12 files changed

+159
-0
lines changed

‎regression/verilog/SVA/immediate3.desc‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
immediate3.sv
3+
--bound 0
4+
^\[full_adder\.assert\.1\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

‎regression/verilog/SVA/immediate3.sv‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module full_adder(input a, b, c, output sum, carry);
2+
3+
assign sum = a ^ b ^ c;
4+
assign carry = a & b | (a ^ b) & c;
5+
6+
always @(*)
7+
assert final({carry, sum} == a + b + c);
8+
9+
endmodule

‎regression/verilog/SVA/static_final1.desc‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
static_final1.sv
3+
--bound 0
4+
^\[full_adder\.p0\] always \(\{ full_adder\.carry, full_adder\.sum \}\) == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

‎regression/verilog/SVA/static_final1.sv‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
module full_adder(input a, b, c, output sum, carry);
2+
3+
assign sum = a ^ b ^ c;
4+
assign carry = a & b | (a ^ b) & c;
5+
6+
// 1800-2017
7+
// 16.4.3 Deferred assertions outside procedural code
8+
p0: assert final ({carry, sum} == a + b + c);
9+
10+
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -94,6 +94,7 @@ IREP_ID_ONE(deassign)
9494
IREP_ID_ONE(continuous_assign)
9595
IREP_ID_ONE(procedural_continuous_assign)
9696
IREP_ID_ONE(wait)
97+
IREP_ID_ONE(verilog_assertion_item)
9798
IREP_ID_ONE(verilog_smv_eventually)
9899
IREP_ID_ONE(verilog_smv_using)
99100
IREP_ID_ONE(verilog_immediate_assert)

‎src/verilog/parser.y‎

Lines changed: 37 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3099,6 +3099,21 @@ statement_brace:
30993099

31003100
assertion_item:
31013101
concurrent_assertion_item
3102+
| deferred_immediate_assertion_item
3103+
;
3104+
3105+
deferred_immediate_assertion_item:
3106+
deferred_immediate_assertion_statement
3107+
{ /* wrap the statement into an item */
3108+
init($$, ID_verilog_assertion_item);
3109+
mto($$, $1);
3110+
}
3111+
| block_identifier TOK_COLON deferred_immediate_assertion_statement
3112+
{ /* wrap the statement into an item */
3113+
stack_expr($3).set(ID_identifier, stack_expr($1).id());
3114+
init($$, ID_verilog_assertion_item);
3115+
mto($$, $3);
3116+
}
31023117
;
31033118

31043119
procedural_assertion_statement:
@@ -3110,6 +3125,7 @@ procedural_assertion_statement:
31103125

31113126
immediate_assertion_statement:
31123127
simple_immediate_assertion_statement
3128+
| deferred_immediate_assertion_statement
31133129
;
31143130

31153131
simple_immediate_assertion_statement:
@@ -3130,6 +3146,27 @@ simple_immediate_cover_statement: TOK_COVER '(' expression ')' action_block
31303146
{ init($$, ID_verilog_immediate_cover); mto($$, $3); mto($$, $5); }
31313147
;
31323148

3149+
deferred_immediate_assertion_statement:
3150+
deferred_immediate_assert_statement
3151+
| deferred_immediate_assume_statement
3152+
| deferred_immediate_cover_statement
3153+
;
3154+
3155+
deferred_immediate_assert_statement:
3156+
TOK_ASSERT TOK_FINAL '(' expression ')' action_block
3157+
{ init($$, ID_verilog_immediate_assert); mto($$, $4); mto($$, $6); }
3158+
;
3159+
3160+
deferred_immediate_assume_statement:
3161+
TOK_ASSUME TOK_FINAL '(' expression ')' action_block
3162+
{ init($$, ID_verilog_immediate_assume); mto($$, $4); mto($$, $6); }
3163+
;
3164+
3165+
deferred_immediate_cover_statement:
3166+
TOK_COVER TOK_FINAL '(' expression ')' statement_or_null
3167+
{ init($$, ID_verilog_immediate_cover); mto($$, $4); mto($$, $6); }
3168+
;
3169+
31333170
wait_statement: TOK_WAIT '(' expression ')' statement_or_null
31343171
{ init($$, ID_wait); mto($$, $3); mto($$, $5); }
31353172
;

‎src/verilog/verilog_elaborate.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -776,6 +776,9 @@ void verilog_typecheckt::collect_symbols(
776776
module_item.id() == ID_verilog_cover_property)
777777
{
778778
}
779+
else if(module_item.id() == ID_verilog_assertion_item)
780+
{
781+
}
779782
else if(module_item.id() == ID_parameter_override)
780783
{
781784
}

‎src/verilog/verilog_expr.h‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1794,6 +1794,36 @@ to_verilog_assert_assume_cover_statement(verilog_statementt &statement)
17941794
return static_cast<verilog_assert_assume_cover_statementt &>(statement);
17951795
}
17961796

1797+
// A wrapper that encapsulates an assertion statement into an item.
1798+
class verilog_assertion_itemt : public verilog_module_itemt
1799+
{
1800+
public:
1801+
const verilog_assert_assume_cover_statementt &statement() const
1802+
{
1803+
return static_cast<const verilog_assert_assume_cover_statementt &>(op0());
1804+
}
1805+
1806+
verilog_assert_assume_cover_statementt &statement()
1807+
{
1808+
return static_cast<verilog_assert_assume_cover_statementt &>(op0());
1809+
}
1810+
};
1811+
1812+
inline const verilog_assertion_itemt &
1813+
to_verilog_assertion_item(const exprt &expr)
1814+
{
1815+
PRECONDITION(expr.id() == ID_verilog_assertion_item);
1816+
validate_operands(expr, 1, "verilog_assertion_item must have 1 operand");
1817+
return static_cast<const verilog_assertion_itemt &>(expr);
1818+
}
1819+
1820+
inline verilog_assertion_itemt &to_verilog_assertion_item(exprt &expr)
1821+
{
1822+
PRECONDITION(expr.id() == ID_verilog_assertion_item);
1823+
validate_operands(expr, 1, "generate_assign must have 1 operand");
1824+
return static_cast<verilog_assertion_itemt &>(expr);
1825+
}
1826+
17971827
// Can be one of three:
17981828
// 1) Immediate assertion statement
17991829
// 2) Procedural concurrent assertion statement

‎src/verilog/verilog_interfaces.cpp‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -271,6 +271,9 @@ void verilog_typecheckt::interface_module_item(
271271
{
272272
// done later
273273
}
274+
else if(module_item.id() == ID_verilog_assertion_item)
275+
{
276+
}
274277
else if(
275278
module_item.id() == ID_continuous_assign ||
276279
module_item.id() == ID_parameter_override)

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 41 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1932,6 +1932,43 @@ void verilog_synthesist::synth_initial(
19321932

19331933
/*******************************************************************\
19341934
1935+
Function: verilog_synthesist::synth_asertion_item
1936+
1937+
Inputs:
1938+
1939+
Outputs:
1940+
1941+
Purpose:
1942+
1943+
\*******************************************************************/
1944+
1945+
void verilog_synthesist::synth_assertion_item(
1946+
const verilog_assertion_itemt &assertion_item)
1947+
{
1948+
// 1800-2017
1949+
// 16.4.3 Deferred assertions outside procedural code
1950+
//
1951+
// module m (input a, b);
1952+
// a1: assert #0 (a == b);
1953+
// endmodule
1954+
// ---->
1955+
// module m (input a, b);
1956+
// always_comb begin
1957+
// a1: assert #0 (a == b);
1958+
// end
1959+
// endmodule
1960+
1961+
construct = constructt::ALWAYS_COMB;
1962+
event_guard = event_guardt::NONE;
1963+
1964+
value_mapt always_value_map;
1965+
value_map = &always_value_map;
1966+
synth_statement(assertion_item.statement());
1967+
value_map = NULL;
1968+
}
1969+
1970+
/*******************************************************************\
1971+
19351972
Function: verilog_synthesist::make_supply_value
19361973
19371974
Inputs:
@@ -3259,6 +3296,10 @@ void verilog_synthesist::synth_module_item(
32593296
synth_assert_assume_cover(
32603297
to_verilog_assert_assume_cover_module_item(module_item));
32613298
}
3299+
else if(module_item.id() == ID_verilog_assertion_item)
3300+
{
3301+
synth_assertion_item(to_verilog_assertion_item(module_item));
3302+
}
32623303
else if(module_item.id()==ID_task)
32633304
{
32643305
// ignore for now

0 commit comments

Comments
 (0)