IEEE1800にはアサーションを書くための演算子や文法がたくさんありますが、すべてを知らなくても実際の検証用のチェッカは書けるのではないかと思います。そこでこれだけは覚えておけばいいんじゃないというものをあげておきます。
concurrent assertionとimmediate assertionがありますがクロック同期の回路の検証用としては通常concurrent assertionをつかうとおもいますのでconcurrent assertionについて考えます。

property ~ endproperty

次のassert宣言の中にpropertyを書いてしまえばproperty宣言はいりませんが、基本として
propertyの名前、引数、clock節、 disable iff、property本体で構成される形式は知っておく必要があるでしょう。

assert宣言

property宣言はそれだけではシミュレーターなどでチェックする動作はしません。propertyをassertすることでチェックするようになります。

演算子

|-> |=>
##n ##[m:n]
[*n] [*m:n]
not

system functions

$past()
$rose()
$fell()
$stable()
\$onehot() $onehot0()

bind

アサーションを書いたチェッカmoduleを検証対象のmoduleと接続するためにbind文を使うのが一般的だと思います。

実際によく使うものということだけでなくOVLやARMのAXI用のチェッカのコードを調べてみて大体上記のものだけで書かれていましたのでこれだけ覚えておけばたいていのチェックができると思います。
シミュレーターだけでなくFormal検証ツールを使うのであれば

assume

は必須です。
あとは

sequence 名前付きのsequenceを定義する
throughout
intersect
[->]

くらいでしょうか。

下記の日本ケイデンスの矢ケ部さんの記事の中に「覚えておくべきアサーションのシンタックス」という表があります。
アサーション活用の手引き (2/5)
上記では

( ) sequenceの区切り
[=n] 非連続繰り返し

たしかにsequenceの繰り返しを書く時に( )はつかいますね。
[=]がありますが個人的には [->]の方が好きです。その辺は好き好きということで。
矢ケ部さんの記事に、全部の文法を知らなくても8割がたのチェッカは書けますということで、ここに上げたものをおぼえておけばだいたいOKということがEDAベンダの方も考えているということが分かりました。