속성 사양 언어

Property Specification Language

PSL(Property Specification Language)은 표현 용이성과 표현력 향상을 위해 연산자의 범위를 가진 선형 시간 로직을 확장하는 시간 로직입니다.PSL은 정규 표현과 구문적 당도를 폭넓게 사용합니다.하드웨어 설계 및 검증 업계에서 널리 사용되고 있습니다.여기서 공식 검증 도구(모델 확인 등) 및/또는 논리 시뮬레이션 도구를 사용하여 특정 PSL 공식이 특정 설계에 적용된다는 것을 증명하거나 반박합니다.

PSL은 처음에 Accellera에 의해 하드웨어 설계에 대한 특성 또는 주장을 지정하기 위해 개발되었습니다.2004년 9월부터 IEEE 1850 워킹그룹에서 언어 표준화가 실시되고 있습니다.2005년 9월에는 IEEE 1850 Property Specification Language(PSL) 표준이 발표되었습니다.

구문 및 의미론

PSL은 어떤 시나리오가 지금 발생할 경우 잠시 후 다른 시나리오가 발생할 수 있음을 나타낼 수 있습니다.예를 들어 속성 "a"는요청은 항상 최종적으로 부여되어야 한다"는 PSL 공식으로 나타낼 수 있습니다.

  always (요청 -> 결국! grant)

"ACK 신호 직후에 이어지는 모든 요구에는 완전한 데이터 전송이 이어져야 합니다.여기서 완전한 데이터 전송은 신호 시작에서 시작하여 신호 종료로 끝나는 시퀀스이며, 그 사이에 비지가 유지됩니다."라는 속성은 PSL 공식으로 나타낼 수 있습니다.

  (true[*]; req; ack) => (시작; 비지[*]; 종료)

이 공식을 만족시키는 트레이스가 오른쪽 그림에 제시되어 있습니다.

만족시키는 단순한 흔적
(true[*]; req; ack) => (시작; 비지[*]; 종료)

PSL의 시간 연산자는 대략 LTL 형식의 연산자와 정규식 형식의 연산자로 분류할 수 있습니다.많은 PSL 연산자에는 느낌표 서픽스(!)로 표시되는 강력한 버전과 약한 버전의 두 가지 버전이 있습니다.강력한 버전은 우발성 요건(즉, 미래에 어떤 것이 유지될 것을 요구한다)을 만드는 반면 약한 버전은 그렇지 않다.포함요건과 비포괄요건을 구별하기 위해 밑줄서픽스( _ )를 사용합니다._a 및 _e 접미사는 보편적(모든) 요건과 존재적(기존적) 요건을 나타내기 위해 사용됩니다.정확한 시간 창은 [n]로 표시되고 유연성은 [m..n]로 표시됩니다.

SERE 스타일의 연산자

가장 일반적으로 사용되는 PSL 연산자는 =>로 표시되는 "복제" 연산자(일명 "복제" 연산자)이다.왼쪽 피연산자는 PSL 정규 표현식이고 오른쪽 피연산자는 임의의 PSL 공식(LTL 스타일 또는 정규 표현 스타일)입니다.r = > p의 의미는 i까지의 시간 시퀀스가 정규식 r과 일치하도록 모든 시점 i에서 i+1로부터의 패스는 속성 p를 만족시켜야 한다는 것이다.이것은 오른쪽 그림에 예시되어 있습니다.

r을 만족시키는 패스는 2개의 연속되지 않는 방법으로 p를 트리거합니다.
r을 만족시키는 경로는 두 가지 중복되는 방법으로 p를 트리거합니다.
r'을 만족시키는 경로는 세 가지 방법으로 p'를 트리거합니다.

PSL의 정규 표현식에는 연결(;), 클리어 클로저(*), 결합( )의 공통 연산자 및 퓨전(:), 교집합(\&) 및 약한 버전(\&)의 연산자 및 연속 카운팅 [*n]과 연속 카운팅(in-continuous counting)의 많은 변형이 있습니다.[=n] 및 [->n]입니다.

트리거 연산자는 아래 표에 나와 있는 것처럼 여러 가지 변형으로 제공됩니다.

여기서 및 t는 PSL 정규식이고 p는 PSL 공식입니다. 

 s = > t!
 s가 일치하면 트레이스의 서픽스에 t가 일치합니다.
  • t가 종료된 후 사이클을 시작합니다.
  • t의 매치는 끝까지 도달해야 한다.
 s -> t!
 s가 일치하면 트레이스의 서픽스에 t가 일치합니다.
  • t는 종료하는 사이클과 같은 사이클을 시작합니다.
  • t의 매치는 끝까지 도달해야 한다.
 s = > t
 s가 일치하면 트레이스의 서픽스에 t가 일치합니다.
  • t가 종료된 후 사이클을 시작합니다.
  • t의 매치는 중간에 끼일 수 있다
 s -> t
 s가 일치하면 트레이스의 서픽스에 t가 일치합니다.
  • t는 종료하는 사이클과 같은 사이클을 시작합니다.
  • t의 매치는 중간에 끼일 수 있다

연결, 융접, 결합, 교차로 및 그 변동에 대한 연산자가 아래 표에 나와 있습니다.

다음 및 t는 PSL 정규 표현입니다.

s ; t 의 일치 후에 t의 일치가 이어집니다.t는 이 종료된 후에 사이클을 시작합니다.
s : t 의 일치 후에 t의 일치가 이어집니다.t는 종료된 사이클과 같은 사이클을 시작합니다.
s t 일치 또는 일치 t
s && t 의 일치와 t의 일치, 양쪽의 지속 시간은 같은 길이입니다.
s & t 의 일치와 t의 일치, 기간 일치의 차이가 있을 수 있습니다.
s within t t의 일치 내에서 s의 일치, ([*]; s; [*]) & (t)의 생략형

연속 반복 연산자는 다음 표에 나와 있습니다.

다음으로 PSL 정규 표현을 나타냅니다.

s[*i] i의 연속된 반복
s[*i..j] s의 i~j회 연속 반복 사이
s[*i..] 적어도 i에서 s의 연속적인 반복
s[*] 연속된 의 반복이 0회 이상
s[+] 의 1개 이상의 연속된 반복

연속되지 않는 반복의 연산자를 다음 표에 나타냅니다.

여기서 b는 임의의 PSL 부울식입니다.

b[=i] 반드시 연속적으로 b를 반복할 필요는 없다.
  • (!b[*];b)[*i];!b[*]와 동등
b[=i..j] 적어도 i에서 j 이하의 b는 반드시 연속적으로 반복되지 않는다.
  • (!b[*];b)[*i..j];!b[*]와 동등
b[=i..] 적어도 나는 b를 연속적으로 반복할 필요는 없다.
  • (!b[*];b)[*i..];!b[*]와 동등
b[->m] m 반드시 b로 끝나는 b의 연속적인 반복은 아니다.
  • (!b[*];b)[*m]과 동등
b[->m:n] b로 끝나는 b를 반드시 연속적으로 반복할 필요는 없다.
  • (!b[*];b)[*m..n]과 동등
b[->m..] 적어도 m은 b로 끝나는 b의 연속적인 반복은 아니다.
  • (!b[*];b)[*m..];!b[*]와 동등
b[->] b[->1] 바로가기,
  • (!b[*];b)에 상당합니다.

LTL 형식의 연산자

다음은 PSL의 일부 LTL 스타일 연산자의 예입니다.

여기서 p와 q는 PSL 공식입니다.

always p 속성 p는 모든 시점을 유지합니다.
never p 속성 p는 어느 시점에서도 유지되지 않습니다.
eventually! p p가 유지되는 미래 시점이 존재한다.
next! p 다음 시점이 존재하며 p는 이 시점으로 유지된다.
next p 다음 시점이 존재하는 경우 p는 이 시점으로 고정됩니다.
next![n] p n번째 시점이 존재하며 p는 이 시점으로 유지된다.
next[n] p n번째 시점이 존재하는 경우 p는 이 시점으로 고정됩니다.
next_e![m..n] p p가 유지되는 전류에서 m번째부터 n번째까지의 시점이 존재합니다.
next_e[m..n] p n번째 이상의 시점이 존재할 경우 p는 m번째에서 n번째 지점 중 하나를 유지합니다.
next_a![m..n] p 최소 n개의 시점이 더 존재하며, p는 m번째부터 n번째까지의 모든 시점으로 고정된다.
next_a[m..n] p p는 다음 m번째부터 n번째까지의 모든 시점을 유지하지만, 많은 경우
p until! q q가 유지되고 p가 그 시점까지 유지되는 시점이 존재합니다.
p until q p는 q가 유지되는 시점(존재하는 경우)까지 버틸 수 있습니다.
p until!_ q q가 유지되고 p가 그 시점과 그 시점까지 유지되는 시점이 존재합니다.
p until_ q p는 q가 유지되는 시점까지 유지되며, 그 시점(존재하는 경우)에
p before! q p는 q가 유지되는 시점까지 엄밀하게 유지되며 p는 최종적으로 유지된다.
p before q p는 q가 유지되는 시점 이전에만 유지되며 p가 유지되지 않으면 q도 유지되지 않습니다.
p before!_ q p는 q가 유지되기 전 또는 같은 시점에 유지되며 p는 최종적으로 유지된다.
p before_ q p는 q가 유지되는 시점 이전 또는 같은 시점에 유지되며 p가 유지되지 않으면 q도 유지되지 않습니다.

샘플링 연산자

다중 클럭 설계의 경우나 더 높은 수준의 추상화가 필요한 경우처럼 다음 시점의 정의를 변경하는 것이 바람직할 수 있습니다.이 목적을 위해 @로 표시된 샘플링 연산자(클럭 연산자)가 사용됩니다.p @ c 공식은 PSL 공식이고, c PSL 부울식은 c가 유지되는 사이클에 투영된 경로 상에 p가 있으면 p @ c는 특정 경로 상에 유지됩니다(오른쪽 그림 참조).

샘플링 연산자의 필요성을 나타내는 경로 및 공식

첫 번째 속성에는 "ACK 신호 직후에 이어지는 모든 요구에는 완전한 데이터 전송이 이어져야 합니다.여기서 완전한 데이터 전송은 신호 시작에서 시작하여 신호 종료로 끝나는 시퀀스로, 데이터가 적어도 8회 유지되어야 합니다.

  (true[*]; req; ack) => (시작; 데이터[=8]; 종료)

단, 상기 신호가 clk가 높은 사이클에서 발생하는 경우만 고려하는 것이 바람직할 수 있습니다.이것은 두 번째 그림에서 설명되지만, 공식은

  ((true[*]; req; ack) => (시작; 데이터[*3]; 종료) @ clk

는 데이터 [*3]를 사용하며 [*n]은 연속된 반복입니다.일치하는 트레이스에는 데이터가 보관 유지되는 비연속적인 3개의 시점이 있지만 clk가 보관 유지되는 시점만 고려하면 데이터가 보관 유지되는 시점이 연속적으로 됩니다.

샘플링 연산자의 효과를 나타내는 경로 및 공식 @

중첩된 @ 공식의 의미는 조금 미묘합니다.관심 있는 독자는 [2]를 참조한다.

연산자 중단

PSL에는 잘린 경로(계산 프레픽스에 대응하는 유한 경로)를 처리하는 연산자가 여러 개 있습니다.잘린 경로는 리셋 및 기타 많은 시나리오로 인해 경계 모델 검사에서 발생합니다.중단 연산자는 경로가 잘렸을 때 이벤트를 처리하는 방법을 지정합니다.이들은 [1]에서 제안된 잘린 의미론에 의존합니다.

여기서 p는 임의의 PSL 공식, b는 임의의 PSL 부울식입니다.

p async_abort b p 홀드 또는 p는 b 홀드까지 실패하지 않는다.
  • b 비동기적으로 인식됨
p sync_abort b p 홀드 또는 p는 b 홀드까지 실패하지 않는다.
  • b 동기 인식
p abort b pasync_sync b에 상당합니다.

표현력

PSL은 시간 논리 LTL을 상정하여 표현력을 오메가 정규 언어의 표현력으로 확장합니다.별 없는 δ-정규 표현의 표현력을 가진 LTL과 비교하여 표현력의 증가는 접미사 함축, 즉 "->"로 표시된 트리거 연산자에 기인할 수 있다.r - > f （ r ） 。여기서 r은 정규식, f는 시간논리식이다.w의 prefix 중 하나가 f를 만족하는 연속성을 갖는 경우 w의 계산에서 유지된다.PSL의 다른 비LTL 연산자는 멀티클럭 설계를 지정하기 위한 @ 연산자, 하드웨어 리셋을 처리하기 위한 중단 연산자, 간결성을 위한 로컬 변수입니다.

레이어

PSL은 부울 레이어, 시간 레이어, 모델링 레이어 및 검증 레이어의 4개의 레이어로 정의됩니다.

  • Boolean 레이어는 설계의 현재 상태를 기술하기 위해 사용되며 위의 HDL 중 하나를 사용하여 표현됩니다.
  • 시간 계층은 시간 경과에 걸쳐 있는 시나리오를 기술하는 데 사용되는 시간 연산자로 구성됩니다.
  • 모델링 레이어를 사용하여 보조 상태 기계를 절차적으로 설명할 수 있습니다.
  • 검증 계층은 검증 도구에 대한 지시사항(예를 들어, 특정 속성이 올바르다고 단언하거나 다른 속성 집합을 검증할 때 특정 속성 집합이 올바르다고 가정하는 것)으로 구성됩니다.

언어 호환성

Property Specification Language는 다음과 같은 여러 전자 시스템 설계 언어(HDL)와 함께 사용할 수 있습니다.

PSL이 위의 HDL 중 하나와 함께 사용되는 경우 부울 레이어는 각 HDL의 연산자를 사용합니다.

레퍼런스

  • 1850-2005 – IEEE Standard for Property Specification Language (PSL). 2005. doi:10.1109/IEEESTD.2005.97780. ISBN 0-7381-4780-X.
  • 1850-2010 – IEEE Standard for Property Specification Language (PSL). 2010. doi:10.1109/IEEESTD.2010.5446004. ISBN 978-0-7381-6255-3.
  • Eisner, Cindy; Fisman, Dana; Havlicek, John; Lustig, Yoad; McIsaac, Anthony; Van Campenhout, David (2003). "Reasoning with Temporal Logic on Truncated Paths" (PDF). Computer Aided Verification. Lecture Notes in Computer Science. Vol. 2725. p. 27. doi:10.1007/978-3-540-45069-6_3. ISBN 978-3-540-40524-5.
  • Eisner, Cindy; Fisman, Dana; Havlicek, John; McIsaac, Anthony; Van Campenhout, David (2003). "The Definition of a Temporal Clock Operator" (PDF). Automata, Languages and Programming. Lecture Notes in Computer Science. Vol. 2719. p. 857. doi:10.1007/3-540-45061-0_67. ISBN 978-3-540-40493-4.

외부 링크

PSL 관련 서적