From cfba8209b947011623313781c669b13c2dbb791c Mon Sep 17 00:00:00 2001 From: Florian Zaruba Date: Sun, 15 Oct 2017 13:37:26 +0200 Subject: [PATCH 1/3] :memo: Add apb adapter --- docs/examples/amba/apb.fl | 0 docs/examples/amba/apb2sram.fl | 106 +++++++++++++++++++++++++++++ docs/examples/{axi => amba}/axi.fl | 0 3 files changed, 106 insertions(+) create mode 100644 docs/examples/amba/apb.fl create mode 100644 docs/examples/amba/apb2sram.fl rename docs/examples/{axi => amba}/axi.fl (100%) diff --git a/docs/examples/amba/apb.fl b/docs/examples/amba/apb.fl new file mode 100644 index 0000000..e69de29 diff --git a/docs/examples/amba/apb2sram.fl b/docs/examples/amba/apb2sram.fl new file mode 100644 index 0000000..2fc884e --- /dev/null +++ b/docs/examples/amba/apb2sram.fl @@ -0,0 +1,106 @@ +module apb2sram (apb : APB, sram: ! SRAMBus) { + + fsm { + + fork { + apb.read(addr, data); + sram.read(addr, data); + } + + fork { + apb.write(addr, data); + sram.write(addr, data); + } + } +} + +struct APB { + addr : int32; + rdata : ! int32; + wdata : int32; + en : int1; + strb : int4; + ready : ! int1; + write : int1; + sel : int1; +} + +struct SRAM { + addr : int32; + rdata : ! int32; + wdata : int32; + wen : int; +} + +trans read (addr : int32, data : int32) on APB { + self.sel = 1; + self.en = 0; + self.write = 0; + self.addr = addr; + addr = self.addr; + clk; + self.en = 1; + self.ready = 1; + self.rdata = data; + while !self.ready { clk; } + data = self.rdata; + clk; +} + +trans write (addr : int32, data : int32) on APB { + self.sel = 1; + self.en = 0; + self.write = 1; + self.wdata = data; + self.addr = addr; + self.strb = 15; + addr = self.addr; + data = self.wdata; + clk; + self.en = 1; + self.ready = 1; + while !self.ready { clk; } + clk; +} + +trans read (addr : int32, data : int32) on SRAM { + self.addr = addr; + addr = self.addr; + + if self.we == 0 { + self.we = 0; + } + + clk; + data = self.rdata; +} + +trans write (addr : int32, data : int32) on SRAM { + self.addr = addr; + addr = self.addr; + self.we = 1; + self.wdata = data; + data = self.wdata; + clk; +} + +# READ +Req (Master): + +self.addr = addr; +self.we = 0; +clk; +data = self.rdata; + +1. Assignments to outputs +2. Reads from inputs + +Resp (Slave): + +addr = self.addr; +self.we = 0; +clk; +data = self.rdata; + +1. Assignment to inputs +2. \ No newline at end of file diff --git a/docs/examples/axi/axi.fl b/docs/examples/amba/axi.fl similarity index 100% rename from docs/examples/axi/axi.fl rename to docs/examples/amba/axi.fl From 5b5e939ab03eb1dff706d24f1eb9f668e3f1bfa5 Mon Sep 17 00:00:00 2001 From: Fabian Schuiki Date: Sun, 15 Oct 2017 17:37:36 +0200 Subject: [PATCH 2/3] Add APB implementation doodles --- docs/examples/amba/apb2sram.fl | 80 ++++++++++++++++++++++++++++++---- docs/examples/amba/apb_a.txt | 40 +++++++++++++++++ docs/examples/amba/apb_b.txt | 47 ++++++++++++++++++++ docs/examples/amba/apb_c.txt | 71 ++++++++++++++++++++++++++++++ 4 files changed, 230 insertions(+), 8 deletions(-) create mode 100644 docs/examples/amba/apb_a.txt create mode 100644 docs/examples/amba/apb_b.txt create mode 100644 docs/examples/amba/apb_c.txt diff --git a/docs/examples/amba/apb2sram.fl b/docs/examples/amba/apb2sram.fl index 2fc884e..7d14451 100644 --- a/docs/examples/amba/apb2sram.fl +++ b/docs/examples/amba/apb2sram.fl @@ -1,5 +1,4 @@ -module apb2sram (apb : APB, sram: ! SRAMBus) { - +module apb2sram (apb: APB, sram: ! SRAMBus) { fsm { fork { @@ -63,15 +62,43 @@ trans write (addr : int32, data : int32) on APB { clk; } +# "Formal" description +trans read (addr: int32, data: int32) on APB { + nop { clk; } + property self.sel == 1; + property self.en == 0; + property self.write == 0; + property self.addr == addr; + clk; + property self.en == 1; + nop { clk; } + property self.ready == 1; + property self.rdata == data; + clk; + release; +} + +trans write (addr: int32, data: int32) on APB { + nop { clk; } + property self.sel == 1; + property self.en == 0; + property self.write == 1; + property self.addr == addr; + property self.wdata == data; + clk; + property self.en == 1; + nop { clk; } + property self.ready == 1; + clk; + release; +} + trans read (addr : int32, data : int32) on SRAM { self.addr = addr; addr = self.addr; - - if self.we == 0 { - self.we = 0; - } - + self.we = 0; clk; + self.data = rdata; data = self.rdata; } @@ -84,6 +111,43 @@ trans write (addr : int32, data : int32) on SRAM { clk; } +struct Reg { + value: T, +} + +tran set (value: const T) on Reg { + let tmp = value; + clk; + self.value = tmp; +} + +tran get (value: T) on Reg { + value = self.value; +} + +module MyMagicSRAM (bus: in SRAM) { + let words: [Reg; 1024]; + + fsm { + INITIAL: { + let addr; + let data; + with bus.read(addr, data) { + let tmp = addr; + clk; + data = words[tmp]; + } + with bus.write(addr, data) { + let tmpA = addr; + let tmpD = data; + clk; + words[tmpA] = tmpD; + } + with epsilon { clk; } + } + } +} + # READ Req (Master): @@ -103,4 +167,4 @@ clk; data = self.rdata; 1. Assignment to inputs -2. \ No newline at end of file +2. diff --git a/docs/examples/amba/apb_a.txt b/docs/examples/amba/apb_a.txt new file mode 100644 index 0000000..c5eafdd --- /dev/null +++ b/docs/examples/amba/apb_a.txt @@ -0,0 +1,40 @@ +module MyMagicSRAM ( + input logic clk, + input logic rst_n, + input logic [31:0] bus_addr, + output logic [31:0] bus_rdata, + input logic [31:0] bus_wdata, + input logic bus_wen +); + + + +endmodule + + +/* +INITIAL: + -- bus.read --> INITIAL (A) + -- bus.write --> INITIAL (B) + +INITIAL: + self.addr = addr; (A) + addr = self.addr; (A) + self.we = 0; (A) + -> A2; (A) +A2: + self.data = rdata; (A) + data = self.rdata; (A) + -> INITIAL; (A) + +INITIAL: + self.addr = addr; (B) + addr = self.addr; (B) + self.we = 1; (B) + self.wdata = data; (B) + data = self.wdata; (B) + -> B2; (B) +B2: + -> INITIAL; (B) + +*/ diff --git a/docs/examples/amba/apb_b.txt b/docs/examples/amba/apb_b.txt new file mode 100644 index 0000000..1403470 --- /dev/null +++ b/docs/examples/amba/apb_b.txt @@ -0,0 +1,47 @@ +module MyMagicSRAM ( + input logic clk, + input logic rst_n, + input logic [31:0] bus_addr, + output logic [31:0] bus_rdata, + input logic [31:0] bus_wdata, + input logic bus_wen +); + + + +endmodule + + +/* +INITIAL: + -- bus.read --> INITIAL (A) + -- bus.write --> INITIAL (B) + +--------------------------- + +INITIAL: + self.addr = addrA; (A) + addrA = self.addr; (A) + let tmpA = addrA; (A) + self.we = 0; (A) + --- + dataA = words[tmpA]; (A) + self.rdata = dataA; (A) + dataA = self.rdata; (A) + -> INITIAL; (A) + +--------------------------- + +INITIAL: + self.addr = addrB; (B) + addrB = self.addr; (B) + let tmpAB = addrB; (B) + self.we = 1; (B) + self.wdata = dataB; (B) + dataB = self.wdata; (B) + let tmpDB = dataB; (B) + --- + words[tmpAB] = tmpDB; (B) + -> INITIAL; (B) + +*/ diff --git a/docs/examples/amba/apb_c.txt b/docs/examples/amba/apb_c.txt new file mode 100644 index 0000000..ef27980 --- /dev/null +++ b/docs/examples/amba/apb_c.txt @@ -0,0 +1,71 @@ +read_master { + sel <= 1; + en <= 0; + write <= 0; + addr <= @ADDR; + clk; + en <= 1; + while !ready { clk; } + let @DATA = rdata; + clk; + // sel <= 0; + // en <= 0; + // addr <= X; +} + +write_master { + sel <= 1; + en <= 0; + write <= 1; + addr <= @ADDR; + wdata <= @DATA; + clk; + en <= 1; + while !ready { clk; } + clk; + // sel <= 0; + // en <= 0; + // addr <= X; +} + +read_slave { + while sel != 1 && en == 0 && write == 0 { clk; } + let @ADDR = addr; + clk; + assert(en == 1); + ready <= 1; + rdata <= @DATA; + clk; + // ready <= 0; + // rdata <= X; +} + +write_slave { + while sel != 1 && en == 0 && write == 1 { clk; } + let @ADDR = addr; + let @DATA = wdata; + clk; + assert(en == 1); + ready <= 1; + clk; + // ready <= 0; +} + +rw_slave { + while sel != 1 && en == 0 { clk; } + let @ADDR = addr; + if write == 0 {} + if write == 1 { + let @DATA = wdata; + } + clk; + assert(en == 1); + ready <= 1; + if write == 0 { + rdata <= @DATA; + } + if write == 1 {} + clk; + // ready <= 0; + // rdata <= X; +} From 84ea9b134d45b306801273535f8993ee6f746278 Mon Sep 17 00:00:00 2001 From: Fabian Schuiki Date: Sun, 15 Oct 2017 17:44:59 +0200 Subject: [PATCH 3/3] Add APB monitor example --- docs/examples/amba/apb_c.txt | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/docs/examples/amba/apb_c.txt b/docs/examples/amba/apb_c.txt index ef27980..b024bfa 100644 --- a/docs/examples/amba/apb_c.txt +++ b/docs/examples/amba/apb_c.txt @@ -29,7 +29,7 @@ write_master { } read_slave { - while sel != 1 && en == 0 && write == 0 { clk; } + while sel != 1 && en != 0 && write != 0 { clk; } let @ADDR = addr; clk; assert(en == 1); @@ -41,7 +41,7 @@ read_slave { } write_slave { - while sel != 1 && en == 0 && write == 1 { clk; } + while sel != 1 && en != 0 && write != 1 { clk; } let @ADDR = addr; let @DATA = wdata; clk; @@ -52,7 +52,7 @@ write_slave { } rw_slave { - while sel != 1 && en == 0 { clk; } + while sel != 1 && en != 0 { clk; } let @ADDR = addr; if write == 0 {} if write == 1 { @@ -69,3 +69,11 @@ rw_slave { // ready <= 0; // rdata <= X; } + +read_monitor { + while sel != 1 && en != 0 && write != 0 { clk; } + clk; + assert(en == 1); + while !ready { clk; } + clk; +}