Project

General

Profile

Task #4117

Support of replication operation

Added by Alexander Kamkin almost 8 years ago. Updated over 7 years ago.

Status:
Closed
Priority:
High
Category:
-
Target version:
Start date:
04/17/2013
Due date:
% Done:

100%

Estimated time:
Detected in build:
svn
Published in build:
0.2

Description

Replicates bit-vector n-times.

{4{w}} // This is equivalent to {w, w, w, w}

History

#1

Updated by Sergey Smolov almost 8 years ago

  • Status changed from New to Open

Сделаю.

#2

Updated by Sergey Smolov almost 8 years ago

  • Status changed from Open to Resolved
  • Assignee changed from Sergey Smolov to Alexander Kamkin

Реализовал операцию в виде метода со следующей сигнатурой:

public static SolverOperation makeSolverOperation(EVerilogOperation type, int times, BigInteger bitVector)

класс HDLOperations

r71

#3

Updated by Sergey Smolov almost 8 years ago

  • Target version set to 0.1
#4

Updated by Alexander Kamkin over 7 years ago

  • Status changed from Resolved to Open
  • Assignee changed from Alexander Kamkin to Sergey Smolov

В общем случае репликация применяется к выражениям; число повторений - также выражение: expression1{expression2}.

BVREPL лучше сделать обыкновенной бинарной операцией (первый аргумент - вектор, второй - число повторений).

#5

Updated by Sergey Smolov over 7 years ago

  • Status changed from Open to Feedback
  • Assignee changed from Sergey Smolov to Alexander Kamkin

Саша, я нашел в языке SMT-LIB параметризованную операцию repeat, которая довольно похожа на репликацию.

((_ repeat i) (_ BitVec m) (_ BitVec i*m))
- ((_ repeat i) x) means concatenate i copies of x

К сожалению, в качестве числа повторений тут может выступать только число типа Int. Нельзя ни подставить туда переменную типа Int, ни арифметическое выражение.

Насколько я понимаю, данную операцию (а также все параметризованные) нужно хранить так же, как и все обычные операции языка SMT-LIB, но в транслятор добавить специальный кусок кода для правильного отображения параметров операций на SMT-LIB. Верно?

#6

Updated by Alexander Kamkin over 7 years ago

  • Assignee changed from Alexander Kamkin to Sergey Smolov

Нужно сделать так, чтобы в качестве первого аргумента (параметра repeat) можно было задавать произвольную операцию. При отображении в SMT-LIB нужно ругаться, если операция не является константной (или даже не является числом).

В этом случае я смогу представить все операции Verilog (кроме вызовов функций) с помощью API.

Это предварительное представление. Следующий этап - вычисление константных выражений (константные выражения схлопнутся в числа, и проблем с отображением в SMT-LIB не будет).

#7

Updated by Alexander Kamkin over 7 years ago

  • Status changed from Feedback to New
  • Priority changed from Normal to High
#8

Updated by Sergey Smolov over 7 years ago

  • Status changed from New to Open
#9

Updated by Sergey Smolov over 7 years ago

  • Status changed from Open to Resolved
  • Assignee changed from Sergey Smolov to Alexander Kamkin

Реализовал поддержку операции repeat, а также вычисление константных выражений. В числа сейчас схлопываются только Integer'ы, в будущем можно расширить данный функционал и на все существующие в библиотеке типы.

r82

#10

Updated by Sergey Smolov over 7 years ago

  • % Done changed from 0 to 100
  • Published in build set to 0.2
#11

Updated by Sergey Smolov over 7 years ago

  • Status changed from Resolved to Closed

Also available in: Atom PDF