Skip to content

Commit 9e75065

Browse files
committed
introduce verilog_sva_property_typet
This introduces a type for Verilog SVA properties To distinguish properties from state predicates and sequences.
1 parent 78d038d commit 9e75065

File tree

2 files changed

+10
-0
lines changed

2 files changed

+10
-0
lines changed

src/hw_cbmc_irep_ids.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -140,6 +140,7 @@ IREP_ID_ONE(verilog_null)
140140
IREP_ID_ONE(verilog_event)
141141
IREP_ID_ONE(verilog_event_trigger)
142142
IREP_ID_ONE(verilog_string)
143+
IREP_ID_ONE(verilog_sva_property)
143144
IREP_ID_ONE(verilog_sva_sequence)
144145
IREP_ID_ONE(reg)
145146
IREP_ID_ONE(macromodule)

src/verilog/verilog_types.h

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -739,6 +739,15 @@ inline verilog_package_scope_typet &to_verilog_package_scope_type(typet &type)
739739
return static_cast<verilog_package_scope_typet &>(type);
740740
}
741741

742+
/// SVA properties
743+
class verilog_sva_property_typet : public typet
744+
{
745+
public:
746+
verilog_sva_property_typet() : typet(ID_verilog_sva_property)
747+
{
748+
}
749+
};
750+
742751
/// SVA sequences
743752
class verilog_sva_sequence_typet : public typet
744753
{

0 commit comments

Comments
 (0)