22어트리뷰트로 컴파일러 제어하기

어트리뷰트는 BSV 타입과 rule 본문으로 표현할 수 없는 사실을 소스에 적어 컴파일러에 전달하는 문법입니다. 생성 RTL에서 유지할 모듈 경계, 생성 포트의 이름, 존재해야 하는 핸드셰이크 신호, 허용되는 rule 스케줄이 이런 사실에 해당합니다. 어떤 어트리뷰트는 컴파일러가 수행하는 요청이고, 어떤 어트리뷰트는 컴파일러가 증명해야 하는 단언이며, 어떤 어트리뷰트는 컴파일러가 그대로 믿는 단언입니다.

모듈, 인터페이스, 원자적 rule, method 조건, implicit condition, 그리고 정적·동적 의미론 장의 컴파일 세 단계를 알고 있어야 합니다. FIFO·split·라이브러리 primitive 장의 FIFO와 FIFOF는 저장 상태에 따라 준비 상태가 달라지므로, 프로토콜 단언이 참인지 판단할 때 좋은 사례가 됩니다.

예제는 모두 bsc로 컴파일해 Verilog를 생성하고 Icarus Verilog로 시뮬레이션합니다. 실행을 누르면 모든 단계가 차례로 실행됩니다.

1. 어트리뷰트 문법

1.1 어트리뷰트 쓰는 법

어트리뷰트는 (*와 *) 사이에 씁니다. 이름을 하나 이상 쉼표로 구분해 나열하고, 값이 필요한 이름은 = 뒤에 값을 씁니다. 어트리뷰트는 바로 뒤에 오는 문법 요소에 적용됩니다.

형식

(* 이름 *)
(* 이름 = 값 *)
(* 이름1, 이름2 = 값 *)

(* synthesize, clock_prefix = "CORE_CLK" *)
module mkCore(CoreIfc);
  ...
endmodule

참고. 어트리뷰트는 주석이 아니며 시뮬레이션 중에 실행되지도 않습니다. 컴파일러가 검사하거나 생성하는 내용을 바꿉니다.

1.2 어트리뷰트의 네 종류

어트리뷰트의 효과는 어느 컴파일 단계에 작용하는지에 따라 달라집니다.

주의. 마지막 종류가 가장 위험합니다. 시뮬레이션에서 위반이 나타나지 않았다고 모든 입력 순서에서 단언이 성립한다는 증명이 되지는 않습니다. 그런데도 합성된 하드웨어는 그 단언을 전제로 만든 스케줄을 따릅니다.

2. 모듈과 함수의 경계

2.1 synthesize는 모듈을 따로 생성합니다

(* synthesize *)는 BSV 모듈을 별도의 Verilog 모듈로 생성하라는 요청입니다. 다른 곳의 인스턴스는 부모 모듈에 인라인되지 않고 생성된 정의를 참조합니다.

형식

(* synthesize *)
module mk이름(인터페이스_타입);
  ...
endmodule

(* synthesize *)
module mkCounter(Counter);
  Reg#(UInt#(8)) count <- mkReg(0);
  method Action incr;
    count <= count + 1;
  endmethod
  method UInt#(8) value = count;
endmodule

method가 계산하는 결과는 그대로이고 계층 구조만 바뀝니다. 그래도 준비 조건·모듈 인자·합성 경계 장에서 처음 본 대로 별도 경계는 스케줄에 영향을 줄 수 있습니다. method 인자 하나는 하드웨어 포트 하나가 되고, 포트 하나는 한 사이클에 값 하나만 전달합니다. 그래서 같은 사이클에 서로 다른 인자로 호출하려는 호출자 둘은 충돌합니다. 인라인된 모듈이라면 호출자마다 별도의 논리를 둘 수 있습니다. 또한 생성 모듈마다 스케줄러가 따로 있으므로 경계를 넘어 rule 사이의 관계를 지정할 수 없습니다.

2.2 noinline은 함수에 같은 경계를 만듭니다

최상위 함수 앞의 (* noinline *)는 함수를 호출할 때마다 펼치지 말고 별도의 Verilog 모듈로 생성하라는 요청입니다.

형식

(* noinline *)
function 결과_타입 이름(인자_타입 인자);
  ...
endfunction

(* noinline *)
function Bit#(1) parity8(Bit#(8) x);
  return ^x;
endfunction

parity8을 호출하는 설계를 컴파일하면 module_parity8.v도 생성됩니다. 인자와 결과가 포트가 되므로 모두 Bits 인스턴스가 있어야 합니다. 경계를 두면 컴파일 작업이 줄고 구조가 드러나지만 배선이 늘어납니다.

2.3 예제: 경계 뒤의 증가기

ModuleBoundary.bsv의 Incrementer는 load method로 받은 값에 1을 더해 저장합니다. Incrementer 인터페이스를 먼저 읽고, 두 synthesize를 찾은 다음, loadValue와 showResult에서 step이 바뀌는 순서를 따라가세요. 실행 명령은 mkIncrementer와 mkTop을 따로 생성합니다.

실행하기 전에 예측해 보세요.

1. 컴파일 단계는 Verilog 파일을 몇 개 생성하며, 파일 이름은 무엇일까요?
2. load(8'h2a) 다음에 showResult는 10진수로 어떤 값을 출력할까요?
3. 값을 넣고 읽는 사이에 한 사이클 간격을 만드는 것은 synthesize일까요, step일까요?

package ModuleBoundary;

interface Incrementer;
  method Action load(Bit#(8) value);
  method Bit#(8) result;
endinterface

// 이 모듈을 별도의 RTL 경계로 생성한다.
(* synthesize *)
module mkIncrementer(Incrementer);
  Reg#(Bit#(8)) valueReg <- mkReg(0);

  method Action load(Bit#(8) value);
    valueReg <= value + 1;
  endmethod

  method Bit#(8) result = valueReg;
endmodule

(* synthesize *)
module mkTop(Empty);
  Incrementer incrementer <- mkIncrementer;
  Reg#(Bit#(2)) step <- mkReg(0);

  rule loadValue (step == 0);
    incrementer.load(8'h2a);
    step <= 1;
  endrule

  rule showResult (step == 1);
    $display("incremented = %0d", incrementer.result);
    $finish(0);
  endrule
endmodule

endpackage

결과 확인.

한 사이클 간격은 synthesize가 아니라 step이 만듭니다. 출력값은 동작을, 두 파일은 경계를 확인합니다.

직접 바꿔 보세요.

1. 자식 모듈의 synthesize를 지우고 명령에서 -g mkIncrementer를 빼서 mkTop만 생성하세요. 시뮬레이션은 여전히 43을 출력하지만 생성 파일은 mkTop.v 하나입니다. 증가기의 레지스터와 논리가 부모 모듈에 인라인되었습니다. 동작은 같고 구현 경계만 사라졌습니다.

3. 포트 이름과 프로토콜 어트리뷰트

3.1 Ready와 Enable

합성된 method에는 데이터 포트와 함께 제어 신호 두 개가 생길 수 있습니다. 두 신호는 호출의 서로 다른 쪽에서 구동합니다.

value method에는 결과와 Ready가 있을 수 있지만, 요청할 Action이 없으므로 Enable은 없습니다.

3.2 생성 포트 이름 바꾸기

이름 지정 어트리뷰트는 생성 RTL 포트의 철자만 바꿉니다. BSV 호출 코드는 같은 method 이름을 계속 씁니다.

형식

interface 이름;
  (* result = "PORT", ready = "PORT_RDY" *)
  method 타입 valueMethod;

  (* enable = "PORT_EN", prefix = "" *)
  method Action actionMethod((* port = "PORT_IN" *) 타입 arg);
endinterface

3.3 always_ready와 always_enabled

두 어트리뷰트는 제어 포트를 없애는 대신, 컴파일러가 증명해야 하는 단언을 만듭니다.

형식

(* always_ready *)   method 타입 이름;           // Ready 포트 없음
(* always_enabled *) method Action 이름(...);    // Enable 포트 없음

interface Tick;
  (* always_enabled *)
  method Action tick(Bit#(1) pulse);
  (* always_ready *)
  method UInt#(8) count;
endinterface

method에 상태에 따른 조건이 있으면 단언이 거짓이므로 컴파일 오류가 발생합니다. 어트리뷰트가 조건을 숨겨 주지는 않습니다.

3.4 예제: 포트 이름을 바꾼 카운터

PortProtocol.bsv의 NamedCounter에는 value method인 value와 Action method인 load가 있습니다. 구현보다 인터페이스를 먼저 읽으세요. 어트리뷰트는 value의 결과 포트 이름을 COUNT로 바꾸고, value가 항상 준비되어 있다고 단언하며, load의 Enable 이름을 LOAD로 바꿉니다.

사이클 0에 loadValue가 8'h3c를 인자로 제시하고, 이름이 LOAD로 바뀐 Enable로 Action을 선택합니다. count == 8'h3c는 클록 에지에 반영됩니다. 사이클 1에 showValue가 이름이 COUNT인 포트로 반영된 값을 읽습니다.

실행하기 전에 예측해 보세요.

1. mkTop이 쓰는 이름은 load와 value일까요, LOAD와 COUNT일까요?
2. load가 값을 쓰는 사이클에 value가 새 값을 볼 수 있을까요?
3. 출력되는 10진수 값은 무엇일까요?
4. mkNamedCounter.v에서 어느 Ready 포트가 없어지고, 어느 Ready 포트가 남을까요?

package PortProtocol;

interface NamedCounter;
  // BSV method는 그대로 두고 생성 포트의 이름만 바꾼다.
  (* result = "COUNT", always_ready *)
  method Bit#(8) value;

  (* enable = "LOAD" *)
  method Action load(Bit#(8) next);
endinterface

(* synthesize *)
module mkNamedCounter(NamedCounter);
  Reg#(Bit#(8)) count <- mkReg(0);

  method Bit#(8) value = count;

  method Action load(Bit#(8) next);
    count <= next;
  endmethod
endmodule

(* synthesize *)
module mkTop(Empty);
  NamedCounter counter <- mkNamedCounter;
  Reg#(Bit#(2)) step <- mkReg(0);

  rule loadValue (step == 0);
    counter.load(8'h3c);
    step <= 1;
  endrule

  rule showValue (step == 1);
    $display("named counter = %0d", counter.value);
    $finish(0);
  endrule
endmodule

endpackage

결과 확인.

출력값은 동작만 증명합니다. 포트 계약은 생성된 Verilog에서 확인합니다. BSV 코드는 계속 counter.load와 counter.value를 호출합니다.

직접 바꿔 보세요.

1. always_ready는 그대로 두고 value에 상태에 따른 조건 if (count != 0)을 추가하세요. mkNamedCounter 생성 단계에서 오류 G0006("Method(s) not always ready: value")이 발생합니다. Ready 포트는 method가 실제로 모든 사이클에 준비되어 있을 때만 없앨 수 있습니다. 실제 핸드셰이크를 되살리거나, 단언이 참이 되도록 method를 고치세요.

4. 스케줄링 어트리뷰트

4.1 한 사이클의 스케줄 순서

스케줄링 어트리뷰트를 이해하려면 한 사이클을 다음 순서로 따라가세요.

1. 사이클 시작 상태로 각 rule의 명시적 조건을 계산합니다.
2. rule이 호출하는 모든 method의 준비 조건을 더합니다. 이것이 implicit condition입니다.
3. 같은 레지스터에 쓰는 두 rule처럼 서로 충돌하는 경우를 찾습니다.
4. 긴급도에 따라 서로 충돌하지 않는 실행 가능한 rule의 집합을 고릅니다.
5. 고른 rule을 허용되는 순서로 놓고, 모든 갱신을 사이클 끝에 함께 반영합니다.

스케줄링 어트리뷰트는 3–5단계에 작용합니다. 어떤 어트리뷰트도 거짓인 조건을 참으로 만들지 못합니다.

4.2 descending_urgency

실행 가능한 두 rule이 충돌하면 하나만 실행됩니다. descending_urgency는 스케줄러가 어느 rule을 먼저 고려할지 정합니다.

형식

(* descending_urgency = "더_긴급한_rule, 덜_긴급한_rule" *)

(* descending_urgency = "flush, accept" *)
rule flush (flushRequested);
  dropped <= count;
  count <= 0;
endrule

rule accept (inputValid);
  count <= count + 1;
endrule

두 rule이 모두 count를 읽고 쓰므로 어느 순서로도 놓을 수 없어 충돌합니다. 두 조건이 같은 사이클에 참이면 flush가 실행되고 accept는 기다립니다. accept만 실행 가능하면 평소처럼 실행됩니다. 긴급도 관계는 추이적이며, a > b, b > c, c > a처럼 순환하면 컴파일 오류가 발생합니다.

긴급도는 충돌하는 rule 사이에서만 의미가 있습니다. dropped <= count;를 지우면 두 rule은 더 이상 충돌하지 않습니다. accept가 flush의 쓰기보다 먼저 count를 읽으므로 accept를 flush 앞에 둘 수 있기 때문입니다.

4.3 execution_order와 preempts

형식

(* execution_order = "먼저, 나중" *)
(* preempts = "이기는_rule, 지는_rule" *)

(* preempts = "urgent, background" *)
rule urgent (step == 0);
  a <= 1;
  step <= 1;
endrule

rule background (step < 2);
  b <= b + 1;
endrule

위의 urgent와 background는 서로 다른 레지스터에 쓰므로 원래는 함께 실행될 수 있습니다. preempts가 있으면 urgent가 실행되는 사이클마다 background가 실행되지 않으므로 사이클 0이 끝난 뒤에도 b는 0입니다. 어트리뷰트를 지우면 사이클 0에 두 rule이 함께 실행되어 b가 1이 됩니다.

4.4 rule 단언: fire_when_enabled와 no_implicit_conditions

두 어트리뷰트는 컴파일러가 증명해야 하는 단언을 rule에 붙입니다.

형식

(* fire_when_enabled *)
(* no_implicit_conditions *)

(* fire_when_enabled, no_implicit_conditions *)
rule tick;
  count <= count + 1;
endrule

tick은 레지스터만 읽고 쓰므로 두 단언을 모두 만족합니다. 여기에 queue.deq 호출을 더하면 no_implicit_conditions가 오류 G0005로 실패합니다. 더 긴급한 충돌 rule에 막힐 수 있는 rule에 fire_when_enabled를 붙여도 G0005가 발생하고, 오류 메시지가 막는 rule의 이름을 알려 줍니다.

(* descending_urgency = "inc, clear" *)
rule inc;
  count <= count + 1;
endrule

(* fire_when_enabled *)
rule clear (count > 3);
  count <= 0;
endrule

4.5 신뢰되는 단언: mutually_exclusive와 conflict_free

형식

(* mutually_exclusive = "r1, r2" *)
(* conflict_free = "r1, r2" *)

(* mutually_exclusive = "left, right" *)
rule left (step == 1 && sel);
  a <= a + 1;
endrule

rule right (step == 1 && !sel);
  a <= a - 1;
endrule

컴파일러는 두 단언을 증명하지 않습니다. 단언을 이용해 덜 보수적인 스케줄을 만들고, 위반 여부는 시뮬레이션에서만 검사됩니다. 위의 코드에서는 sel과 !sel이 실제로 배타적이므로 단언이 사실과 맞습니다.

4.6 예제: 충돌하는 두 rule의 긴급도

RulePriority.bsv의 두 선택 rule은 모두 selected와 pending에 씁니다. pending과 safetyRequested의 초기값을 읽고, 두 선택 rule이 쓰는 레지스터를 모두 적어 보세요.

첫 사이클에는 두 조건이 모두 참이고 두 rule이 충돌합니다. descending_urgency 때문에 스케줄러는 chooseSafety를 먼저 고려하고, chooseSafety가 selected == 8'ha5를 반영하며 pending을 거짓으로 만듭니다. chooseNormal은 그 사이클에 실행되지 않습니다. 다음 사이클에는 두 선택 rule이 모두 비활성이고 showSelection이 값을 출력합니다.

실행하기 전에 예측해 보세요.

1. 첫 사이클에 두 선택 rule은 모두 실행 가능할까요?
2. selected에는 어떤 값이 반영될까요?
3. chooseNormal이 실행되는 사이클이 있을까요?

package RulePriority;

(* synthesize *)
module mkTop(Empty);
  Reg#(Bit#(8)) selected <- mkReg(0);
  Reg#(Bool) pending <- mkReg(True);
  Reg#(Bool) safetyRequested <- mkReg(True);

  // 쓰기 충돌이 생기면 safety rule을 먼저 선택한다.
  (* descending_urgency = "chooseSafety, chooseNormal" *)
  rule chooseSafety (pending && safetyRequested);
    selected <= 8'ha5;
    pending <= False;
  endrule

  rule chooseNormal (pending);
    selected <= 8'h11;
    pending <= False;
  endrule

  rule showSelection (!pending);
    $display("selected = %h", selected);
    $finish(0);
  endrule
endmodule

endpackage

결과 확인.

직접 바꿔 보세요. 변경은 하나씩 따로 시험하세요.

1. safetyRequested를 False로 시작하세요. chooseSafety가 비활성이므로 긴급도가 결정할 것이 없고, chooseNormal이 8'h11을 반영합니다. 긴급도는 겹친 경우를 해결할 뿐 조건을 대신하지 않습니다.
2. 어트리뷰트를 "chooseNormal, chooseSafety"로 뒤집으세요. 출력이 11이 되고 bsc가 경고 G0021로 chooseSafety가 절대 실행될 수 없다고 알립니다. chooseSafety가 실행 가능할 때는 pending도 참이므로, 더 긴급한 chooseNormal도 항상 함께 실행 가능합니다.
3. 어트리뷰트를 지우세요. 출력은 그대로 a5지만 bsc가 경고 G0010으로 chooseSafety를 임의로 더 긴급하게 처리했다고 알리고, pending 읽기·쓰기 충돌을 나열합니다. 상태를 공유하는 rule 장에서 설명한 바로 그 경고 쌍입니다. descending_urgency를 execution_order로 바꾸어도 같은 경고가 나옵니다. 함께 실행될 수 없는 두 rule에 순서를 정해도 충돌은 해결되지 않습니다.

5. split과 nosplit

if나 case가 있는 rule은 분기마다 다른 상태를 다루더라도 보통 한 단위로 실행됩니다. 조건문 앞의 (* split *)는 각 분기를 별도의 조건과 스케줄을 가진 rule 조각으로 나누라는 요청입니다. (* nosplit *)는 그 아래에서 분할을 멈춥니다.

형식

(* split *)
if (조건) 동작1; else 동작2;

rule route;
  (* split *)
  if (sel) a <= x;
  else     b <= x;
endrule

분할한 뒤에는 a에 쓰는 분기가, b에 대한 쓰기와만 충돌하는 다른 rule과 함께 실행될 수 있습니다.

주의. 독립적인 조건문이 많으면 조각 수가 지수적으로 늘어나 스케줄링이 느려지고, 분기 조건을 매 사이클 계산하는 논리도 늘어납니다. 실제로 이유 없이 막힌 분기를 찾은 뒤에만 split을 쓰세요.

6. 클록, 리셋, 인자, doc 어트리뷰트

이 어트리뷰트들은 기존 RTL과 연결할 수 있도록 합성된 모듈의 바깥 모양을 정합니다.

(* synthesize, clock_prefix = "CORE_CLK", reset_prefix = "CORE_RST_N" *)
module mkCore(CoreIfc);
  ...
endmodule

(* doc = "routes one value per cycle" *)
rule route;
  ...
endrule

주의. 포트 이름은 외부와의 계약입니다. clock_prefix = "CORE_CLK"를 쓰면 mkCore의 클록 입력 이름이 CORE_CLK가 되므로, CLK라는 포트에 연결하는 기존 테스트벤치는 더 이상 elaboration되지 않습니다. BSV 안에서 닫힌 설계는 기본 이름을 쓰세요.

7. 자주 하는 실수

7.1 조건이 있는 method에 always_ready 붙이기

// 잘못된 코드: 인터페이스는 always_ready를 단언하는데 ...
interface Counter;
  (* always_ready *)
  method Bit#(8) value;
endinterface
// ... 모듈이 method에 조건을 둔다: G0006 "Method(s) not always ready"
method Bit#(8) value if (count != 0) = count;

// 바른 코드: 인터페이스에서 always_ready를 빼고 Ready 포트를 유지한다
interface Counter;
  method Bit#(8) value;
endinterface

always_ready는 Ready를 없애므로, 호출자가 값이 유효하지 않은 때에도 method를 읽을 수 있게 됩니다. 그래서 method가 모든 상태에서 준비되어 있지 않으면 컴파일 오류가 발생합니다. method 어트리뷰트는 인터페이스 선언에 씁니다. 모듈 안의 method 정의에 쓰면 오류 P0022("Attributes not allowed for method")가 발생합니다.

7.2 FIFO를 쓰는 rule에 no_implicit_conditions 붙이기

// 잘못된 코드: q.first와 q.deq는 항상 준비되어 있지 않으므로 G0005
(* no_implicit_conditions *)
rule drain;
  r <= q.first;
  q.deq;
endrule

// 바른 코드: 단언을 지운다. rule은 의도대로 데이터를 기다린다
rule drain;
  r <= q.first;
  q.deq;
endrule

이 어트리뷰트는 FIFO의 implicit condition을 없애 주지 않습니다. implicit condition이 없다고 단언할 뿐이고, 그 단언이 거짓입니다.

7.3 긴급도 순서를 거꾸로 쓰기

// 잘못된 코드: 일반적인 rule이 특수한 rule보다 앞선다. 경고 G0021
(* descending_urgency = "chooseNormal, chooseSafety" *)

// 바른 코드: 조건이 더 좁은 rule이 더 긴급해야 한다
(* descending_urgency = "chooseSafety, chooseNormal" *)

한 rule의 조건이 다른 rule의 조건을 포함하면, 조건이 더 좁은 쪽이 더 긴급해야 선택될 수 있습니다. G0021은 경고일 뿐이므로 스케줄을 바꿀 때마다 경고를 확인하세요.

7.4 충돌에서 질 수 있는 rule에 fire_when_enabled 붙이기

// 잘못된 코드: 더 긴급한 chooseSafety가 chooseNormal을 막으므로 G0005
(* descending_urgency = "chooseSafety, chooseNormal" *)
rule chooseSafety (pending); ... endrule
(* fire_when_enabled *)
rule chooseNormal (pending); ... endrule

// 바른 코드: 이기는 rule에 단언을 붙이거나 충돌 자체를 없앤다

fire_when_enabled는 다른 rule이 이 rule을 막지 않는다는 약속입니다. 긴급도 결정에서 지는 rule은 정의상 막힙니다.

7.5 경고를 없애려고 신뢰되는 단언 추가하기

// 잘못된 코드: 두 조건이 동시에 참일 수 있으므로 단언이 거짓이다
(* mutually_exclusive = "left, right" *)
rule left  (step == 1);         a <= a + 1; endrule
rule right (step == 1 && sel);  a <= a - 1; endrule

mutually_exclusive와 conflict_free는 증명되지 않고 그대로 믿어집니다. 불변식을 따로 적고, 그 불변식을 유지하는 상태 전이를 찾은 뒤에만 단언을 추가하세요. 그 논증을 세울 수 없다면 보수적인 스케줄이 옳습니다.

8. 정리

9. 확인 문제

1. 별도 합성 경계가 method의 결과를 바꾸지 않으면서 동시성을 줄일 수 있는 까닭은 무엇일까요?

   정답 보기

   별도 모듈의 method 인자는 한 사이클에 값 하나만 전달하는 포트 하나가 됩니다. 그래서 같은 사이클에 다른 인자가 필요한 호출자 둘은 충돌합니다. 인라인된 모듈이라면 호출자마다 별도의 논리를 둘 수 있습니다. method 안의 계산은 어느 쪽이든 같습니다.

2. method 호출에서 Ready와 Enable은 각각 어느 쪽이 구동할까요?

   정답 보기

   Ready는 method를 구현한 모듈이 구동하며, 호출을 처리할 수 있는지 알립니다. Enable은 호출하는 쪽이 구동하며, 이번 사이클에 Action method를 호출한다고 알립니다.

3. RulePriority.bsv에서 descending_urgency가 두 선택 rule이 모두 실행 가능할 때만 결과를 바꾸는 까닭은 무엇일까요?

   정답 보기

   긴급도는 충돌하는 실행 가능 rule 사이에서만 결정합니다. chooseSafety의 조건이 거짓이면 결정할 것이 없으므로 chooseNormal이 혼자 실행됩니다.

4. 단언이 거짓일 때 no_implicit_conditions와 mutually_exclusive는 어떻게 다를까요?

   정답 보기

   no_implicit_conditions는 컴파일러가 증명하므로 거짓이면 G0005로 컴파일이 중단됩니다. mutually_exclusive는 그대로 믿어지므로 거짓이어도 컴파일되고, 두 조건을 실제로 함께 참으로 만드는 시뮬레이션 실행만이 위반을 드러냅니다.

5. (* preempts = "urgent, background" *)의 두 rule은 서로 다른 레지스터에 씁니다. 두 rule이 같은 사이클에 실행될 수 있을까요?

   정답 보기

   실행될 수 없습니다. preempts는 실제 충돌이 없어도 충돌을 강제하고 앞의 rule에 우선권을 줍니다. urgent가 실행되는 사이클에는 background가 실행되지 않습니다.

아래 실습 문제는 이 장의 계약을 적용합니다. bounded buffer의 enqueue method에 붙은 준비 상태 단언이 버퍼 자신의 상태와 모순되는 문제, 조건 없는 tick method를 always-enabled RTL 프로토콜로 선언하는 문제, 의존하는 큐의 상태와 스케줄링 단언이 모순되는 rule을 다루는 문제입니다.