Project

General

Profile

Actions
Copy link

Bug #9296

closed

vcegar-tests/cache_coherence/two_processor_bin_2.v:46: illegal types of "then" and "else" expressions : unsigned word[1] and boolean

Added by Sergey Smolov about 6 years ago. Updated over 5 years ago.

Status:
Closed
Priority:
High
Assignee:
Alexander Kamkin
Target version:
0.1
Start date:
10/04/2018
Due date:
% Done:

100%

Estimated time:
Detected in build:
master
Platform:
Published in build:
0.1.1-beta-190722

Description

The 46th line of two_processor_bin_2.v file:

assign ND_inB = (master_outA ) ? ND_inA : (ndB && !bus_ackB);

produces the error via model checking:
illegal types of "then" and "else" expressions : unsigned word[1] and boolean

The ND_inA variable has 1-bit vector dataType ("then"), but the "ndB && !bus_ackB" expression ("else") is represented by the VeriTrans as follows: (AND (EQ bus_ackB 0) (NOT (EQ ndB 0))).
So it has Boolean data type since all operations are logic, not bitvector-oriented.

Actions
Copy link
 #1

Updated by Sergey Smolov over 5 years ago

  • Status changed from New to Closed
  • % Done changed from 0 to 100
  • Published in build set to 0.1.1-beta-190722
Actions
Copy link

Also available in: Atom PDF