Skip to content

Commit

Permalink
Verilog: strenthen typing for generate constructs
Browse files Browse the repository at this point in the history
This uses types stronger than exprt for Verilog generate constructs.
  • Loading branch information
kroening committed Jan 22, 2024
1 parent 8f0a473 commit 699db59
Show file tree
Hide file tree
Showing 3 changed files with 48 additions and 23 deletions.
32 changes: 32 additions & 0 deletions src/verilog/verilog_expr.h
Original file line number Diff line number Diff line change
Expand Up @@ -230,6 +230,23 @@ inline verilog_generate_blockt &to_verilog_generate_block(exprt &expr)
return static_cast<verilog_generate_blockt &>(expr);
}

class verilog_generate_caset : public verilog_module_itemt
{
public:
};

inline const verilog_generate_caset &to_verilog_generate_case(const exprt &expr)
{
PRECONDITION(expr.id() == ID_generate_case);
return static_cast<const verilog_generate_caset &>(expr);
}

inline verilog_generate_caset &to_verilog_generate_case(exprt &expr)
{
PRECONDITION(expr.id() == ID_generate_case);
return static_cast<verilog_generate_caset &>(expr);
}

class verilog_generate_ift : public verilog_module_itemt
{
public:
Expand Down Expand Up @@ -273,6 +290,21 @@ class verilog_generate_fort : public verilog_module_itemt
{
}

const exprt &init() const
{
return op0();
}

const exprt &cond() const
{
return op1();
}

const exprt &increment() const
{
return op2();
}

const verilog_module_itemt &body() const
{
return static_cast<const verilog_module_itemt &>(get_sub()[3]);
Expand Down
31 changes: 11 additions & 20 deletions src/verilog/verilog_generate.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -187,11 +187,11 @@ void verilog_typecheckt::elaborate_generate_item(
if(statement.id()==ID_generate_block)
elaborate_generate_block(to_verilog_generate_block(statement), dest);
else if(statement.id()==ID_generate_case)
elaborate_generate_case(statement, dest);
elaborate_generate_case(to_verilog_generate_case(statement), dest);
else if(statement.id()==ID_generate_if)
elaborate_generate_if(statement, dest);
elaborate_generate_if(to_verilog_generate_if(statement), dest);
else if(statement.id()==ID_generate_for)
elaborate_generate_for(statement, dest);
elaborate_generate_for(to_verilog_generate_for(statement), dest);
else if(statement.id() == ID_decl)
elaborate_generate_decl(to_verilog_decl(statement), dest);
else if(statement.id() == ID_inst)
Expand Down Expand Up @@ -223,7 +223,7 @@ Function: verilog_typecheckt::elaborate_generate_case
\*******************************************************************/

void verilog_typecheckt::elaborate_generate_case(
const exprt &statement,
const verilog_generate_caset &statement,
module_itemst &dest)
{
}
Expand All @@ -241,7 +241,7 @@ Function: verilog_typecheckt::elaborate_generate_if
\*******************************************************************/

void verilog_typecheckt::elaborate_generate_if(
const exprt &statement,
const verilog_generate_ift &statement,
module_itemst &dest)
{
if(statement.operands().size()!=3 &&
Expand Down Expand Up @@ -360,35 +360,26 @@ Function: verilog_typecheckt::elaborate_generate_for
\*******************************************************************/

void verilog_typecheckt::elaborate_generate_for(
const exprt &statement,
const verilog_generate_fort &for_statement,
module_itemst &dest)
{
if(statement.operands().size()!=4)
{
error().source_location = statement.source_location();
error() << "generate_for expects four operands" << eom;
throw 0;
}

auto &for_statement = to_multi_ary_expr(statement);

elaborate_generate_assign(for_statement.op0(), dest);
elaborate_generate_assign(for_statement.init(), dest);

// work out what the loop index is
auto loop_index = generate_for_loop_index(for_statement.op0());
auto loop_index = generate_for_loop_index(for_statement.init());

while(true)
{
mp_integer condition =
convert_integer_constant_expression(for_statement.op1());
convert_integer_constant_expression(for_statement.cond());

if(condition==0) break;

// Order is important!
// First execute the block.
// If it's a generate_block, append the loop counter to
// the block's identifier, surrounded by square brackets.
auto copy_of_body = for_statement.op3();
auto copy_of_body = for_statement.body();
if(copy_of_body.id() == ID_generate_block)
{
const mp_integer loop_index_int =
Expand All @@ -401,6 +392,6 @@ void verilog_typecheckt::elaborate_generate_for(
elaborate_generate_item(copy_of_body, dest);

// Now increase the loop counter.
elaborate_generate_assign(for_statement.op2(), dest);
elaborate_generate_assign(for_statement.increment(), dest);
}
}
8 changes: 5 additions & 3 deletions src/verilog/verilog_typecheck.h
Original file line number Diff line number Diff line change
Expand Up @@ -209,9 +209,11 @@ class verilog_typecheckt:
void elaborate_generate_decl(const verilog_declt &, module_itemst &dest);
void elaborate_generate_inst(const verilog_instt &, module_itemst &dest);
void elaborate_generate_item(const exprt &statement, module_itemst &dest);
void elaborate_generate_if(const exprt &statement, module_itemst &dest);
void elaborate_generate_case(const exprt &statement, module_itemst &dest);
void elaborate_generate_for(const exprt &statement, module_itemst &dest);
void elaborate_generate_if(const verilog_generate_ift &, module_itemst &dest);
void
elaborate_generate_case(const verilog_generate_caset &, module_itemst &dest);
void
elaborate_generate_for(const verilog_generate_fort &, module_itemst &dest);
exprt generate_for_loop_index(const exprt &initialization_statement) const;

// generate state
Expand Down

0 comments on commit 699db59

Please sign in to comment.